FOM: Consistency proofs

[wtait@ix.netcom.com]

Vaughan Pratt(3/29) wrote in response to Steel (3/25)
>I would think that in order for Cohen's argument to compete with Gentzen's
>it would need a one-paragraph summary that is as clearly motivated as
>the above.  Can someone supply this?
I have not seen the proof that Paul Cohen recently gave at Berkeley; but in the early 60's he (independently) gave a version of Ackermann's consistency proof for PA using the so-called `epsilon substitution method'---though at that time, I don't think (but I don't really remember) that Cohen gave the ordinal amnalysis necessary to obtain the proof-theoretic ordinal epsilon_0. 

In answer to John Steel's question, if that was the proof Cohen gave, it is quite different from Gentzen's. It amounts to introducing for each quantifier-free formula phi(x,y,Š,z), all of whose terms other than the distinct y, Š, z, contain x, a new *selection function* constant f for phi with the axioms (1) phi(r,s,Š,t) \implies phi(f(s,Š,t),s,Š,t) 
and (in PA) the axioms
(2)r<f(s,Š,t) \implies \neg phi(r,s,Š,t). 
So at the initial stage, we have the (quantifier-free) formulas of PA andf at the n+1st stage we have the formulas built up from the constants at the nth stage together with the selection function constants for formulas at the nth stage. Deductions in PA, as usually formalized, are transformed into deductions in the quantifier-free part of PA together with the axioms for the selection functions by successively replacing parts \exists x phi(x,s,Š,t) (with phi quantifier-free) by phi(f(s,Š,t),s,Š,t). Also, we can assume that the deduction contains no free variables. (Assume that the conclusion of the original deduction contains no quatifiers, e.g. by taking its universal closure, and then replace all of the remaining free variables in the deduction by 0.)

In a given deduction in this quantifier-free system, there will be some finite list f_1, Š, f_n of all the selection function constants occuring in the deduction, ordered so that, if f_i occurs in the formula for which f_j is the selection constant, then i<j. Thus, we may think of f_j as a functional f_j = F_j(f_1,Š,f_(j-1)) of the selection functions f_i with i<j. So we will interpret the selection constants in the deduction in such a way as to satisfy the axioms  if we solve the system of equations

(3) F_j(f_1, Š,f_(j-1))(y,Š,z) = the least x<Min{r_1,Š,r_(k_j)}phi_j(x,y,Š,z)  (j=1,Š,n)

where the r_i are all of the r occuring in axioms (1) in the deduction (for f=f_j) and the vbalue is 0 if there is no such x. Of course T_j(f_1, Š, f_n) = the least x<Min{r_1,Š,r_(k_j)} depends in general on the f_i, but only on a finite number of their values---T_j is continuous in the f_i.

Solve first for f_n by successive approximation. Set F_n^0(f_1, Š,f_(j-1))(y,Š,z) =0 and F_n^(k+1) = T_n(f_1, Š, f_n^0), as a functional of f_1, Š, f_(n-1). Note that, for any system of values of y, Š, z, and for any k, f_n^k(y,Š,z) >0 implies f_n^m(y,Š,z)=f_n^k(y,Šz) for all m>k. So f_n^*(y,Š,z) = F_n^*(f_1, Š, f_(n-1))(y,Š,z)=Lim_kf_n^k(y,Š,z) is defined and, by the continuity of T_n, satisfies (3) for j=n. Now substitute this solution in the equations (3) for j=n-1. We need only note that F_n^*(f_1, Š, f_(n-1)) is continuous in the f_i for i<n to repeat the same construction for n-1; etc.

This, as I (quite possibly mis-) remember, is essentially the argument of the MS Cohen showed me in 1963. The ordinal analysis involves showing that F_n is defined by omega-recursion, F_(n-1) by omega^omega-recursion, etc. (For my sins, I carried out the analysis in 1961-2. It appears in a paper ``The Substitution Method'', JSL 30, 1965, which I do not recommend.)

The Gentzen consistency proof is in a different direction and is best understood as showing how to transform any proof of Delta in PA into a winning strategy for player DISJ in his game G(phi) with CONJ. Delta is a finite set of sentences of PA. If Delta contains a true atomic sentence, DISJ wins. If Delta contains only false atoms, CONJ wins.  Otherwise: If any conjuctive formula (i.e. psi\wedge chi or \forall x psi(x)) occurs in Delta, CONJ must choose one and _replace_ it in Delta by a component (psi or chi in one case, psi(n) for some numeral n in the other). If no conjunctive formula occurs, then DISJ must choose a disjunctive formula (psi \vee chi or \exists x psi(x)) and _add_ one of its components to Delta. (Its not a very fair game.) In any case, if the game is not over, a new set Delta' is on the board and the game proceeds. A winning strategy for DISJ takes the form of a cut-free deduction (and every cut-free deduction transforms into a winning strategy for DISJ: It may not be one initially because there might be an inference from Gamma+psi to Gamma+phi in the deduction, where psi is a component of the disjunctive formula phi, even though Gamma contains conjunctive formulas.)

In this case, Gentzen's ordinal analysis assigns a length to the winning strategy for DISJ associated with the original deduction in PA. It is just the height of the cut-free proof tree.

In 1963, when Cohen showed me his proof, I had already concluded (to my sorrow) that the substitution method would not work for second-order arithmetic because, in that case, T_j (now of type 3) is not in general continuous in the f_i (now possibly of type 2). (Ackerman had published a `consistency proof' for second-order arithmetic using the substitution method; but von Neumann found an error in it.) So, if Cohen's new analysis of PA is like his original one, I would dearly like to see the details of its extension to second-order, much less to set theory.

Bill Tait