Theories of iterated inductive definitions explained

In set theory and logic, Buchholz's ID hierarchy is a hierarchy of subsystems of first-order arithmetic. The systems/theories

ID _{\nu} are referred to as "the formal theories of ν-times iterated inductive definitions". ID_ν extends PA by ν iterated least fixed points of monotone operators.

Definition

Original definition

The formal theory ID_ω (and ID_ν in general) is an extension of Peano Arithmetic, formulated in the language L_ID, by the following axioms:^[1]

\forall y \forall x ( ak{M} ^{ak{M}} _{y,} x) → x \in P ^{ak{M}} _{y)} \forall y (\forall x ( ak{M} _{y(F,} x) → F(x)) → \forall x (x \in P ^{ak{M}} _{y} → F(x))) for every L_ID-formula F(x)\forall y \forall x _{0} \forall x ^{ak{M}} _{<y} x _{0x} _{1} \leftrightarrow x _{0} < y \land x _{1} \in P ^{ak{M}} _{x _{0}} )

The theory ID_ν with ν ≠ ω is defined as:

\forall y \forall x (Z ^{ak{M}} _{y,} x) → x \in P ^{ak{M}} _{y)} \forall x ( ak{M} _{u(F,} x) → F(x)) → \forall x (P ^{ak{M}} _{ux} → F(x)) for every L_ID-formula F(x) and each u < ν\forall y \forall x _{0} \forall x ^{ak{M}} _{<y} x _{0x} _{1} \leftrightarrow x _{0} < y \land x _{1} \in P ^{ak{M}} _{x _{0}} )

Explanation / alternate definition

ID₁

A set

I \subseteq \N is called inductively defined if for some monotonic operator \Gamma: P(N) → P(N) , LFP(\Gamma) = I , where LFP(f) denotes the least fixed point of f . The language of ID₁, L _{ID _{1}} , is obtained from that of first-order number theory, L _{\N} , by the addition of a set (or predicate) constant I_A for every X-positive formula A(X, x) in L_N[X] that only contains X (a new set variable) and x (a number variable) as free variables. The term X-positive means that X only occurs positively in A (X is never on the left of an implication). We allow ourselves a bit of set-theoretic notation:F(x) = \{x \in N \mid F(x)\} s \in F means F(s)

• For two formulas

F and G , F \subseteq G means \forall x F(x) → G(x) .

Then ID₁ contains the axioms of first-order number theory (PA) with the induction scheme extended to the new language as well as these axioms:

(ID ^{1 :} _{1 )} A(I _{A)} \subseteq I _{A} (ID ^{2 :} _{1 )} A(F) \subseteq F → I _{A} \subseteq F

Where

F(x) ranges over all L _{ID _{1}} formulas.

Note that

(ID ^{1} _{1 )} expresses that I _{A}  is closed under the arithmetically definable set operator \Gamma _{A(S)} = \{x \in \N \mid \N \models A(S, x)\} , while (ID ^{2} _{1 )}  expresses that I _{A}  is the least such (at least among sets definable in L _{ID _{1}} ).

Thus,

I _{A}  is meant to be the least pre-fixed-point, and hence the least fixed point of the operator \Gamma _{A} .

ID_ν

To define the system of ν-times iterated inductive definitions, where ν is an ordinal, let

\prec  be a primitive recursive well-ordering of order type ν. We use Greek letters to denote elements of the field of \prec . The language of ID_ν, L _{ID _{\nu}} is obtained from L _{\N} by the addition of a binary predicate constant J_A for every X-positive L _{\N[X,} Y] formula A(X, Y, \mu, x) that contains at most the shown free variables, where X is again a unary (set) variable, and Y is a fresh binary predicate variable. We write x \in J ^{\mu} _{A} instead of J _{A(\mu,} x) , thinking of x as a distinguished variable in the latter formula.

The system ID_ν is now obtained from the system of first-order number theory (PA) by expanding the induction scheme to the new language and adding the scheme

