Formalizing non-standard arguments in second-order arithmetic

In this paper, we introduce the systems ns-ACA0 and ns-WKL0 of non-standard second-order arithmetic in which we can formalize non-standard arguments in ACA0 and WKL0, respectively. Then, we give direct transformations from non-standard proofs in ns-ACA0 or ns-WKL0 into proofs in ACA0 or WKL0.

• Type: Journal
• Year: 2010
• Where: JSYML
• Authors: Keita Yokoyama
• Keywords: JSYML 2010, Non-standard, Non-standard Arguments, Non-standard Proofs