[FOM] Iterating under Con(T)

[Dmytro Taranovsky]

Richard Heck wrote: 
> A student in an advanced logic course recently asked me, "What happens
> if we start with PA and keep adding consistency statements forever?"
> To make the question more precise, define the following sequence of
> theories by transfinite recursion:
> T_0 = PA
> T_{k+1} = T_k + Con(T_k)
> T_l = \cup_{k<l} T_k, for l a limit

The problem here is passing at the limit steps from \cup_{k<l} T_k to (a
code for) a recursively enumerable function enumerating \cup_{k<l} T_k.
One needs the code to define Con(T_l).

If the transitions are done naturally, then for every natural theory S
(substantially) stronger than PA, a Pi-0-1 statement is provable in S
iff it is provable in T_alpha where alpha is the proof-theoretical
ordinal of S.  The sequence ends at the first non-recursive ordinal;
T_{omega_1^CK} proves all true Pi-0-1 statements.

It is not known if the transition can be done naturally.  It can be done
naturally for ordinals within natural (recursive) ordinal notations.
>From the hyperjump of zero, it is also possible to define a sequence of
Con(T)s satisfying basic formal conditions of naturalness, including
length omega_1^CK, monotonicity, recursiveness of every proper initial
subsequence of Ts, and Pi-0-1 completeness of T_{omega_1^CK}.

If the transitions are not done naturally, then the sequence may break
down by becoming non-recursive (or even proving all true Pi-0-1
statements) at the stage omega*omega.  I think it is also possible to
reach omega_1^CK without ever proving Con(PA + 1-Con(PA)).

The consistency sequence can just as well be defined using Exponential
Function Arithmetic in place of Peano Arithmetic.  

It is more common to construct the sequence at the Pi-0-2 or Pi-1-1
level.  The reason is that at successor steps one does not need
complicated consistency statements.  One can simply replace f(n) with
f(n)+1 for the Pi-0-2 statement "f is total" and increases the rank of R
by 1 for the Pi-1-1 statement "R is well-founded".  The above discussion
also applies to construction of such sequences.

Dmytro Taranovsky
http://web.mit.edu/dmytro/www/main.htm