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 selfreferential
sentences. The strategies are logical ones and have been developed to
search for natural deduction proofs in classical firstorder logic.
The heuristics are mostly of a very general
mathematical character
and are concerned with the goaldirected use of definitions and lemmata.
When they are specific to the metamathematical context, these heuristics
allow us, for example, to move between the object and metatheory.
Instead of viewing this work as highlevel proof search, it can be regarded
as a first step in a proofplanning framework: the next refining steps
would consist in verifying the axiomatically given conditions.
