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

Wong, Tin Lok

doi:10.1090/proc/13125

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