[FOM] Interpretability in Q/CORRECTION
Harvey Friedman
friedman at math.ohio-state.edu
Thu Dec 23 08:12:28 EST 2004
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
More information about the FOM
mailing list