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.


dimacs-www@dimacs.rutgers.edu
Document last modified on May 23, 1995