[FOM] Interpretability in Q/CORRECTION

[Harvey Friedman]

This is a CORRECTED copy of my previous email of 12/22/04 6:39PM.

Hopefully, this will pass scrutiny, and can be compared with what Solovay
did. 

On 12/20/04 6:05 AM, "Edward T. Dean" <edean at myway.com> wrote:

> 
> I have been skimming through Edward Nelson's _Predicative Arithmetic_
> recently, and he writes (at the tail end of Ch. 15) that he does not know the
> answer to a certain compatibility problem regarding interpretability in
> Robinson arithmetic: for formulas A and B, if both Q[A] and Q[B] are
> interpretable in Q, then is Q[A,B] interpretable in Q?  I'm just wondering if
> anyone on FOM does know the answer, as the book is decently aged.
> 

The answer is no. In fact, I give a simple (and well studied) Pi01 sentence
A such that Q[A] and Q[notA] are both interpretable in Q.

THEOREM A. Let T be finitely axiomatized systems in predicate calculus with
equality. The following are equivalent.
i) EFA = ISigma0(exp) proves "T is cut free consistent";
ii) T is interpretable in Q.

We write Con*(ISigma0) for "ISigma0 is cut free consistent".

It is convenient to use Q', the obvious axiomatization of Q by a single
universal sentence, using 0,S,+,x,<=,<,=, and cutoff subtraction.

LEMMA 1. EFA proves Con*(ISigma0).

LEMMA 2. EFA proves Q + Con*(ISigma0) is cut free consistent.

Proof: Argue in EFA. Suppose 1 = 0 can be derived from Q + Con*(ISigma0) by
a cut free proof. Then 1 = 0 can be derived from Q' + Con*(ISigma0) by a cut
free proof. Hence Q' + Con*(ISigma0) is false. This contradicts Lemma 1. QED

LEMMA 3. ISigma0 does not prove Con*(ISigma0).

LEMMA 4. EFA proves the following. There is no cut free proof in ISigma0 of
Con*(ISigma0).

LEMMA 5. EFA proves that ISigma0 + Con*(ISigma0) and ISigma0 +
notCon*(ISigma0) are both cut free consistent.

THEOREM B. Q + Con*(ISigma0) and Q + notCon*(ISigma0) are both interpretable
in Q.   

By sharpening Theorem 1, we can also get

THEOREM C. ISigma0 + Con*(ISigma0) and Isigma0 + notCon*(ISigma0) are both
interpretable in Q.

Years ago, I had a series of theorems to the effect that "relative
consistency is the same as interpretability". This stuff has been published
and reworked by several authors.

I don't remember seeing this particular refinement:

THEOREM. Let S,T be finitely axiomatized systems in predicate calculus with
equality, where Q is interpretable in S. The following are equivalent.
i) EFA = ISigma0(exp) proves "if S is cut free consistent then T is cut free
consistent;
ii) T is interpretable in S.

Harvey Friedman