# 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