DIMACS Seminar


Self-Verifying Axiom Systems and the Polynomial Hierarchy


Dan Willard
SUNY - Albany


Seminar Room 431, CoRE Building, Busch Campus
Rutgers University


11:00 AM
Monday, June 5, 1995


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