Gödel incompleteness theorems and the limits of their applicability. I

L. D. Beklemishev

Trudy Matematicheskogo Instituta imeni V.A. Steklova, Tome 65 (2010) no. 5, pp. 857-899

Résumé

This is a survey of results related to the Gödel incompleteness theorems and the limits of their applicability. The first part of the paper discusses Gödel's own formulations along with modern strengthenings of the first incompleteness theorem. Various forms and proofs of this theorem are compared. Incompleteness results related to algorithmic problems and mathematically natural examples of unprovable statements are discussed. Bibliography: 68 titles.

Détail

Keywords: incompleteness, proof, computability.
Mots-clés : Gödel theorems

Bibliographie

[1] K. Gödel, “Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I”, Monatsh. Math. Phys., 38:1 (1931), 173–198 | DOI | MR | Zbl

[2] R. Zach, “Hilbert's Program”, The Stanford Encyclopedia of Philosophy, ed. E. N. Zalta, 2009 http://plato.stanford.edu/archives/spr2009/entries/hilbert-program/

[3] C. Smorinskii, “The incompleteness theorems”, Handbook of mathematical logic, Stud. Logic Found. Math., 90, ed. J. Barwise, North-Holland, Amsterdam–New York–Oxford, 1977, 821–865 | MR

[4] S. C. Kleene, “Introductory note to 1930b, 1931 and 1932b”, Kurt Gödel. Collected Works, v. 1, Publications 1929–1936, ed. S. Feferman et al., The Clarendon Press, Oxford Univ. Press, New York, 1986, 126–141 | MR | Zbl

[5] K. Gödel, “On undecidable propositions of formal mathematical systems”, Kurt Gödel. Collected Works, v. 1, Publications 1929–1936, The Clarendon Press, Oxford Univ. Press, New York, 1986, 346–373 | MR | Zbl

[6] Kurt Gödel. Collected Works, v. 1, Publications 1929–1936, eds. S. Feferman, J. R. Dawson, S. C. Kleene, G. H. Moore, R. M. Solovay, J. van Heijenoort, The Clarendon Press, Oxford Univ. Press, New York, 1986 | MR | Zbl

[7] A. Tarski, “Der Wahrheitsbegriff in der formalisierten Sprachen”, Stud. Philos., 1 (1935), 261–405 | Zbl

[8] A. Ehrenfeucht, S. Feferman, “Representability of recursively enumerable sets in formal theories”, Arch. Math. Logik Grundlag., 5:1-2 (1960), 37–41 | MR | Zbl

[9] R. M. Smullyan, Diagonalization and self-reference, Oxford Logic Guides, 27, The Clarendon Press, Oxford Univ. Press, New York, 1994, 396 pp. | MR | Zbl

[10] J. B. Rosser, “Gödel theorems for non-constructive logics”, J. Symbolic Logic, 2:3 (1937), 129–137 | DOI | Zbl

[11] W. Craig, “On axiomatizability within a system”, J. Symbolic Logic, 18:1 (1953), 30–32 | DOI | MR | Zbl

[12] S. C. Kleene, “General recursive functions of natural numbers”, Math. Ann., 112:1 (1936), 727–742 | DOI | MR | Zbl

[13] S. C. Kleene, “Recursive predicates and quantifiers”, Trans. Amer. Math. Soc., 53:1 (1943), 41–73 | DOI | DOI | MR | Zbl

[14] S. C. Kleene, “A symmetric form of Gödel's theorem”, Indag. Math., 12 (1950), 244–246 | MR | Zbl

[15] S. C. Kleene, Introduction to metamathematics, Van Nostrand, New York, 1952, 550 pp. | MR | MR | Zbl

[16] R. M. Smullyan, Theory of formal systems, Ann. Math. Stud., 47, Princeton Univ. Press, Princeton, NJ, 1961, 142 pp. | MR | MR | Zbl | Zbl

[17] V. A. Uspenskii, “An elementary exposition of Gödel's incompleteness theorem”, Russian Math. Surveys, 29:1 (1974), 63–106 | DOI | MR | Zbl | Zbl

[18] B. Rosser, “Extensions of some theorems of Gödel and Church”, J. Symbolic Logic, 1:3 (1936), 87–91 | DOI | Zbl

[19] A. Mostowski, “On definable sets of positive integers”, Fund. Math., 34 (1947), 81–112 | MR | Zbl

[20] W. V. Quine, “Concatenation as a basis for arithmetic”, J. Symbolic Logic, 11:4 (1946), 105–114 | DOI | MR | Zbl

[21] A. Tarski, A. Mostowski, R. M. Robinson, Undecidable theories, Stud. Logic Found. Math., North-Holland, Amsterdam, 1953, 98 pp. | MR | Zbl

[22] A. S. Troelstra, H. Schwichtenberg, Basic proof theory, Cambridge Tracts Theoret. Comput. Sci., 43, Cambridge Univ. Press, Cambridge, 1996, 343 pp. | MR | Zbl

[23] J. R. Shoenfield, Mathematical logic, Addison-Wesley, Reading, MA–London–Don Mills, ON, 1967, 344 pp. | MR | MR | Zbl

