Automated Search for Gödel’s Proofs

  • Wilfried Sieg
  • Clinton Field


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”.)


Natural Deduction Derivability Condition Logical Strategy Automate Search Incompleteness Theorem 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    K. Ammon: An automatic proof of Gödel’s incompleteness theorem. Artificial Intelligence 61 (1993) pp 291–306CrossRefGoogle Scholar
  2. 2.
    G. Boolos: The logic of provability (Cambridge University Press, Cambridge 1993)Google Scholar
  3. 3.
    S. Bröning, M. Thielscher and W. Bibel: Letter to the editor. Artificial Intelligence 61 (1993) pp 353–4CrossRefGoogle Scholar
  4. 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)Google Scholar
  5. 5.
    A. Bundy, D. Basin, D. Hutter and A. Ireland: Rippling: Meta-level guidance for mathematical reasoning (Book manuscript 2003)Google Scholar
  6. 6.
    J. Byrnes: Proof search and normal forms in natural deduction. Ph.D. Thesis (Department of Philosophy, Carnegie Mellon University 1999)Google Scholar
  7. 7.
    P. J. Cohen: Set theory and the continuum hypothesis (Benjamin, Reading Mass. 1966)Google Scholar
  8. 8.
    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)Google Scholar
  9. 9.
    D. Fearnley-Sander: Review of Quaife [16]. Scholar
  10. 10.
    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–128Google Scholar
  11. 11.
    S. Feferman: Finitary inductively presented logics. In: Logic Colloquium’ 88, ed by R. Ferro et al. (North-Holland, Amsterdam 1988) pp 191–220Google Scholar
  12. 12.
    F. Fitch: Symbolic Logic (The Ronald Press Company, New York 1952)Google Scholar
  13. 13.
    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–198CrossRefGoogle Scholar
  14. 14.
    M. Löb: Solution of a problem of Leon Henkin. J. Symbolic Logic 20 (1955) pp 115–118CrossRefGoogle Scholar
  15. 15.
    A. Quaife: Automated proofs of Löb’s theorem and Gödel’s two incompleteness theorems. Journal of Automated Reasoning 4 (1988) pp 219–231CrossRefGoogle Scholar
  16. 16.
    A. Quaife: Automated Development of Fundamental Mathematical Theories (Kluwer, Dordrecht 1992)Google Scholar
  17. 17.
    N. Shankar: Metamathematics, Machines, and Gödel’s Proof. Cambridge Tracts in Theoretical Computer Science 38 (Cambridge University Press, Cambridge 1994)Google Scholar
  18. 18.
    W. Sieg: Elementary proof theory. Technical Report 297 (Institute for Mathematical Studies in the Social Sciences, Stanford 1978) 104 ppGoogle Scholar
  19. 19.
    W. Sieg: Mechanisms and Search (Aspects of Proof Theory). AILA Preprint (1992)Google Scholar
  20. 20.
    W. Sieg and J. Byrnes: Normal natural deduction proofs (in classical logic). Studia Logica 60 (1998) pp 67–106CrossRefGoogle Scholar
  21. 21.
    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–191Google Scholar
  22. 22.
    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–193Google Scholar

Copyright information

© Springer-Verlag Italia 2008

Authors and Affiliations

  • Wilfried Sieg
    • 1
  • Clinton Field
    • 1
  1. 1.Department of PhilosophyCarnegie Mellon UniversityUS

Personalised recommendations