DIMACS Seminar


Title:

Self-Verifying Axiom Systems and the Polynomial Hierarchy

Speaker:

Dan Willard
SUNY - Albany

Place:

Seminar Room 431, CoRE Building, Busch Campus
Rutgers University

Time:

11:00 AM
Monday, June 5, 1995

Abstract:

Define an axiom system \alpha to be self-verifying iff

1. Under some (suitably weak) definition of consistency, the system \alpha can verify its own consistency.

2. The system \alpha is, in fact, consistent. (Requirement 2 is necessary because Godel's Incompleteness Theorem does not preclude an inconsistent axiom system from formally verifying a theorem asserting its own consistency.)

This talk will introduce two new axiom frameworks, called ISIT and ISITR. The first framework maps an arbitrary initial axiom system A onto an axiom system ISIT(A) which is self-verifying and can prove all the \Pi_1 theorems that A can prove. If conventional ZF-Set Theory is consistent, then our first Consistency-Preservation Theorem will establish that if A is consistent then ISIT(A) is consistent. It is not known whether ISITR is also a consistency-preserving framework, although the fundamental difference between ISIT and ISITR is essentially that the latter treats the sentences 4-2=2, 6-3=3, 8-4=4 .... as axioms rather than as theorems.

The surprising facet is that we can prove that if ISITR is, indeed, consistency-preserving, as one might conjecture, then P $\neq$ NP.

Our talk will explain why the relationship between ISIT and ISITR is much more puzzling than one might first anticipate. It will also conjecture that ISITR is consistency preserving.


Document last modified on May 23, 1995