Abstract
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 heuistics 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 “√2 is not rational”.)
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
K. Ammon: An automatic proof of Gödel’s incompleteness theorem. Artificial Intelligence 61 (1993) pp 291–306
G. Boolos: The logic of provability (Cambridge University Press, Cambridge 1993)
S. Bröning, M. Thielscher and W. Bibel: Letter to the editor. Artificial Intelligence 61 (1993) pp 353–4
A. Bundy, F. Giunchiglia, A. Villafiorita and T. Walsh: An incompleteness theorem via abstraction. Technical Report #9302-15 (Istituto per la ricerca scientifica e tecnologica, Trento 1996)
A. Bundy, D. Basin, D. Hutter and A. Ireland: Rippling: Meta-level guidance for mathematical reasoning (Book manuscript 2003)
J. Byrnes: Proof search and normal forms in natural deduction. Ph.D. Thesis (Department of Philosophy, Carnegie Mellon University 1999)
P. J. Cohen: Set theory and the continuum hypothesis (Benjamin, Reading Mass. 1966)
R. Dedekind: Uber die Einföhrung neuer Funktionen in der Mathematik (Habilitationsrede 1854, pp 428–38) In: Gesammelte mathematische Werke, ed by Fricke, Noether and Ore, vol. 3 (Vieweg 1933)
D. Fearnley-Sander: Review of Quaife [16]. http://psyche.cs.monash.edu.au/
S. Feferman: Inductively presented systems and the formalization of metamathematics. In: Logic Colloquium’ 80, ed by D. van Dalen, D. Lascar and T. J. Smiley (North-Holland, Amsterdam 1982) pp 95–128
S. Feferman: Finitary inductively presented logics. In: Logic Colloquium’ 88, ed by R. Ferro et al. (North-Holland, Amsterdam 1988) pp 191–220
F. Fitch: Symbolic Logic (The Ronald Press Company, New York 1952)
K. Gödel: Uber formal unentscheidbare Sätze der Principia mathematica und verwandter Systeme I. Monatshefte för Mathematik und Physik 38 (1931) pp 173–198
M. Löb: Solution of a problem of Leon Henkin. J. Symbolic Logic 20 (1955) pp 115–118
A. Quaife: Automated proofs of Löb’s theorem and Gödel’s two incompleteness theorems. Journal of Automated Reasoning 4 (1988) pp 219–231
A. Quaife: Automated Development of Fundamental Mathematical Theories (Kluwer, Dordrecht 1992)
N. Shankar: Metamathematics, Machines, and Gödel’s Proof. Cambridge Tracts in Theoretical Computer Science 38 (Cambridge University Press, Cambridge 1994)
W. Sieg: Elementary proof theory. Technical Report 297 (Institute for Mathematical Studies in the Social Sciences, Stanford 1978) 104 pp
W. Sieg: Mechanisms and Search (Aspects of Proof Theory). AILA Preprint (1992)
W. Sieg and J. Byrnes: Normal natural deduction proofs (in classical logic). Studia Logica 60 (1998) pp 67–106
W. Sieg and S. Cittadini: Normal natural deduction proofs (in non-classical logics). Technical Report No. CMU-PHIL-130 (2002) 29 pp. The paper has since been published in: Mechanizing Mathematical Reasoning, ed by Hutter and Stephan (Springer, 2005) pp 169–191
W. Sieg, I. Lindstrom and S. Lindstrom: Gödel’s incompleteness theorems-a computer-based course in elementary proof theory. In: University-Level Computer-Assisted Instruction at Stanford 1968–80, ed by P. Suppes (Stanford 1981) pp 183–193
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer-Verlag Italia
About this chapter
Cite this chapter
Sieg, W., Field, C. (2008). Automated Search for Gödel’s Proofs. In: Lupacchini, R., Corsi, G. (eds) Deduction, Computation, Experiment. Springer, Milano. https://doi.org/10.1007/978-88-470-0784-0_7
Download citation
DOI: https://doi.org/10.1007/978-88-470-0784-0_7
Publisher Name: Springer, Milano
Print ISBN: 978-88-470-0783-3
Online ISBN: 978-88-470-0784-0
eBook Packages: Humanities, Social Sciences and LawPhilosophy and Religion (R0)