Formalizing non-standard arguments in second-order arithmetic

Research output: Contribution to journalArticlepeer-review

7 Citations (Scopus)


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.

Original languageEnglish
Pages (from-to)1199-1210
Number of pages12
JournalJournal of Symbolic Logic
Issue number4
Publication statusPublished - 2010 Dec

ASJC Scopus subject areas

  • Philosophy
  • Logic


Dive into the research topics of 'Formalizing non-standard arguments in second-order arithmetic'. Together they form a unique fingerprint.

Cite this