Ordinals Connected with Formal Theories for Transfinitely Iterated Inductive Definitions

Let Th be a formal theory extending number theory. Call an ordinal ξ provable in Th if there is a primitive recursive ordering which can be proved in Th to be a wellordering and whose order type is > ξ. One may define the ordinal ∣ Th ∣ of Th to be the least ordinal which is not provable in Th. By [3] and [12] we get , where ID N is the formal theory for N -times iterated inductive definitions. We will generalize this result not only to the case of transfinite iterations but also to a more general notion of ‘the ordinal of a theory’. For an X-positive arithmetic formula [X, x ] there is a natural norm ∣ x ∣: = μξ ( x ∈ I ξ ), where I ξ is defined as { x : [∪ μ ξ I μ , x ]} by recursion on ξ (cf. [7], [17]). By P we denote the least fixed point of [ X , x ]. Then P = ∪ ξ ξ holds. If Th allows the formation of P , we get the canonical definitions ∥Th( )∥ = sup{∣ x ∣ + 1: Th ⊢ x ∈ P } and ∥Th∥ = sup{∥Th( )∥: P is definable in Th} (cf. [17]). If ≺ is any primitive recursive ordering define Q ≺[ X,x] as the formula ∀ y ( y ≺ x → y ∈ X ) and ∣ x ∣≺:= ∣ x ∣ O ≺. Then ∣ x ∣≺ turns out to be the order type of the ≺ -predecessors of x and P is the accessible part of ≺. So Th ⊢ x ∈ P implies the provability of ∣ x ∣≺ in Th.