Ordinals connected with formal theories for transfinitely iterated inductive definitions
Wolfram Pohlers · Journal of Symbolic Logic · 1978
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.