[FOM] Omega Consistency of Q Implies Consistency of PA?

[V.Yu. Shavrukov]

On Apr 15, 2015, at 16:49, Richard Heck <richard_heck at brown.edu> wrote:
> Feferman mentions in a footnote in "Arithmetization" that Kreisel showed that the omega consistency of Q finitistically implies the consistency of PA. Unfortunately, the paper to which he refers seems to be hard to get. Can anyone explain the proof of this?
> 
> Richard Heck

First, one should note that there is more than one formalization of "the omega-consistency of Q" — there is the global version

(Aφ) [ (Ax) [Q] φ(x) —> ¬ [Q] (Ex) ¬ φ(x) ],

the corresponding local version (separate sentences for each φ(.)), and there may be more — one of Smoryński's papers has an overview.


I am going to use the above global version recalling that

(*)  Q + induction is equivalent to PA

The following argument works under the assumption that for each theorem of PA,  Q + a single instance of induction schema suffices.  This probably is not true (there is however a standardly finite number N such that N instances always suffice — I am pretty sure  N ≤ 100), but the argument can be modified to work with finite disjunctions of negations of induction instances.

Reason finitistically (IΔ₀+exp, I guess):

If PA is inconsistent then then by (*)+assumption,  Q  proves the negation of some induction axiom:

[Q] (Ey) ¬ (Ap)(φ(p,0) & (Ax)(φ(p,x) —> φ(p,x+1)) —> φ(p,y))

Yet for each n,  [Q] (Ap)(φ(p,0) & (Ax)(φ(p,x) —> φ(p,x+1)) —> φ(p,n)), 

this is seen by (Δ₀(exp)-)induction on  n  [if you keep around an exp-term for the corresponding Q-proof rather than just induct existence of a proof.  The Q-proof itself can in fact be a proof in pure predicate calculus.]

Thus  Q  is not  ω-consistent.


best regards,
Volodya Shavrukov