Theories of iterated inductive definitions

In set theory and logic, Buchholz's ID hierarchy is a hierarchy of subsystems of first-order arithmetic. The systems/theories ${\displaystyle 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]

• ${\displaystyle \forall y\forall x({\mathfrak {M}}_{y}(P_{y}^{\mathfrak {M}},x)\rightarrow x\in P_{y}^{\mathfrak {M}})}$
• ${\displaystyle \forall y(\forall x({\mathfrak {M}}_{y}(F,x)\rightarrow F(x))\rightarrow \forall x(x\in P_{y}^{\mathfrak {M}}\rightarrow F(x)))}$ for every L_ID-formula F(x)
• ${\displaystyle \forall y\forall x_{0}\forall x_{1}(P_{<y}^{\mathfrak {M}}x_{0}x_{1}\leftrightarrow x_{0}<y\land x_{1}\in P_{x_{0}}^{\mathfrak {M}})}$

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

• ${\displaystyle \forall y\forall x(Z_{y}(P_{y}^{\mathfrak {M}},x)\rightarrow x\in P_{y}^{\mathfrak {M}})}$
• ${\displaystyle \forall x({\mathfrak {M}}_{u}(F,x)\rightarrow F(x))\rightarrow \forall x(P_{u}^{\mathfrak {M}}x\rightarrow F(x))}$ for every L_ID-formula F(x) and each u < ν
• ${\displaystyle \forall y\forall x_{0}\forall x_{1}(P_{<y}^{\mathfrak {M}}x_{0}x_{1}\leftrightarrow x_{0}<y\land x_{1}\in P_{x_{0}}^{\mathfrak {M}})}$

Explanation / alternate definition

ID₁

