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 $I{D}_{\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:

• $\mathrm{\forall }y\mathrm{\forall }x({\mathfrak{𝔐}}_y(P_y^{\mathfrak{𝔐}},x)\to x\in P_y^{\mathfrak{𝔐}})$
• $\mathrm{\forall }y(\mathrm{\forall }x({\mathfrak{𝔐}}_y(F,x)\to F(x))\to \mathrm{\forall }x(x\in P_y^{\mathfrak{𝔐}}\to F(x)))$ for every L_ID-formula F(x)
• $\mathrm{\forall }y\mathrm{\forall }{x}_0\mathrm{\forall }{x}_1(P_{<y}^{\mathfrak{𝔐}}{x}_0{x}_1\leftrightarrow x_0<y\wedge x_1\in P_{x_0}^{\mathfrak{𝔐}})$

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

• $\mathrm{\forall }y\mathrm{\forall }x(Z_y(P_y^{\mathfrak{𝔐}},x)\to x\in P_y^{\mathfrak{𝔐}})$
• $\mathrm{\forall }x({\mathfrak{𝔐}}_u(F,x)\to F(x))\to \mathrm{\forall }x(P_u^{\mathfrak{𝔐}}x\to F(x))$ for every L_ID-formula F(x) and each u < ν
• $\mathrm{\forall }y\mathrm{\forall }{x}_0\mathrm{\forall }{x}_1(P_{<y}^{\mathfrak{𝔐}}{x}_0{x}_1\leftrightarrow x_0<y\wedge x_1\in P_{x_0}^{\mathfrak{𝔐}})$

Explanation / alternate definition

ID₁

A set $I\subseteq \mathbb{\mathbb{N}}$ is called inductively defined if for some monotonic operator $\mathrm{\Gamma }:P(N)\to P(N)$, $LFP(\mathrm{\Gamma })=I$, where $LFP(f)$ denotes the least fixed point of $f$. The language of ID₁, $L_{I{D}_1}$, is obtained from that of first-order number theory, $L_{\mathbb{\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)=\{x\in N\mid F(x)\}$
• $s\in F$ means $F(s)$
• For two formulas $F$ and $G$, $F\subseteq G$ means $\mathrm{\forall }xF(x)\to 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:

• $(I{D}_1{)}^1:A(I_A)\subseteq I_A$
• $(I{D}_1{)}^2:A(F)\subseteq F\to I_A\subseteq F$

Where $F(x)$ ranges over all $L_{I{D}_1}$ formulas. Note that $(I{D}_1{)}^1$ expresses that $I_A$ is closed under the arithmetically definable set operator ${\mathrm{\Gamma }}_A(S)=\{x\in \mathbb{\mathbb{N}}\mid \mathbb{\mathbb{N}}\models A(S,x)\}$, while $(I{D}_1{)}^2$ expresses that $I_A$ is the least such (at least among sets definable in $L_{I{D}_1}$). Thus, $I_A$ is meant to be the least pre-fixed-point, and hence the least fixed point of the operator ${\mathrm{\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_{I{D}_{\nu }}$ is obtained from $L_{\mathbb{\mathbb{N}}}$ by the addition of a binary predicate constant J_A for every X-positive $L_{\mathbb{\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 $(T{I}_{\nu }):TI(\prec ,F)$ expressing transfinite induction along $\prec$ for an arbitrary $L_{I{D}_{\nu }}$ formula $F$ as well as the axioms:

• $(I{D}_{\nu }{)}^1:\mathrm{\forall }\mu \prec \nu ;A^{\mu }(J_A^{\mu })\subseteq J_A^{\mu }$
• $(I{D}_{\nu }{)}^2:\mathrm{\forall }\mu \prec \nu ;A^{\mu }(F)\subseteq F\to J_A^{\mu }\subseteq F$

where $F(x)$ is an arbitrary $L_{I{D}_{\nu }}$ formula. In $(I{D}_{\nu }{)}^1$ and $(I{D}_{\nu }{)}^2$ we used the abbreviation $A^{\mu }(F)$ for the formula $A(F,(\lambda \gamma y;\gamma \prec \mu \wedge 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 ${\mathrm{\Gamma }}_A^{\mu }(S)=\{n\in \mathbb{\mathbb{N}}|(\mathbb{\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 $I{D}_{\prec \nu }=\bigcup _{\xi \prec \nu }I{D}_{\xi }$.

Variants

${\widehat{\mathsf{I}\mathsf{D}}}_{\nu }$ - ${\widehat{\mathsf{I}\mathsf{D}}}_{\nu }$ is a weakened version of ${\mathsf{I}\mathsf{D}}_{\nu }$. In the system of ${\widehat{\mathsf{I}\mathsf{D}}}_{\nu }$, a set $I\subseteq \mathbb{\mathbb{N}}$ is instead called inductively defined if for some monotonic operator $\mathrm{\Gamma }:P(N)\to P(N)$, $I$ is a fixed point of $\mathrm{\Gamma }$, rather than the least fixed point. This subtle difference makes the system significantly weaker: $PTO({\widehat{\mathsf{I}\mathsf{D}}}_1)=\psi ({\mathrm{\Omega }}^{{\epsilon }_0})$, while $PTO({\mathsf{I}\mathsf{D}}_1)=\psi ({\epsilon }_{\mathrm{\Omega }+1})$. ${\mathsf{I}\mathsf{D}}_{\nu }\mathrm{\#}$ is ${\widehat{\mathsf{I}\mathsf{D}}}_{\nu }$ weakened even further. In ${\mathsf{I}\mathsf{D}}_{\nu }\mathrm{\#}$, 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{I}\mathsf{D}}_1\mathrm{\#})=\psi ({\mathrm{\Omega }}^{\omega })$, while $PTO({\widehat{\mathsf{I}\mathsf{D}}}_1)=\psi ({\mathrm{\Omega }}^{{\epsilon }_0})$. ${\mathsf{W}\mathsf{-}\mathsf{I}\mathsf{D}}_{\nu }$ is the weakest of all variants of ${\mathsf{I}\mathsf{D}}_{\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}\mathsf{-}\mathsf{I}\mathsf{D}}_1)={\psi }_0(\mathrm{\Omega }\times \omega )$, while $PTO({\mathsf{I}\mathsf{D}}_1)=\psi ({\epsilon }_{\mathrm{\Omega }+1})$. ${\mathsf{U}\mathsf{(}\mathsf{I}\mathsf{D}}_{\nu }\mathsf{)}$ is an "unfolding" strengthening of ${\mathsf{I}\mathsf{D}}_{\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 ${\epsilon }_0$ to ${\mathrm{\Gamma }}_0$: $PTO({\mathsf{I}\mathsf{D}}_1)=\psi ({\epsilon }_{\mathrm{\Omega }+1})$, while $PTO({\mathsf{U}\mathsf{(}\mathsf{I}\mathsf{D}}_1\mathsf{)})=\psi ({\mathrm{\Gamma }}_{\mathrm{\Omega }+1})$.

Results

• Let ν > 0. If a ∈ T₀ contains no symbol D_μ with ν < μ, then "a ∈ W₀" is provable in ID_ν.
• ID_ω is contained in ${\mathrm{\Pi }}_1^1-CA+BI$.
• If a ${\mathrm{\Pi }}_2^0$-sentence $\mathrm{\forall }x\mathrm{\exists }y\phi (x,y)(\phi \in {\mathrm{\Sigma }}_1^0)$ is provable in ID_ν, then there exists $p\in N$ such that $\mathrm{\forall }n\ge p\mathrm{\exists }k<H_{D_0{D}_{\nu }^{n}0}(1)\phi (n,k)$.
• If the sentence A is provable in ID_ν for all ν < ω, then there exists k ∈ N such that $\underset{k}{\overset{D_{\nu }^{k}0}{⊢}}{A}^N$.

Proof-theoretic ordinals

• The proof-theoretic ordinal of ID_<ν is equal to ${\psi }_0({\mathrm{\Omega }}_{\nu })$.
• The proof-theoretic ordinal of ID_ν is equal to ${\psi }_0({\epsilon }_{{\mathrm{\Omega }}_{\nu }+1})={\psi }_0({\mathrm{\Omega }}_{\nu +1})$ .
• The proof-theoretic ordinal of ${\widehat{ID}}_{<\omega }$ is equal to ${\mathrm{\Gamma }}_0$.
• The proof-theoretic ordinal of ${\widehat{ID}}_{\nu }$ for $\nu <\omega$ is equal to $\phi (\phi (\nu ,0),0)$.
• The proof-theoretic ordinal of ${\widehat{ID}}_{\phi (\alpha ,\beta )}$ is equal to $\phi (1,0,\phi (\alpha +1,\beta -1))$.
• The proof-theoretic ordinal of ${\widehat{ID}}_{<\phi (0,\alpha )}$ for $\alpha >1$ is equal to $\phi (1,\alpha ,0)$.
• The proof-theoretic ordinal of ${\widehat{ID}}_{<\nu }$ for $\nu \ge {\epsilon }_0$ is equal to $\phi (1,\nu ,0)$.
• The proof-theoretic ordinal of $I{D}_{\nu }\mathrm{\#}$ is equal to $\phi ({\omega }^{\nu },0)$.
• The proof-theoretic ordinal of $I{D}_{<\nu }\mathrm{\#}$ is equal to $\phi (0,{\omega }^{\nu +1})$.
• The proof-theoretic ordinal of $W\text{<mo stretchy="false">−</mo>}I{D}_{\phi (\alpha ,\beta )}$ is equal to ${\psi }_0({\mathrm{\Omega }}_{\phi (\alpha ,\beta )}\times \phi (\alpha +1,\beta -1))$.
• The proof-theoretic ordinal of $W\text{<mo stretchy="false">−</mo>}I{D}_{<\phi (\alpha ,\beta )}$ is equal to ${\psi }_0(\phi (\alpha +1,\beta -1{)}^{{\mathrm{\Omega }}_{\phi (\alpha ,\beta -1)}+1})$.
• The proof-theoretic ordinal of $U(I{D}_{\nu })$ is equal to ${\psi }_0(\phi (\nu ,0,\mathrm{\Omega }+1))$.
• The proof-theoretic ordinal of $U(I{D}_{<\nu })$ is equal to ${\psi }_0({\mathrm{\Omega }}^{\mathrm{\Omega }+\phi (\nu ,0,\mathrm{\Omega })})$.
• The proof-theoretic ordinal of ID₁ (the Bachmann-Howard ordinal) is also the proof-theoretic ordinal of $\mathsf{K}\mathsf{P}$, $\mathsf{K}\mathsf{P}\mathsf{\omega }$, $\mathsf{C}\mathsf{Z}\mathsf{F}$ and $\mathsf{M}{\mathsf{L}}_{\mathsf{1}}\mathsf{V}$.
• The proof-theoretic ordinal of W-ID_ω (${\psi }_0({\mathrm{\Omega }}_{\omega }{\epsilon }_0)$) is also the proof-theoretic ordinal of $\mathsf{W}\mathsf{-}\mathsf{K}\mathsf{P}\mathsf{I}$.
• The proof-theoretic ordinal of ID_ω (the Takeuti-Feferman-Buchholz ordinal) is also the proof-theoretic ordinal of $\mathsf{K}\mathsf{P}\mathsf{I}$, ${\mathrm{\Pi }}_1^1-\mathsf{C}\mathsf{A}+\mathsf{B}\mathsf{I}$ and ${\mathrm{\Delta }}_2^1-\mathsf{C}\mathsf{A}+\mathsf{B}\mathsf{I}$.
• The proof-theoretic ordinal of ID_<ω^ω (${\psi }_0({\mathrm{\Omega }}_{{\omega }^{\omega }})$) is also the proof-theoretic ordinal of ${\mathrm{\Delta }}_2^1-\mathsf{C}\mathsf{R}$.
• The proof-theoretic ordinal of ID_<ε0 (${\psi }_0({\mathrm{\Omega }}_{{\epsilon }_0})$) is also the proof-theoretic ordinal of ${\mathrm{\Delta }}_2^1-\mathsf{C}\mathsf{A}$ and ${\mathrm{\Sigma }}_2^1-\mathsf{A}\mathsf{C}$.

References

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