Automated search for Gödel’s proofs. (English) Zbl 1064.03010
Summary: We present strategies and heuristics underlying a search procedure that finds proofs for Gödel’s incompleteness theorems at an abstract axiomatic level. As axioms we take for granted the representability and derivability conditions for the central syntactic notions as well as the diagonal lemma for constructing self-referential sentences. The strategies are logical ones and have been developed to search for natural deduction proofs in classical first-order logic. The heuristics are mostly of a very general mathematical character and are concerned with the goal-directed use of definitions and lemmata. When they are specific to the meta-mathematical context, these heuristics allow us, for example, to move between the object- and meta-theory. Instead of viewing this work as high-level proof search, it can be regarded as a first step in a proof-planning framework: the next refining steps would consist in verifying the axiomatically given conditions. Comparisons with the literature are detailed in Section 4. (The general mathematical heuristics are indeed general: in Appendix B we show that they, together with two simple algebraic facts and the logical strategies, suffice to find a proof of “\(\sqrt {2}\) is not rational”.)
MSC:
| 03B35 | Mechanization of proofs and logical operations |
| 68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
| 68T20 | Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) |
References:
| [1] | Ammon, K., An automatic proof of Gödel’s incompleteness theorem, Artificial Intelligence, 61, 291-306 (1993) · Zbl 0779.68073 |
| [2] | Boolos, G., The Logic of Provability (1993), Cambridge University Press · Zbl 0891.03004 |
| [3] | Brüning, S.; Thielscher, M.; Bibel, W., Letter to the editor, Artificial Intelligence, 61, 353-354 (1993) |
| [4] | A. Bundy, D. Basin, D. Hutter, A. Ireland, Rippling: Meta-level guidance for mathematical reasoning, Book manuscript, 2003; A. Bundy, D. Basin, D. Hutter, A. Ireland, Rippling: Meta-level guidance for mathematical reasoning, Book manuscript, 2003 · Zbl 1095.68108 |
| [5] | A. Bundy, F. Giunchiglia, A. Villafiorita, T. Walsh, An incompleteness theorem via abstraction, Technical Report #9302-15, Istituto per la ricerca scientifica e tecnologica, Trento, 1996; A. Bundy, F. Giunchiglia, A. Villafiorita, T. Walsh, An incompleteness theorem via abstraction, Technical Report #9302-15, Istituto per la ricerca scientifica e tecnologica, Trento, 1996 · Zbl 0890.03004 |
| [6] | J. Byrnes, Proof search and normal forms in natural deduction, Ph.D. Thesis, Department of Philosophy, Carnegie Mellon University, 1999; J. Byrnes, Proof search and normal forms in natural deduction, Ph.D. Thesis, Department of Philosophy, Carnegie Mellon University, 1999 |
| [7] | Cohen, P. J., Set Theory and the Continuum Hypothesis (1966), Benjamin: Benjamin Reading, MA · Zbl 0182.01301 |
| [8] | (Fricke; Noether; Ore, Gesammelte mathematische Werke, vol. 3 (1933), Vieweg) |
| [9] | Fearnley-Sander, D., Review of Quaife 1992 |
| [10] | Feferman, S., Inductively presented systems and the formalization of meta-mathematics, (van Dalen; Lascar; Smiley, Logic Colloquium ’80 (1982), North-Holland Publishing Company), 95-128 · Zbl 0516.03006 |
| [11] | Feferman, S., Finitary inductively presented logics, (Ferro; etal., Logic Colloquium ’88 (1988), North-Holland Publishing Company), 191-220 · Zbl 0823.03032 |
| [12] | Fitch, F., Symbolic Logic (1952), The Ronald Press Company: The Ronald Press Company New York · Zbl 0049.00504 |
| [13] | Gödel, K., Über formal unentscheidbare Sätze der Principia mathematica und verwandter Systeme I, Monatshefte für Mathematik und Physik, 38, 173-198 (1931) · JFM 57.0054.02 |
| [14] | Löb, M., Solution of a problem of Leon Henkin, The Journal of Symbolic Logic, 20, 115-118 (1955) · Zbl 0067.00202 |
| [15] | Quaife, A., Automated proofs of Löb’s theorem and Gödel’s two incompleteness theorems, Journal of Automated Reasoning, 4, 219-231 (1988) · Zbl 0657.03007 |
| [16] | Quaife, A., Automated Development of Fundamental Mathematical Theories (1992), Kluwer Academic Publishers · Zbl 0773.03010 |
| [17] | Shankar, N., Metamathematics, Machines, and Gödel’s Proof, Cambridge Tracts in Theoretical Computer Science, vol. 38 (1994), Cambridge University Press · Zbl 0813.68150 |
| [18] | W. Sieg, Elementary proof theory, Technical Report 297, Institute for Mathematical Studies in the Social Sciences, Stanford, 1978, p. 104; W. Sieg, Elementary proof theory, Technical Report 297, Institute for Mathematical Studies in the Social Sciences, Stanford, 1978, p. 104 |
| [19] | W. Sieg, Mechanisms and Search (Aspects of Proof Theory), AILA Preprint, 1992; W. Sieg, Mechanisms and Search (Aspects of Proof Theory), AILA Preprint, 1992 |
| [20] | Sieg, W.; Byrnes, J., Normal natural deduction proofs (in classical logic), Studia Logica, 60, 67-106 (1998) · Zbl 0954.03015 |
| [21] | W. Sieg, S. Cittadini, Normal natural deduction proofs (in non-classical logics), Technical Report No. CMU-PHIL-130, 2002, p. 29; W. Sieg, S. Cittadini, Normal natural deduction proofs (in non-classical logics), Technical Report No. CMU-PHIL-130, 2002, p. 29 · Zbl 1098.03026 |
| [22] | Sieg, W.; Lindstrom, I.; Lindstrom, S., Gödel’s incompleteness theorems—a computer-based course in elementary proof theory, (Suppes, P., University-Level Computer-Assisted Instruction at Stanford 1968-80 (1981), Stanford), 183-193 |
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.
