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 IDN 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.
Ordinal analysis of non-monotone Π10-definable inductive definitions
