A formally verified abstract account of Gödel’s incompleteness theorems. (English) Zbl 1535.03284
Fontaine, Pascal (ed.), Automated deduction – CADE 27. 27th international conference on automated deduction, Natal, Brazil, August 27–30, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11716, 442-461 (2019).
Summary: We present an abstract development of Gödel’s incompleteness theorems, performed with the help of the Isabelle/HOL theorem prover. We analyze sufficient conditions for the theorems’ applicability to a partially specified logic. In addition to the usual benefits of generality, our abstract perspective enables a comparison between alternative approaches from the literature. These include Rosser’s variation of the first theorem, Jeroslow’s variation of the second theorem, and the Świerczkowski-Paulson semantics-based approach. As part of our framework’s validation, we upgrade Paulson’s Isabelle proof to produce a mechanization of the second theorem that does not assume soundness in the standard model, and in fact does not rely on any notion of model or semantic interpretation.
For the entire collection see [Zbl 1428.68018].
For the entire collection see [Zbl 1428.68018].
MSC:
| 03F40 | Gödel numberings and issues of incompleteness |
| 68V15 | Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) |
References:
| [1] | Ammon, K., An automatic proof of Gödel’s incompleteness theorem, Artif. Intell., 61, 2, 291-306 (1993) · Zbl 0779.68073 · doi:10.1016/0004-3702(93)90070-R |
| [2] | Auerbach, D., Intensionality and the Gödel theorems, Philos. Stud. Int. J. Philos. Anal. Tradit., 48, 3, 337-351 (1985) |
| [3] | Blanchette, JC; Popescu, A.; Traytel, D.; Demri, S.; Kapur, D.; Weidenbach, C., Unified classical logic completeness, Automated Reasoning, 46-60 (2014), Cham: Springer, Cham · Zbl 1409.68250 · doi:10.1007/978-3-319-08587-6_4 |
| [4] | Boolos, G., The Logic of Provability (1993), Cambridge: Cambridge University Press, Cambridge · Zbl 0891.03004 |
| [5] | Buldt, B., The scope of Gödel’s first incompleteness theorem, Log. Univers., 8, 3, 499-552 (2014) · Zbl 1339.03004 · doi:10.1007/s11787-014-0107-3 |
| [6] | Bundy, A., Giunchiglia, F., Villafiorita, A., Walsh, T.: An incompleteness theorem via abstraction. Technical report, Istituto per la Ricerca Scientifica e Tecnologica, Trento (1996) · Zbl 0890.03004 |
| [7] | Carnap, R., Logische syntax der sprache, Philos. Rev., 44, 4, 394-397 (1935) · doi:10.2307/2179996 |
| [8] | Davis, M., The Undecidable: Basic Papers on Undecidable Propositions, Unsolvable Problems, and Computable Functions (1965), Mineola: Dover Publication, Mineola · Zbl 1099.03002 |
| [9] | Diaconescu, R., Institution-Independent Model Theory (2008), Basel: Birkhäuser, Basel · Zbl 1144.03001 |
| [10] | Feferman, S.; Dawson, JW Jr; Kleene, SC; Moore, GH; Solovay, RM; van Heijenoort, J., Kurt Gödel: Collected Works. Vol. 1: Publications 1929-1936 (1986), Oxford: Oxford University Press, Oxford |
| [11] | Fiore, M.P., Plotkin, G.D., Turi, D.: Abstract syntax and variable binding. In: Logic in Computer Science (LICS) 1999, pp. 193-202. IEEE Computer Society (1999) |
| [12] | Gabbay, MJ; Mathijssen, A., Nominal (universal) algebra: equational logic with names and binding, J. Log. Comput., 19, 6, 1455-1508 (2009) · Zbl 1191.08003 · doi:10.1093/logcom/exp033 |
| [13] | Gödel, K., Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I, Monatshefte für Mathematik und Physik, 38, 1, 173-198 (1931) · JFM 57.0054.02 · doi:10.1007/BF01700692 |
| [14] | Goguen, JA; Burstall, RM, Institutions: abstract model theory for specification and programming, J. ACM, 39, 1, 95-146 (1992) · Zbl 0799.68134 · doi:10.1145/147508.147524 |
| [15] | Harrison, J.: HOL light proof of Gödel’s first incompleteness theorem. http://code.google.com/p/hol-light/, directory Arithmetic |
| [16] | Hilbert, D.; Bernays, P., Grundlagen der Mathematik (1939), Heidelberg: Springer, Heidelberg · Zbl 0020.19301 |
| [17] | Jeroslow, RG, Redundancies in the Hilbert-Bernays derivability conditions for Gödel’s second incompleteness theorem, J. Symb. Log., 38, 3, 359-367 (1973) · Zbl 0276.02031 · doi:10.2307/2273028 |
| [18] | Kaliszyk, C.; Urban, J., HOL(y)Hammer: online ATP service for HOL light, Math. Comput. Sci., 9, 1, 5-22 (2015) · Zbl 1322.68177 · doi:10.1007/s11786-014-0182-0 |
| [19] | Kikuchi, M.; Kurahashi, T., Generalizations of Gödel’s incompleteness theorems for \(\sum\) n-definable theories of arithmetic, Rew. Symb. Logic, 10, 4, 603-616 (2017) · Zbl 1426.03038 · doi:10.1017/S1755020317000235 |
| [20] | Kossak, R., Mathematical Logic (2018), Cham: Springer, Cham · Zbl 1462.03002 · doi:10.1007/978-3-319-97298-5 |
| [21] | Kunčar, O.; Popescu, A.; Urban, C.; Zhang, X., A consistent foundation for Isabelle/HOL, Interactive Theorem Proving, 234-252 (2015), Cham: Springer, Cham · Zbl 1433.68556 · doi:10.1007/978-3-319-22102-1_16 |
| [22] | Kunčar, O.; Popescu, A.; Yang, H., Comprehending Isabelle/HOL’s consistency, Programming Languages and Systems, 724-749 (2017), Heidelberg: Springer, Heidelberg · Zbl 1485.68285 · doi:10.1007/978-3-662-54434-1_27 |
| [23] | Löb, M., Solution of a problem of Leon Henkin, J. Symb. Log., 20, 2, 115-118 (1955) · Zbl 0067.00202 · doi:10.2307/2266895 |
| [24] | Nipkow, T.; Wenzel, M.; Paulson, LC, Isabelle/HOL (2002), Heidelberg: Springer, Heidelberg · Zbl 1097.68632 · doi:10.1007/3-540-45949-9 |
| [25] | O’Connor, R.; Hurd, J.; Melham, T., Essential incompleteness of arithmetic verified by Coq, Theorem Proving in Higher Order Logics, 245-260 (2005), Heidelberg: Springer, Heidelberg · Zbl 1152.03315 · doi:10.1007/11541868_16 |
| [26] | Paulson, LC, A machine-assisted proof of Gödel’s incompleteness theorems for the theory of hereditarily finite sets, Rew. Symb. Logic, 7, 3, 484-498 (2014) · Zbl 1337.03021 · doi:10.1017/S1755020314000112 |
| [27] | Paulson, LC, A mechanised proof of Gödel’s incompleteness theorems using Nominal Isabelle, J. Autom. Reason., 55, 1, 1-37 (2015) · Zbl 1357.68200 · doi:10.1007/s10817-015-9322-8 |
| [28] | Paulson, L.C., Blanchette, J.C.: Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers. In: The 8th International Workshop on the Implementation of Logics, IWIL 2010, Yogyakarta, Indonesia, 9 October 2011, pp. 1-11 (2010) |
| [29] | Popescu, A.; Roşu, G., Term-generic logic, Theor. Comput. Sci., 577, 1-24 (2015) · Zbl 1310.03044 · doi:10.1016/j.tcs.2015.01.047 |
| [30] | Popescu, A., Trayel, D.: A formally verified abstract account of Gödel’s incompleteness theorems (extended report) (2019). https://bitbucket.org/traytel/abstract_incompleteness/downloads/report.pdf · Zbl 1535.03284 |
| [31] | Popescu, A., Traytel, D.: Formalization associated with this paper (2019). https://bitbucket.org/traytel/abstract_incompleteness/ |
| [32] | Quaife, A., Automated proofs of Löb’s theorem and Gödel’s two incompleteness theorems, J. Autom. Reason., 4, 2, 219-231 (1988) · Zbl 0657.03007 · doi:10.1007/BF00244396 |
| [33] | Raatikainen, P.: Gödel’s incompleteness theorems. In: The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University (2018) |
| [34] | Schlichtkrull, A.; Blanchette, JC; Traytel, D.; Waldmann, U.; Galmiche, D.; Schulz, S.; Sebastiani, R., Formalizing Bachmair and Ganzinger’s ordered resolution prover, Automated Reasoning, 89-107 (2018), Cham: Springer, Cham · Zbl 1468.68306 · doi:10.1007/978-3-319-94205-6_7 |
| [35] | Shankar, N., Metamathematics, Machines, and Gödel Proof (1994), Cambridge: Cambridge University Press, Cambridge · Zbl 0813.68150 · doi:10.1017/CBO9780511569883 |
| [36] | Sieg, W.: Elementary proof theory. Technical report, Institute for Mathematical Studies in the Social Sciences, Stanford (1978) |
| [37] | Sieg, W.; Field, C., Automated search for Gödel’s proofs, Ann. Pure Appl. Logic, 133, 1-3, 319-338 (2005) · Zbl 1064.03010 · doi:10.1016/j.apal.2004.10.014 |
| [38] | Smith, P., An Introduction to Gödel’s Incompleteness Theorems (2007), Cambridge: Cambridge University Press, Cambridge |
| [39] | Smorynski, C.; Barwise, J., The incompleteness theorems, Handbook of Mathematical Logic, 821-865 (1977), Amsterdam: North-Holland, Amsterdam · doi:10.1016/S0049-237X(08)71123-6 |
| [40] | Świerczkowski, S., Finite sets and Gödel incompleteness theorems, Diss. Math., 422, 1-58 (2003) · Zbl 1058.03065 |
| [41] | Tarski, A., Mostowski, A., Robinson, R.: Undecidable Theories. Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam (1953). 3rd edn. 1971 · Zbl 0053.00401 |
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.
