Automated search for Gödel’s proofs

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 “ √ 2 is not rational”.)