A set ${\displaystyle I\subseteq \mathbb {N} }$ is called inductively defined if for some monotonic operator ${\displaystyle \Gamma :P(N)\rightarrow P(N)}$, ${\displaystyle LFP(\Gamma )=I}$, where ${\displaystyle LFP(f)}$ denotes the least fixed point of ${\displaystyle f}$. The language of ID₁, ${\displaystyle L_{ID_{1}}}$, is obtained from that of first-order number theory, ${\displaystyle L_{\mathbb {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:

• ${\displaystyle F(x)=\{x\in N\mid F(x)\}}$
• ${\displaystyle s\in F}$ means ${\displaystyle F(s)}$
• For two formulas ${\displaystyle F}$ and ${\displaystyle G}$, ${\displaystyle F\subseteq G}$ means ${\displaystyle \forall xF(x)\rightarrow 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:

• ${\displaystyle (ID_{1})^{1}:A(I_{A})\subseteq I_{A}}$
• ${\displaystyle (ID_{1})^{2}:A(F)\subseteq F\rightarrow I_{A}\subseteq F}$

Where ${\displaystyle F(x)}$ ranges over all ${\displaystyle L_{ID_{1}}}$ formulas.

Note that ${\displaystyle (ID_{1})^{1}}$ expresses that ${\displaystyle I_{A}}$ is closed under the arithmetically definable set operator ${\displaystyle \Gamma _{A}(S)=\{x\in \mathbb {N} \mid \mathbb {N} \models A(S,x)\}}$, while ${\displaystyle (ID_{1})^{2}}$ expresses that ${\displaystyle I_{A}}$ is the least such (at least among sets definable in ${\displaystyle L_{ID_{1}}}$).

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

ID_ν

To define the system of ν-times iterated inductive definitions, where ν is an ordinal, let ${\displaystyle \prec }$ be a primitive recursive well-ordering of order type ν. We use Greek letters to denote elements of the field of ${\displaystyle \prec }$. The language of ID_ν, ${\displaystyle L_{ID_{\nu }}}$ is obtained from ${\displaystyle L_{\mathbb {N} }}$ by the addition of a binary predicate constant J_A for every X-positive ${\displaystyle L_{\mathbb {N} }[X,Y]}$ formula ${\displaystyle 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 ${\displaystyle x\in J_{A}^{\mu }}$ instead of ${\displaystyle 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 ${\displaystyle (TI_{\nu }):TI(\prec ,F)}$ expressing transfinite induction along ${\displaystyle \prec }$ for an arbitrary ${\displaystyle L_{ID_{\nu }}}$ formula ${\displaystyle F}$ as well as the axioms:

• ${\displaystyle (ID_{\nu })^{1}:\forall \mu \prec \nu ;A^{\mu }(J_{A}^{\mu })\subseteq J_{A}^{\mu }}$
• ${\displaystyle (ID_{\nu })^{2}:\forall \mu \prec \nu ;A^{\mu }(F)\subseteq F\rightarrow J_{A}^{\mu }\subseteq F}$

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

We then define ${\textstyle ID_{\prec \nu }=\bigcup _{\xi \prec \nu }ID_{\xi }}$.

Variants

${\displaystyle {\widehat {\mathsf {ID}}}_{\nu }}$ - ${\displaystyle {\widehat {\mathsf {ID}}}_{\nu }}$ is a weakened version of ${\displaystyle {\mathsf {ID}}_{\nu }}$. In the system of ${\displaystyle {\widehat {\mathsf {ID}}}_{\nu }}$, a set ${\displaystyle I\subseteq \mathbb {N} }$ is instead called inductively defined if for some monotonic operator ${\displaystyle \Gamma :P(N)\rightarrow P(N)}$, ${\displaystyle I}$ is a fixed point of ${\displaystyle \Gamma }$, rather than the least fixed point. This subtle difference makes the system significantly weaker: ${\displaystyle PTO({\widehat {\mathsf {ID}}}_{1})=\psi (\Omega ^{\varepsilon _{0}})}$, while ${\displaystyle PTO({\mathsf {ID}}_{1})=\psi (\varepsilon _{\Omega +1})}$.

${\displaystyle {\mathsf {ID}}_{\nu }\#}$ is ${\displaystyle {\widehat {\mathsf {ID}}}_{\nu }}$ weakened even further. In ${\displaystyle {\mathsf {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: ${\displaystyle PTO({\mathsf {ID}}_{1}\#)=\psi (\Omega ^{\omega })}$, while ${\displaystyle PTO({\widehat {\mathsf {ID}}}_{1})=\psi (\Omega ^{\varepsilon _{0}})}$.

${\displaystyle {\mathsf {W-ID}}_{\nu }}$ is the weakest of all variants of ${\displaystyle {\mathsf {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. ${\displaystyle PTO({\mathsf {W-ID}}_{1})=\psi _{0}(\Omega \times \omega )}$, while ${\displaystyle PTO({\mathsf {ID}}_{1})=\psi (\varepsilon _{\Omega +1})}$.

${\displaystyle {\mathsf {U(ID}}_{\nu }{\mathsf {)}}}$ is an "unfolding" strengthening of ${\displaystyle {\mathsf {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 ${\displaystyle \varepsilon _{0}}$ to ${\displaystyle \Gamma _{0}}$: ${\displaystyle PTO({\mathsf {ID}}_{1})=\psi (\varepsilon _{\Omega +1})}$, while ${\displaystyle PTO({\mathsf {U(ID}}_{1}{\mathsf {)}})=\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 ${\displaystyle \Pi _{1}^{1}-CA+BI}$.
• If a ${\displaystyle \Pi _{2}^{0}}$-sentence ${\displaystyle \forall x\exists y\varphi (x,y)(\varphi \in \Sigma _{1}^{0})}$ is provable in ID_ν, then there exists ${\displaystyle p\in N}$ such that ${\displaystyle \forall n\geq p\exists k<H_{D_{0}D_{\nu }^{n}0}(1)\varphi (n,k)}$.
• If the sentence A is provable in ID_ν for all ν < ω, then there exists k ∈ N such that ${\displaystyle \vdash _{k}^{D_{\nu }^{k}0}A^{N}}$.

Proof-theoretic ordinals

• The proof-theoretic ordinal of ID_<ν is equal to ${\displaystyle \psi _{0}(\Omega _{\nu })}$.
• The proof-theoretic ordinal of ID_ν is equal to ${\displaystyle \psi _{0}(\varepsilon _{\Omega _{\nu }+1})=\psi _{0}(\Omega _{\nu +1})}$ .
• The proof-theoretic ordinal of ${\displaystyle {\widehat {ID}}_{<\omega }}$ is equal to ${\displaystyle \Gamma _{0}}$.
• The proof-theoretic ordinal of ${\displaystyle {\widehat {ID}}_{\nu }}$ for ${\displaystyle \nu <\omega }$ is equal to ${\displaystyle \varphi (\varphi (\nu ,0),0)}$.
• The proof-theoretic ordinal of ${\displaystyle {\widehat {ID}}_{\varphi (\alpha ,\beta )}}$ is equal to ${\displaystyle \varphi (1,0,\varphi (\alpha +1,\beta -1))}$.
• The proof-theoretic ordinal of ${\displaystyle {\widehat {ID}}_{<\varphi (0,\alpha )}}$ for ${\displaystyle \alpha >1}$ is equal to ${\displaystyle \varphi (1,\alpha ,0)}$.
• The proof-theoretic ordinal of ${\displaystyle {\widehat {ID}}_{<\nu }}$ for ${\displaystyle \nu \geq \varepsilon _{0}}$ is equal to ${\displaystyle \varphi (1,\nu ,0)}$.
• The proof-theoretic ordinal of ${\displaystyle ID_{\nu }\#}$ is equal to ${\displaystyle \varphi (\omega ^{\nu },0)}$.
• The proof-theoretic ordinal of ${\displaystyle ID_{<\nu }\#}$ is equal to ${\displaystyle \varphi (0,\omega ^{\nu +1})}$.
• The proof-theoretic ordinal of ${\displaystyle W{\textrm {-}}ID_{\varphi (\alpha ,\beta )}}$ is equal to ${\displaystyle \psi _{0}(\Omega _{\varphi (\alpha ,\beta )}\times \varphi (\alpha +1,\beta -1))}$.
• The proof-theoretic ordinal of ${\displaystyle W{\textrm {-}}ID_{<\varphi (\alpha ,\beta )}}$ is equal to ${\displaystyle \psi _{0}(\varphi (\alpha +1,\beta -1)^{\Omega _{\varphi (\alpha ,\beta -1)}+1})}$.
• The proof-theoretic ordinal of ${\displaystyle U(ID_{\nu })}$ is equal to ${\displaystyle \psi _{0}(\varphi (\nu ,0,\Omega +1))}$.
• The proof-theoretic ordinal of ${\displaystyle U(ID_{<\nu })}$ is equal to ${\displaystyle \psi _{0}(\Omega ^{\Omega +\varphi (\nu ,0,\Omega )})}$.
• The proof-theoretic ordinal of ID₁ (the Bachmann-Howard ordinal) is also the proof-theoretic ordinal of ${\displaystyle {\mathsf {KP}}}$, ${\displaystyle {\mathsf {KP\omega }}}$, ${\displaystyle {\mathsf {CZF}}}$ and ${\displaystyle {\mathsf {ML_{1}V}}}$.
• The proof-theoretic ordinal of W-ID_ω (${\displaystyle \psi _{0}(\Omega _{\omega }\varepsilon _{0})}$) is also the proof-theoretic ordinal of ${\displaystyle {\mathsf {W-KPI}}}$.
• The proof-theoretic ordinal of ID_ω (the Takeuti-Feferman-Buchholz ordinal) is also the proof-theoretic ordinal of ${\displaystyle {\mathsf {KPI}}}$, ${\displaystyle \Pi _{1}^{1}-{\mathsf {CA}}+{\mathsf {BI}}}$ and ${\displaystyle \Delta _{2}^{1}-{\mathsf {CA}}+{\mathsf {BI}}}$.
• The proof-theoretic ordinal of ID_<ω^ω (${\displaystyle \psi _{0}(\Omega _{\omega ^{\omega }})}$) is also the proof-theoretic ordinal of ${\displaystyle \Delta _{2}^{1}-{\mathsf {CR}}}$.
• The proof-theoretic ordinal of ID_<ε0 (${\displaystyle \psi _{0}(\Omega _{\varepsilon _{0}})}$) is also the proof-theoretic ordinal of ${\displaystyle \Delta _{2}^{1}-{\mathsf {CA}}}$ and ${\displaystyle \Sigma _{2}^{1}-{\mathsf {AC}}}$.

References

• An independence result for ${\displaystyle \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 ${\displaystyle \Sigma _{2}^{1}-AC}$
• Large countable ordinals and numbers in Agda
• Ordinal analysis in nLab