Formalizing non-standard arguments in second-order arithmetic

Keita Yokoyama

doi:10.2178/jsl/1286198143

Formalizing non-standard arguments in second-order arithmetic

Keita Yokoyama

SCI - Mathematics

Research output: Contribution to journal › Article › peer-review

7 Citations (Scopus)

Abstract

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

Original language	English
Pages (from-to)	1199-1210
Number of pages	12
Journal	Journal of Symbolic Logic
Volume	75
Issue number	4
DOIs	https://doi.org/10.2178/jsl/1286198143
Publication status	Published - 2010 Dec

ASJC Scopus subject areas

Philosophy
Logic

Access to Document

10.2178/jsl/1286198143

Cite this

@article{dee5eb1a5823447fb386d39ee7536ec1,

title = "Formalizing non-standard arguments in second-order arithmetic",

abstract = "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.",

author = "Keita Yokoyama",

year = "2010",

month = dec,

doi = "10.2178/jsl/1286198143",

language = "English",

volume = "75",

pages = "1199--1210",

journal = "Journal of Symbolic Logic",

issn = "0022-4812",

publisher = "Association for Symbolic Logic",

number = "4",

}

TY - JOUR

T1 - Formalizing non-standard arguments in second-order arithmetic

AU - Yokoyama, Keita

PY - 2010/12

Y1 - 2010/12

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=78951474675&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=78951474675&partnerID=8YFLogxK

U2 - 10.2178/jsl/1286198143

DO - 10.2178/jsl/1286198143

M3 - Article

AN - SCOPUS:78951474675

SN - 0022-4812

VL - 75

SP - 1199

EP - 1210

JO - Journal of Symbolic Logic

JF - Journal of Symbolic Logic

IS - 4

ER -

Formalizing non-standard arguments in second-order arithmetic

Abstract

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this