Interpreting Weak König’s Lemma using the Arithmetized Completeness Theorem
HTML articles powered by AMS MathViewer
- by Tin Lok Wong PDF
- Proc. Amer. Math. Soc. 144 (2016), 4021-4024 Request permission
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
- Jeremy Avigad, Formalizing forcing arguments in subsystems of second-order arithmetic, Ann. Pure Appl. Logic 82 (1996), no. 2, 165–191. MR 1419805, DOI 10.1016/0168-0072(96)00003-6
- 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
- Petr Hájek and Pavel Pudlák, Metamathematics of first-order arithmetic, Perspectives in Mathematical Logic, Springer-Verlag, Berlin, 1993. MR 1219738, DOI 10.1007/978-3-662-22156-3
- 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
- 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, DOI 10.1016/j.apal.2014.10.003
- 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
- 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, DOI 10.1016/S0049-237X(98)80023-2
- 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, DOI 10.1017/CBO9780511581007
- 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, DOI 10.1016/0168-0072(86)90074-6
Additional Information
- Tin Lok Wong
- Affiliation: Kurt Gödel Research Center for Mathematical Logic, University of Vienna, Austria
- MR Author ID: 825514
- Email: tin.lok.wong@univie.ac.at
- 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
- © Copyright 2016 American Mathematical Society
- Journal: Proc. Amer. Math. Soc. 144 (2016), 4021-4024
- MSC (2010): Primary 03C62, 03F25, 03H15
- DOI: https://doi.org/10.1090/proc/13125
- MathSciNet review: 3513557