[FOM] Omega Consistency of Q Implies Consistency of PA?
v.yu.shavrukov at gmail.com
Wed Apr 15 16:24:08 EDT 2015
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.
More information about the FOM