 Thus one might try to address the incompleteness of T by forming a sequence of theories \(\bT=\bT_0\subset \bT_1\subset\bT_2\subset\ldots\) where \(\bT_{i+1}=\bT_i'\) and to continue this into the transfinite. The latter can be achieved by letting \(\bT_{\lambda}=\bigcup_{\alpha&lt;\lambda}\bT_{\alpha}\) for limit ordinals λ and \(\bT_{\alpha+1}=\bT_{\alpha}'\) for successor ordinals \(\alpha+1\). However, the consistency statement for \(\bT_{\lambda}\), thus the provability predicate for the theory, has to be expressed in the language of \(\bT_{\lambda}\), and one cannot simply use set theoretic ordinals. Furthermore, the extensions of T are all supposed to be formal theories, i.e., the axioms have to be enumerable by recursive functions. To deal with both issues at once, one has to deal with ordinals in an effective way.