[FOM] Consistency of formal systems

Richard Zach rzach at ucalgary.ca
Sat Jun 14 17:05:23 EDT 2003

To elaborate on Bill's response:

> On Friday, June 13, 2003, at 09:45  AM, Matt Insall wrote:
> <snip>
>
>> 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.
>
The problem is here:

>> 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).
>
You can only "continue the procedure" along constructive ordinals (ie,
well-founded orderings which are defined by pr. formulas).  If you don't
have such a definition of the ordinals, you can't write down the formula
that says "x is an axiom of S(\alpha)" where \alpha is any infinite
ordinal. The constructive ordinals O are all, of course, countable, and
indeed bounded by a countable ordinal ("the first non-constructive
ordinal, \omega_1^C(hurch)K(leene)"). If you made all this precise,
you'd never leave the countable.

Ordinal logics were first discussed by Turing, and then by Feferman.
Instead of adding A_q, they considered adding the consistency statement
or reflection principles.  The main results are that if you add Con and
iterate through O (ie, all constructive ordinals), you get all true
\Pi_1 sentences of arithmetic; same if you add local reflection
(Pr(\phi) -> \phi for all sentences \phi). If you iterate adding global
reflection ((\forall x)Pr(\phi(x)) -> (\forall x)\phi(x) for all
formulas \phi(x)) you get all true sentences of arithmetic.  In fact,
it's enough to iterate up to \omega+1 for the former result, and through
\omega^{\omega^\omega} for the second.  Of course, all this doesn't
answer the question you might now have: what happens when you keep

References:

@ARTICLE{Turing:39,
author = {Alan M. Turing},
year = 1939,
title = {Systems of logic based on ordinals},
journal = {Proc. London Math. Soc., ser. 2},
volume = 45,
pages = {161--228}
}

@ARTICLE{Feferman:62,
author = {Solomon Feferman},
year = 1962,
title = {Transfinite recursive progressions of axiomatic theories},
journal = JSYML,
volume = 27,
pages = {259--316}
}

@ARTICLE{Schmerl:82,
author = {Ulf R. Schmerl},
year = 1982,
title = {Iterated reflection principles and the $\omega$-rule},
journal = JSYML,
volume = 47,
pages = {721--733}
}

Yours,
Richard
--
Richard Zach ...... http://www.ucalgary.ca/~rzach/
Assistant  Professor,   Department  of  Philosophy
University of Calgary, Calgary, AB T2N 1N4, Canada