[FOM] Iterating under Con(T)

[Richard Heck]

A student in an advanced logic course recently asked me, "What happens
if we start with PA and keep adding consistency statements forever?" I
had a few things to say, but it occurred to me that I don't actually
know the answer to this question, so I thought someone here might be
willing to let me know what it is I don't know. The question is
obviously close to ones that have been widely studied, but I'm no expert
on iterated sequences of theories and ordinal notations and such.

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
This sequence is monotonic and so there is a fixed point, T. It seems we
can show by induction that T is consistent and, indeed, true in the
standard model. It is also clear that T is not axiomatizable, since T =
T + Con(T), hence T proves Con(T). Question: What is T? Is T true
arithmetic? Other question: What can we say about the axiomatizable
theories in this sequence? Are there non-axiomatizable theories below T?
If so, what is the first non-axiomatizable theory in the sequence? Final
question: Is there something general that can be said about such
sequences? I.e., what happens if we start instead with Q or Z or ZFC or
who knows what else?

Cheers,
Richard

-- 
==================================================================
Richard G Heck, Jr
Professor of Philosophy
Brown University
http://bobjweil.com/heck/
==================================================================
Get my public key from http://sks.keyserver.penguin.de
Hash: 0x1DE91F1E66FFBDEC
Learn how to sign your email using Thunderbird and GnuPG at:
http://dudu.dyn.2-h.org/nist/gpg-enigmail-howto