[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 
adding A_q?


  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}

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

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

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

More information about the FOM mailing list