[24] P. Pudlák, “Cuts, consistency statements and interpretations”, J. Symbolic Logic, 50:2 (1985), 423–441 | DOI | MR | Zbl

[25] S. Feferman, “Arithmetization of metamathematics in a general setting”, Fund. Math., 49 (1960), 35–92 | MR | Zbl

[26] P. Hájek, P. Pudlák, Metamathematics of first-order arithmetic, Perspect. Math. Logic, Springer-Verlag, Berlin, 1993, 460 pp. | MR | Zbl

[27] Yu. V. Matiyasevich, “Enumerable sets are Diophantine”, Soviet Math. Dokl., 11 (1970), 354–358 | MR | Zbl

[28] Yu. V. Matiyasevich, Hilbert's tenth problem, Found. Comput. Ser., MIT Press, Cambridge, MA, 1993, 264 pp. | MR | MR | Zbl | Zbl

[29] Yu. L. Ershov, Problemy razreshimosti i konstruktivnye modeli, Nauka, M., 1980, 416 pp. | MR | Zbl

[30] Yu. L. Ershov, I. A. Lavrov, A. D. Taimanov, M. A. Taitslin, “Elementary theories”, Russian Math. Surveys, 20:4 (1965), 35–105 | DOI | MR | Zbl

[31] A. Bès, “A survey of arithmetical definability. A tribute to Maurice Boffa”, Bull. Belg. Math. Soc. Simon Stevin, 2001, suppl., 1–54 | MR | Zbl

[32] V. Švejdar, “An interpretation of Robinson arithmetic in its Grzegorczyk's weaker variant”, Fund. Inform., 81:1–3 (2007), 347–354 | MR | Zbl

[33] R. L. Vaught, “On a theorem of Cobham concerning undecidable theories”, Logic, Methodology and Philosophy of Science (Proc. 1960 Internat. Congr.), Stanford Univ. Press, Stanford, 1962, 14–25 | MR | Zbl

[34] V. Švejdar, “Weak theories and essential incompleteness”, The Logica Yearbook 2007, Proceedings of the Logica 07 International Conference, ed. M. Peliš, Philosophia, Praha, 2008, 213–224

[35] A. Visser, “Pairs, sets and sequences in first-order theories”, Arch. Math. Logic, 47:4 (2008), 299–326 | DOI | MR | Zbl

[36] A. Visser, Cardinal arithmetic in weak theories, Logic Group Preprint Series, 265, Department of Philosophy, Univ. Utrecht, 2008 http://igitur-archive.library.uu.nl/lg/2008-0422-200811/UUindex.html

[37] H. Putnam, “Decidability and essential undecidability”, J. Symbolic Logic, 22:1 (1957), 39–54 | DOI | MR | Zbl

[38] A. Ehrenfeucht, “Two theories with axioms built by means of pleonasms”, J. Symbolic Logic, 22:1 (1957), 36–38 | DOI | MR | Zbl

[39] J. P. Jones, J. C. Shepherdson, “Variants of Robinson's essentially undecidable theory $R$”, Arch. Math. Logik Grundlag., 23:1 (1983), 61–64 | DOI | MR | Zbl

[40] A. Visser, Why the theory R is special?, Logic Group Preprint Series, 279, Department of Philosophy, Univ. Utrecht, 2009 http://igitur-archive.library.uu.nl/ph/2009-0812-200111/UUindex.html

[41] R. L. Vaught, “Axiomatizability by a schema”, J. Symbolic Logic, 32:4 (1967), 473–479 | DOI | MR | Zbl

[42] S. Feferman, “Finitary inductively presented logics”, Logic Colloquium' 88 (Padova, 1988), Stud. Logic Found. Math., 127, North-Holland, Amsterdam, 1989, 191–220 | MR | Zbl

[43] A. Grzegorczyk, “Undecidability without arithmetization”, Studia Logica, 79:2 (2005), 163–230 | DOI | MR | Zbl

[44] F. Ferreira, “Polynomial time computable arithmetic”, Logic and computation (Pittsburgh, PA, 1987), Contemp. Math., 106, Amer. Math. Soc., Providence, RI, 1990, 137–156 | MR | Zbl

[45] Yu. L. Ershov, Definability and computability, Siberian School of Algebra and Logic, Consultants Bureau, New York, 1996, 262 pp. | MR | MR | Zbl | Zbl

[46] G. J. Chaitin, “Information-theoretic limitations of formal systems”, J. Assoc. Comput. Mach., 21:3 (1974), 403–424 | DOI | MR | Zbl

[47] G. Boolos, “A new proof of Gödel's incompleteness theorem”, Notices Amer. Math. Soc., 36 (1989), 388–390; G. Boolos, “A new proof of Gödel's incompleteness theorem”, Logic, logic, and logic, Harvard Univ. Press, Cambridge, MA, 1998, 383–388 | Zbl

[48] P. Raatikainen, “On interpreting Chaitin's incompleteness theorem”, J. Philos. Logic, 27:6 (1998), 569–586 | DOI | MR | Zbl

