# 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 $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:
* $\forall y\forall x({\mathfrak {M}}_{y}(P_{y}^{\mathfrak {M}},x)\rightarrow x\in P_{y}^{\mathfrak {M}})$
* $\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)
* $\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:
* $\forall y\forall x(Z_{y}(P_{y}^{\mathfrak {M}},x)\rightarrow x\in P_{y}^{\mathfrak {M}})$
* $\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 < ν
* $\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$_1$

A set $I\subseteq \mathbb {N}$ is called inductively defined if for some monotonic operator $\Gamma :P(N)\rightarrow P(N)$, $LFP(\Gamma )=I$, where $LFP(f)$ denotes the least fixed point of $f$. The language of ID$_1$, $L_{ID_{1}}$, is obtained from that of first-order number theory, $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:
* $F=\{x\in N\mid F(x)\}$
* $s\in F$ means $F(s)$
* For two formulas $F$ and $G$, $F\subseteq G$ means $\forall xF(x)\rightarrow G(x)$.
Then ID$_1$ 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_{1})^{2}:A(F)\subseteq F\rightarrow 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 \mathbb {N} \mid \mathbb {N} \models A(S,x)\}$, while $(ID_{1})^{2}$ 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_{\mathbb {N} }$ by the addition of a binary predicate constant J$_A$ for every X-positive $L_{\mathbb {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_{A}^{\mu }$ 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_{\nu })^{1}:\forall \mu \prec \nu ;A^{\mu }(J_{A}^{\mu })\subseteq J_{A}^{\mu }$
* $(ID_{\nu })^{2}:\forall \mu \prec \nu ;A^{\mu }(F)\subseteq F\rightarrow J_{A}^{\mu }\subseteq F$
where $F(x)$ is an arbitrary $L_{ID_{\nu }}$ formula. In $(ID_{\nu })^{1}$ and $(ID_{\nu })^{2}$ we used the abbreviation $A^{\mu }(F)$ for the formula $A(F,(\lambda \gamma y;\gamma \prec \mu \land y\in J_{A}^{\gamma }),\mu ,x)$, where $x$ is the distinguished variable. We see that these express that each $J_{A}^{\mu }$, for $\mu \prec \nu$, is the least fixed point (among definable sets) for the operator $\Gamma _{A}^{\mu }(S)=\{n\in \mathbb {N} |(\mathbb {N} ,(J_{A}^{\gamma })_{\gamma \prec \mu }\}$. Note how all the previous sets $J_{A}^{\gamma }$, for $\gamma \prec \mu$, are used as parameters.
We then define ID$_{≺ν}$=⋃$_{ξ≺ν}$ID$_ξ${\textstyle ID_{\prec \nu }=\bigcup _{\xi \prec \nu }ID_{\xi }}.

#### Variants

${\widehat {\mathsf {ID}}}_{\nu }$ - ${\widehat {\mathsf {ID}}}_{\nu }$ is a weakened version of ${\mathsf {ID}}_{\nu }$. In the system of ${\widehat {\mathsf {ID}}}_{\nu }$, a set $I\subseteq \mathbb {N}$ is instead called inductively defined if for some monotonic operator $\Gamma :P(N)\rightarrow 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 {\mathsf {ID}}}_{1})=\psi (\Omega ^{\varepsilon _{0}})$, while $PTO({\mathsf {ID}}_{1})=\psi (\varepsilon _{\Omega +1})$.
${\mathsf {ID}}_{\nu }\#$ is ${\widehat {\mathsf {ID}}}_{\nu }$ weakened even further. In ${\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: $PTO({\mathsf {ID}}_{1}\#)=\psi (\Omega ^{\omega })$, while $PTO({\widehat {\mathsf {ID}}}_{1})=\psi (\Omega ^{\varepsilon _{0}})$.
${\mathsf {W-ID}}_{\nu }$ is the weakest of all variants of ${\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. $PTO({\mathsf {W-ID}}_{1})=\psi _{0}(\Omega \times \omega )$, while $PTO({\mathsf {ID}}_{1})=\psi (\varepsilon _{\Omega +1})$.
${\mathsf {U(ID}}_{\nu }{\mathsf}}$ is an "unfolding" strengthening of ${\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 $\varepsilon _{0}$ to $\Gamma _{0}$: $PTO({\mathsf {ID}}_{1})=\psi (\varepsilon _{\Omega +1})$, while $PTO({\mathsf {U(ID}}_{1}{\mathsf}})=\psi (\Gamma _{\Omega +1})$.

## Results

* Let ν > 0. If a ∈ T$_0$ contains no symbol D$_μ$ with ν < μ, then "a ∈ W$_0$" is provable in ID$_ν$.
* ID$_ω$ is contained in $\Pi _{1}^{1}-CA+BI$.
* If a $\Pi _{2}^{0}$-sentence $\forall x\exists y\varphi (x,y)(\varphi \in \Sigma _{1}^{0})$ is provable in ID$_ν$, then there exists $p\in N$ such that $\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 $\vdash _{k}^{D_{\nu }^{k}0}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 ,\beta )}$ is equal to $\varphi (1,0,\varphi (\alpha +1,\beta -1))$.
* The proof-theoretic ordinal of ${\widehat {ID}}_{<\varphi (0,\alpha )}$ 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{\textrm {-}}ID_{\varphi (\alpha ,\beta )}$ is equal to $\psi _{0}(\Omega _{\varphi (\alpha ,\beta )}\times \varphi (\alpha +1,\beta -1))$.
* The proof-theoretic ordinal of $W{\textrm {-}}ID_{<\varphi (\alpha ,\beta )}$ is equal to $\psi _{0}(\varphi (\alpha +1,\beta -1)^{\Omega _{\varphi (\alpha ,\beta -1)}+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 _{0}(\Omega ^{\Omega +\varphi (\nu ,0,\Omega )})$.
* The proof-theoretic ordinal of ID$_1$ (the Bachmann-Howard ordinal) is also the proof-theoretic ordinal of ${\mathsf {KP}}$, ${\mathsf {KP\omega }}$, ${\mathsf {CZF}}$ and ${\mathsf {ML_{1}V}}$.
* The proof-theoretic ordinal of W-ID$_ω$ ($\psi _{0}(\Omega _{\omega }\varepsilon _{0})$) is also the proof-theoretic ordinal of ${\mathsf {W-KPI}}$.
* The proof-theoretic ordinal of ID$_ω$ (the Takeuti-Feferman-Buchholz ordinal) is also the proof-theoretic ordinal of ${\mathsf {KPI}}$, $\Pi _{1}^{1}-{\mathsf {CA}}+{\mathsf {BI}}$ and $\Delta _{2}^{1}-{\mathsf {CA}}+{\mathsf {BI}}$.
* The proof-theoretic ordinal of ID$_{<ω^ω}$ ($\psi _{0}(\Omega _{\omega ^{\omega }})$) is also the proof-theoretic ordinal of $\Delta _{2}^{1}-{\mathsf {CR}}$.
* The proof-theoretic ordinal of ID$_{<ε0}$ ($\psi _{0}(\Omega _{\varepsilon _{0}})$) is also the proof-theoretic ordinal of $\Delta _{2}^{1}-{\mathsf {CA}}$ and $\Sigma _{2}^{1}-{\mathsf {AC}}$.