×

On formalization of model-theoretic proofs of Gödel’s theorems. (English) Zbl 0822.03032

Summary: Within a weak subsystem of second-order arithmetic \(\text{WKL}_ 0\), that is \(\Pi_ 2^ 0\)-conservative over PRA, we reformulate Kreisel’s proof of the Second Incompleteness Theorem and Boolos’ proof of the First Incompleteness Theorem.

MSC:

03F35 Second- and higher-order arithmetic and fragments
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Boolos, G., “A new proof of the Gödel Incompleteness Theorem,” Notices of the American Mathematical Society , vol. 36 (1989), pp. 388–390. · Zbl 0972.03544
[2] Feferman, S., “Arithmetization of metamathematics in a general setting,” Fundamenta Mathematicae , vol. 49 (1960), pp. 35–92. · Zbl 0095.24301
[3] Kikuchi, M., “A note on Boolos’ proof of the Incompleteness Theorem,” Mathematical Logic Quarterly , vol. 40 (1994), pp. 528–532. · Zbl 0805.03052 · doi:10.1002/malq.19940400409
[4] Kreisel, G., “Notes on arithmetical models for consistent formulae of the predicate calculus,” Fundamenta Mathematicae , vol. 37 (1950), pp. 265–285. · Zbl 0040.00302
[5] Simpson, S., Subsystems of Second Order Arithmetic , forthcoming. · Zbl 0909.03048
[6] Simpson, S., and K. Tanaka, “On the strong soundness of the theory of real closed fields,” Proceedings of the Fourth Asian Logic Conference , (1990), pp. 7–10.
[7] Smoryński, C., “The Incompleteness Theorems,” pp. 821–865 in Handbook of Mathematical Logic , edited by J. Barwise, North Holland, Amsterdam, 1977.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.