Remote Access Proceedings of the American Mathematical Society
Green Open Access

Proceedings of the American Mathematical Society

ISSN 1088-6826(online) ISSN 0002-9939(print)



Interpreting Weak König's Lemma using the Arithmetized Completeness Theorem

Author: Tin Lok Wong
Journal: Proc. Amer. Math. Soc. 144 (2016), 4021-4024
MSC (2010): Primary 03C62, 03F25, 03H15
Published electronically: April 20, 2016
MathSciNet review: 3513557
Full-text PDF

Abstract | References | Similar Articles | Additional Information

Abstract: We present a previously unpublished proof of the conservativity of $ \mathrm {WKL}_0$ over  $ \mathrm I\Sigma _1$ using the Arithmetized Completeness Theorem, which, in particular, constitutes an $ \omega $-interpretation of  $ \mathrm {WKL}_0$ in  $ \mathrm I\Sigma _1$. We also show that $ \mathrm {WKL}_0^*$ is interpretable in $ \mathrm I\Delta _0+\mathrm {exp}$.

References [Enhancements On Off] (What's this?)

  • [1] Jeremy Avigad, Formalizing forcing arguments in subsystems of second-order arithmetic, Ann. Pure Appl. Logic 82 (1996), no. 2, 165-191. MR 1419805 (97k:03067),
  • [2] Petr Hájek, Interpretability and fragments of arithmetic, Arithmetic, proof theory, and computational complexity (Prague, 1991), Oxford Logic Guides, vol. 23, Oxford Univ. Press, New York, 1993, pp. 185-196. MR 1236462 (94f:03066)
  • [3] Petr Hájek and Pavel Pudlák, Metamathematics of first-order arithmetic, Perspectives in Mathematical Logic, Springer-Verlag, Berlin, 1993. MR 1219738 (94d:03001)
  • [4] Aleksandar Djordje Ignjatovic, Fragments of first and second-order arithmetic and length of proofs, ProQuest LLC, Ann Arbor, MI, 1990. Thesis (Ph.D.)-University of California, Berkeley. MR 2685328
  • [5] Leszek Aleksander Kołodziejczyk and Keita Yokoyama, Categorical characterizations of the natural numbers require primitive recursion, Ann. Pure Appl. Logic 166 (2015), no. 2, 219-231. MR 3281817,
  • [6] J. B. Paris, Some conservation results for fragments of arithmetic, Model theory and arithmetic (Paris, 1979-1980) Lecture Notes in Math., vol. 890, Springer, Berlin-New York, 1981, pp. 251-262. MR 645006 (83f:03060)
  • [7] Pavel Pudlák, The lengths of proofs, Handbook of proof theory, Stud. Logic Found. Math., vol. 137, North-Holland, Amsterdam, 1998, pp. 547-637. MR 1640332 (99i:03073),
  • [8] Stephen G. Simpson, Subsystems of second order arithmetic, 2nd ed., Perspectives in Logic, Cambridge University Press, Cambridge; Association for Symbolic Logic, Poughkeepsie, NY, 2009. MR 2517689 (2010e:03073)
  • [9] Stephen G. Simpson and Rick L. Smith, Factorization of polynomials and $ \Sigma ^0_1$ induction, Ann. Pure Appl. Logic 31 (1986), no. 2-3, 289-306. Special issue: second Southeast Asian logic conference (Bangkok, 1984). MR 854297 (88b:03093),

Similar Articles

Retrieve articles in Proceedings of the American Mathematical Society with MSC (2010): 03C62, 03F25, 03H15

Retrieve articles in all journals with MSC (2010): 03C62, 03F25, 03H15

Additional Information

Tin Lok Wong
Affiliation: Kurt Gödel Research Center for Mathematical Logic, University of Vienna, Austria

Received by editor(s): July 10, 2015
Received by editor(s) in revised form: October 2, 2015, and November 6, 2015
Published electronically: April 20, 2016
Additional Notes: Part of this paper was presented at the Logic Colloquium in Vienna, Austria, in July 2014. The author was financially supported by the Austrian Science Fund (FWF) project P24654-N25 while this research was carried out.
Communicated by: Mirna Džamonja
Article copyright: © Copyright 2016 American Mathematical Society

American Mathematical Society