Formalizing non-standard arguments in second-order arithmetic
Keita Yokoyama · Journal of Symbolic Logic · 2010
Abstract In this paper, we introduce the systems ns-ACA0and ns-WKL0of non-standard second-order arithmetic in which we can formalize non-standard arguments in ACA0and WKL0, respectively. Then, we give direct transformations from non-standard proofs in ns-ACA0or ns-WKL0into proofs in ACA0or WKL0.