Ernest Schimmerling

Mathematical logic seminar - April 20, 2004

Time: 12 - 1:30 p.m.

Room: Wean Hall 7220

Speaker:     Wilfried Sieg
Professor and Head
Philosophy Department
Carnegie Mellon University

Title: Automated Search for Gödel's Proofs

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