[FOM] Iterating under Con(T)

[hendrik@topoi.pooq.com]

On Fri, Mar 10, 2006 at 02:46:46PM -0500, Richard Heck wrote:
> joeshipman at aol.com wrote:
> > Heck:
> >> 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
> > ...[S]houldn't you be closing each step under logical implication? 
 Or is there some other worry I've missed?

There might be multiple Con(T_k) at a limit ordinal k, from different 
descriptions of the set of formulas in the theory at that point.  In 
this case, you might need dependent choice to continue your 
construction.  It's not clear to me to what extent you want to perform 
your construction within PA.

-- hendrik