[49] M. Kikuchi, “Kolmogorov complexity and the second incompleteness theorem”, Arch. Math. Logic, 36:6 (1997), 437–443 | DOI | MR | Zbl

[50] V. A. Uspenskii, “Teorema Gedelya o nepolnote i chetyre dorogi, veduschie k nei. Lektsiya 1”, Lektsii Letnei shkoly ‘Sovremennaya matematika’, Dubna, 2007 http://www.mathnet.ru/php/presentation.phtml?option_lang=rus&presentid=122

[51] V. A. Uspenskii, Teorema Gedelya o nepolnote, Populyarnye lektsii po matematike, Nauka, M., 1982, 110 pp.

[52] E. Mendelson, Introduction to mathematical logic, Van Nostrand, Princeton, NJ, 1964, 300 pp. | MR | MR | Zbl | Zbl

[53] V. H. Dyson, J. P. Jones, J. C. Shepherdson, “Some Diophantine forms of Gödel's theorem”, Arch. Math. Logik Grundlag., 22:1-2 (1982), 51–60 | DOI | MR | Zbl

[54] P. S. Novikov, “Ob algoritmicheskoi nerazreshimosti problemy tozhdestva slov v teorii grupp”, Tr. MIAN SSSR, 44, Izd-vo AN SSSR, M., 1955, 3–143 | MR | Zbl

[55] S. I. Adyan, “Algoritmicheskaya nerazreshimost problem raspoznavaniya nekotorykh svoistv grupp”, Dokl. AN SSSR, 103:4 (1955), 533–535 | MR | Zbl

[56] S. I. Adyan, “Nerazreshimost nekotorykh algoritmicheskikh problem teorii grupp”, Tr. MMO, 6, 1957, 231–298 | MR | Zbl

[57] A. Bovykin, “Brief introduction to unprovability”, Logic Colloquium 2006, Proceedings of Annual European Conference on Logic of the Association for Symbolic Logic (Radboud University, Nijmegen, 2006), Lect. Notes Log., Assoc. Symbol. Logic, Chicago, IL; Cambridge Univ. Press, Cambridge Cambridge Univ. Press, 2009, 38–64 | MR | Zbl

[58] J. Paris, L. Harrington, “A mathematical incompleteness in Peano arithmetic”, Handbook of mathematical logic, Stud. Logic Found. Math., 90, ed. J. Barwise, North-Holland, Amsterdam–New York–Oxford, 1977, 1133–1142 | MR

[59] L. A. S. Kirby, J. Paris, “Accessible independence results for Peano arithmetic”, Bull. London Math. Soc., 14:4 (1982), 285–293 | DOI | MR | Zbl

[60] A. Kanamori, K. McAloon, “On Gödel's incompleteness and finite combinatorics”, Ann. Pure Appl. Logic, 33:1 (1987), 23–41 | DOI | MR | Zbl

[61] L. D. Beklemishev, “The Worm principle”, Logic Colloquium' 02, Joint proceedings of the Annual European Summer Meeting of the Association for Symbolic Logic and the Biannual Meeting of the German Association for Mathematical Logic and the Foundations of Exact Sciences (the Colloquium Logicum) (Munster, 2002), Lect. Notes Log., 27, Assoc. Symbol. Logic, La Jolla, CA; A K Peters, Ltd., Wellesley, MA, 2006, 75–95 ; Logic Group Preprint Series, 219, Utrecht Univ., March, 2003 | MR | Zbl

[62] M. Hamano, M. Okada, “A relationship among Gentzen's proof-reduction, Kirby–Paris' hydra game, and Buchholz's hydra game”, Math. Logic Quart., 43:1 (1997), 103–120 | DOI | MR | Zbl

[63] S. G. Simpson, “Nichtbeweisbarkeit von gewissen kombintorischen Eigenschaften endlicher Bäume”, Arch. Math. Logik Grundlag., 25:1 (1985), 45–65 | DOI | MR | Zbl

[64] M. Rathjen, A. Weiermann, “Proof-theoretic investigations on Kruskal's theorem”, Ann. Pure Appl. Logic, 60:1 (1993), 49–88 | DOI | MR | Zbl

[65] H. M. Friedman, “Internal finite tree embeddings”, Reflections on the foundations of mathematics (Stanford, CA, 1998), Lect. Notes Log., 15, Assoc. Symbol. Logic, Urbana, IL; A K Peters, Ltd., Natick, MA, 2002, 60–91 | MR | Zbl

[66] W. Buchholz, “An independence result for $(\Pi_1^1\text{-}\mathrm{CA})+\mathrm{BI}$”, Ann. Pure Appl. Logic, 33:2 (1987), 131–155 | DOI | MR | Zbl

[67] H. M. Friedman, “Finite functions and the necessary use of large cardinals”, Ann. of Math. (2), 148:3 (1998), 803–893, arXiv: arXiv: math/9811187 | DOI | MR | Zbl

[68] H. M. Friedman, Downloadable manuscripts at http://www.math.ohio-state.edu/~friedman/manuscripts.html