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 ${\mathsf {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({\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₁

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₁, $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₁ 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 ${\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₀ contains no symbol D_μ with ν < μ, then "a ∈ W₀" 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₁ (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}}$ .