# [FOM] Iterating under Con(T)

hendrik@topoi.pooq.com hendrik at topoi.pooq.com
Wed Mar 22 08:42:33 EST 2006

```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