(TI _{\nu):} TI(\prec, F) expressing transfinite induction along \prec for an arbitrary L _{ID _{\nu}}  formula F  as well as the axioms:(ID ^{1 :} _{\nu)} \forall \mu \prec \nu; A ^{\mu(J} ^{\mu} ^{A)} \subseteq J ^{\mu} _{A} (ID ^{2 :} _{\nu)} \forall \mu \prec \nu; A ^{\mu(F)} \subseteq F → J ^{\mu} _{A} \subseteq F

where

F(x)  is an arbitrary L _{ID _{\nu}}  formula. In (ID ^{1} _{\nu)}  and (ID ^{2} _{\nu)}  we used the abbreviation A ^{\mu(F)}  for the formula A(F, ( λ \gamma y; \gamma \prec \mu \land y \in J ^{\gamma} _{A),} \mu, x) , where x  is the distinguished variable. We see that these express that each J ^{\mu} _{A} , for \mu \prec \nu , is the least fixed point (among definable sets) for the operator \Gamma ^{\mu} _{A(S)} = \{n \in \N | (\N, (J ^{\gamma} _{A)} _{\gamma} \} . Note how all the previous sets J ^{\gamma} _{A} , for \gamma \prec \mu , are used as parameters.

We then define $ID\_\; =\; \backslash bigcup\; \_ID\_\backslash xi$.

Variants

\widehat{ ID }_\nu - \widehat{ ID }_\nu is a weakened version of ID _{\nu} . In the system of \widehat{ ID }_\nu, a set I \subseteq \N is instead called inductively defined if for some monotonic operator \Gamma: P(N) → P(N) , I is a fixed point of \Gamma , rather than the least fixed point. This subtle difference makes the system significantly weaker: PTO(\widehat{ ID }_1) = \psi(\Omega^), while PTO( ID _{1)} = \psi(\varepsilon _{\Omega+1} ) .ID _{\nu\#} is \widehat{ ID }_\nu weakened even further. In ID _{\nu\#} , not only does it use fixed points rather than least fixed points, and has induction only for positive formulas. This once again subtle difference makes the system even weaker: PTO( ID _{1\#)} = \psi(\Omega ^{\omega)} , while PTO(\widehat{ ID }_1) = \psi(\Omega^).W-ID _{\nu} is the weakest of all variants of ID _{\nu} , based on W-types. The amount of weakening compared to regular iterated inductive definitions is identical to removing bar induction given a certain subsystem of second-order arithmetic. PTO( W-ID _{1)} = \psi _{0(\Omega x \omega)} , while PTO( ID _{1)} = \psi(\varepsilon _{\Omega+1} ) .U(ID _{\nu)} is an "unfolding" strengthening of ID _{\nu} . It is not exactly a first-order arithmetic system, but captures what one can get by predicative reasoning based on ν-times iterated generalized inductive definitions. The amount of increase in strength is identical to the increase from \varepsilon _{0} to \Gamma _{0} : PTO( ID _{1)} = \psi(\varepsilon _{\Omega+1} ) , while PTO( U(ID _{1))} = \psi(\Gamma _{\Omega+1} ) .

Results

• Let ν > 0. If a ∈ T₀ contains no symbol D_μ with ν < μ, then "a ∈ W₀" is provable in ID_ν.
• ID_ω is contained in

\Pi ^{1} _{1} - CA + BI .

• If a

\Pi ^{0} _{2} -sentence \forall x \exists y \varphi(x, y) (\varphi \in \Sigma ^{0} _{1 )} is provable in ID_ν, then there exists p \in N such that \forall n \geq p \exists k < H _{D ^{n} _{\nu 0}} ( 1 ) \varphi(n, k) .

• If the sentence A is provable in ID_ν for all ν < ω, then there exists k ∈ N such that

\vdash ^{D ^{k} _{\nu 0}} _{k} A ^{N} .

Proof-theoretic ordinals

• The proof-theoretic ordinal of ID_<ν is equal to

\psi _{0(\Omega} _{\nu)} .

• The proof-theoretic ordinal of ID_ν is equal to

\psi _{0(\varepsilon} ^{\Omega _{\nu+1}} ) = \psi _{0(\Omega} _{\nu+1} ) .

• The proof-theoretic ordinal of

\widehat{ID} _{<\omega} is equal to \Gamma _{0} .

• The proof-theoretic ordinal of

\widehat{ID} _{\nu} for \nu < \omega is equal to \varphi(\varphi(\nu, 0 ), 0 ) .

• The proof-theoretic ordinal of

\widehat{ID} _{\varphi(\alpha,} is equal to \varphi( 1 , 0 , \varphi(\alpha +1 , \beta -1 )) .

• The proof-theoretic ordinal of

\widehat{ID} _{<\varphi(0,} for \alpha > 1 is equal to \varphi( 1 , \alpha, 0 ) .

• The proof-theoretic ordinal of

\widehat{ID} _{<\nu} for \nu \geq \varepsilon _{0} is equal to \varphi( 1 , \nu, 0 ) .

• The proof-theoretic ordinal of

ID _{\nu\#} is equal to \varphi(\omega ^{\nu,} 0 ) .

• The proof-theoretic ordinal of

ID _{<\nu} \# is equal to \varphi( 0 , \omega ^{\nu+1} ) .

• The proof-theoretic ordinal of

W rm{-}ID _{\varphi(\alpha,} is equal to \psi _{0(\Omega} _{\varphi(\alpha,} x \varphi(\alpha +1 , \beta -1 )) .

• The proof-theoretic ordinal of

W rm{-}ID _{<\varphi(\alpha,} is equal to \psi _{0(\varphi(\alpha+1,} \beta -1 ) ^{\Omega _{\varphi(\alpha,} +1} ) .

• The proof-theoretic ordinal of

U(ID _{\nu)} is equal to \psi _{0(\varphi(\nu,} 0 , \Omega +1 )) .

• The proof-theoretic ordinal of

U(ID _{<\nu} ) is equal to \psi ^{\Omega + \varphi(\nu, 0 , \Omega)} _{0 (\Omega} ) .

• The proof-theoretic ordinal of ID₁ (the Bachmann-Howard ordinal) is also the proof-theoretic ordinal of

KP , KP\omega , CZF and ML _{1} V .

• The proof-theoretic ordinal of W-ID_ω (

\psi _{0(\Omega} _{\omega\varepsilon} _{0)} ) is also the proof-theoretic ordinal of W-KPI .

• The proof-theoretic ordinal of ID_ω (the Takeuti-Feferman-Buchholz ordinal) is also the proof-theoretic ordinal of

KPI , \Pi ^{1} _{1} - CA + BI and \Delta ^{1} _{2} - CA + BI .

• The proof-theoretic ordinal of ID_<ω^ω (

\psi _{0(\Omega} ^{\omega ^{\omega}} ) ) is also the proof-theoretic ordinal of \Delta ^{1} _{2} - CR .

• The proof-theoretic ordinal of ID_<ε0 (

\psi _{0(\Omega} ^{\varepsilon _{0}} ) ) is also the proof-theoretic ordinal of \Delta ^{1} _{2} - CA and \Sigma ^{1} _{2} - AC .

References

• An independence result for \Pi ^{1} _{1} - CA + BI
• Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies
• Iterated inductive definitions in nLab
• Lemma for the intuitionistic theory of iterated inductive definitions
• Iterated Inductive Definitions and \Sigma ^{1} _{2} - AC
• Large countable ordinals and numbers in Agda
• Ordinal analysis in nLab

Notes and References

1. W. Buchholz, "An Independence Result for (\Pi ^{1} _{1 rm{-CA}) rm{+BI}} ", Annals of Pure and Applied Logic vol. 33 (1987).