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