[FOM] Consistency of formal systems

[William Tait]

The problem surely is that, even going through only the constructive 
ordinals, you need to show at limit ordinals that the union of the 
theories that you have obtained at smaller ordinals is a theory to 
which Rosser's theorem applies. Turing, Feferman and Fenstad have 
written on such hierarchies of theories; but I don't remember the 
details. I think that Feferman gave a bound on how high such a 
hierarchy could go and then Fenstad improved on it (?)

Feferman JSL 27 (1962): 259-316.

Bill Tait


On Friday, June 13, 2003, at 09:45  AM, Matt Insall wrote:

> On another list, a friend, Hitoshi Kitada, posted the following 
> argument,
> which I post here with his permission.  My question to this list is 
> where
> did it go wrong?  I think I know where there is a mistake, but I have
> difficulty explaining why.  Can someone help me explain where the 
> problem
> is?  (After the quote, I will state the line at which I think there is
> a first error.
>
>
>
> <<Begin Quote>>
> Consider Rosser's formula A_q(q), which means
>
> ``To any proof of A_q(q), there exists a proof of ~A_q(q) with an equal
> or lesser Goedel number." ( ~ denotes negation )
>
> Then one can prove that, if the formal system S(0) of number theory is
> consistent, then neither A_q(q) nor ~A_q(q) is provable.
>
> Add one of A_q(q) or ~A_q(q) as a new axiom of S(0), and name it S(1).
> Then by Rosser's theorem, S(1) is consistent, if S(0) is consistent.
>
> Let A_q(1)(q(1)) be the new Rosser's formula having the same meaning as
> above, but now in S(1). Then arguing similarly we have that neither
> A_q(1)(q(1)) nor ~A_q(1)(q(1)) is provable in S(1).
>
> Continue this procedure, and construct a system S(omega) that has
> countably infinite new axioms having either form A_q(n)(q(n)) or
> ~A_q(n)(q(n)) for n > or = 0.
>
> Then S(pmega) is consistent. Further with some reasoning we can show
> that the Rosser's formula A_q(omega)(q(omega)) in S(omega) is also
> primitive recursively defined, so Goedel number q(omega) is
> well-defined.
>
> Continue this procedure transfinite inductively to reach the
> cardinality of continuum. We do not lose the primitive recursive
> definition of Rosser's formula at each step. But at some step we have 
> to
> reach the continuum if we assume something like continuum hypothesis.
> Then we must have exhausted all of the formulas of S(0) at some step
> with an ordinal beta before we reach the continuum. At that beta, we
> have an inconsistent S(beta).
>
> We started with an assumption that S(0) is consistent, and at each step
> we had a consistent system S(alpha), so the above-obtained S(beta) must
> be consistent in this construction. This is a contradiction.
>
> Then by reductio ad absurdum, one has that the first assumption that 
> S(0)
> is consistent is wrong, and he has that the number theory S(0) is
> inconsistent.
>
>
> What was wrong? If the argument is not deceiving us, a possible cause 
> of
> the contradiction is continuum hypothesis or an equivalent: for some
> ordinal alpha, the cardinality of alpha is equal to the continuum
> cardinality.
>
> If this is the cause of the contradiction, we seem to have to 
> reconsider
> ZFC.
> <<End Quote>>
>
> The place I first notice what I think is an error is
> ``Then we must have exhausted all of the formulas of S(0) at some step
> with an ordinal beta before we reach the continuum. At that beta, we
> have an inconsistent S(beta).''
>
> I say this assumes that at each step, we not only add one formula,
> but we also deductively close the result.  Otherwise, it is conceivable
> that after some beta, the tower of S(alphas) stabilizes (i.e. for
> each alpha and gamma >= beta, S(alpha)=S(gamma)).  But in fact, I am
> not convinced that this makes some S(beta) inconsistent.  I believe 
> that
> at some beta, S(beta) must be complete and consistent, and the least
> such beta must be a special type of denumerable limit ordinal.
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>