1. Definition

1.1. 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:

• [math]\displaystyle{ \forall y \forall x (\mathfrak{M}_y(P^\mathfrak{M}_y, x) \rightarrow x \in P^\mathfrak{M}_y) }[/math]
• [math]\displaystyle{ \forall y (\forall x (\mathfrak{M}_y(F, x) \rightarrow F(x)) \rightarrow \forall x (x \in P^\mathfrak{M}_y \rightarrow F(x))) }[/math] for every L_ID-formula F(x)
• [math]\displaystyle{ \forall y \forall x_0 \forall x_1(P^\mathfrak{M}_{\lt y}x_0x_1 \leftrightarrow x_0 \lt y \and x_1 \in P^\mathfrak{M}_{x_0}) }[/math]

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

• [math]\displaystyle{ \forall y \forall x (Z_y(P^\mathfrak{M}_y, x) \rightarrow x \in P^\mathfrak{M}_y) }[/math]
• [math]\displaystyle{ \forall x (\mathfrak{M}_u(F, x) \rightarrow F(x)) \rightarrow \forall x (P^\mathfrak{M}_ux \rightarrow F(x)) }[/math] for every L_ID-formula F(x) and each u < ν
• [math]\displaystyle{ \forall y \forall x_0 \forall x_1(P^\mathfrak{M}_{\lt y}x_0x_1 \leftrightarrow x_0 \lt y \and x_1 \in P^\mathfrak{M}_{x_0}) }[/math]

1.2. Explanation / Alternate Definition

ID₁

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

• [math]\displaystyle{ F(x) = \{x \in N | F(x)\} }[/math]
• [math]\displaystyle{ s \in F }[/math] means [math]\displaystyle{ F(s) }[/math]
• For two formulas [math]\displaystyle{ F }[/math] and [math]\displaystyle{ G }[/math], [math]\displaystyle{ F \subseteq G }[/math] means [math]\displaystyle{ \forall x F(x) \rightarrow G(x) }[/math].

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:

• [math]\displaystyle{ (ID_1)^1: A(I_A) \subseteq I_A }[/math]
• [math]\displaystyle{ (ID_1)^2: A(F) \subseteq F \rightarrow I_A \subseteq F }[/math]

Where [math]\displaystyle{ F(x) }[/math] ranges over all [math]\displaystyle{ L_{ID_1} }[/math] formulas.

Note that [math]\displaystyle{ (ID_1)^1 }[/math] expresses that [math]\displaystyle{ I_A }[/math] is closed under the arithmetically definable set operator [math]\displaystyle{ \Gamma_A(S) = \{x \in \N | \N \models A(S, x)\} }[/math], while [math]\displaystyle{ (ID_1)^2 }[/math] expresses that [math]\displaystyle{ I_A }[/math] is the least such (at least among sets definable in [math]\displaystyle{ L_{ID_1} }[/math]).

Thus, [math]\displaystyle{ I_A }[/math] is meant to be the least pre-fixed-point, and hence the least fixed point of the operator [math]\displaystyle{ \Gamma_A }[/math].

ID_ν

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

• [math]\displaystyle{ (ID_\nu)^1: \forall \mu \prec \nu; A^\mu(J^\mu_A) \subseteq J^\mu_A }[/math]
• [math]\displaystyle{ (ID_\nu)^2: \forall \mu \prec \nu; A^\mu(F) \subseteq F \rightarrow J^\mu_A \subseteq F }[/math]

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

We then define [math]\displaystyle{ ID_{\prec \nu} = \bigcup \limits_{\xi \prec \nu}ID_\xi }[/math].

Variants

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

[math]\displaystyle{ \mathsf{ID}_\nu\# }[/math] is [math]\displaystyle{ \widehat{\mathsf{ID}}_\nu }[/math] weakened even further. In [math]\displaystyle{ \mathsf{ID}_\nu\# }[/math], 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: [math]\displaystyle{ PTO(\mathsf{ID}_1\#) = \psi(\Omega^\omega) }[/math], while [math]\displaystyle{ PTO(\widehat{\mathsf{ID}}_1) = \psi(\Omega^{\varepsilon_0}) }[/math].

[math]\displaystyle{ \mathsf{W-ID}_\nu }[/math] is the weakest of all variants of [math]\displaystyle{ \mathsf{ID}_\nu }[/math], 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. [math]\displaystyle{ PTO(\mathsf{W-ID}_1) = \psi_0(\Omega\times\omega) }[/math], while [math]\displaystyle{ PTO(\mathsf{ID}_1) = \psi(\varepsilon_{\Omega+1}) }[/math].

[math]\displaystyle{ \mathsf{U(ID}_\nu\mathsf{)} }[/math] is an "unfolding" strengthening of [math]\displaystyle{ \mathsf{ID}_\nu }[/math]. 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 [math]\displaystyle{ \varepsilon_0 }[/math] to [math]\displaystyle{ \Gamma_0 }[/math]: [math]\displaystyle{ PTO(\mathsf{ID}_1) = \psi(\varepsilon_{\Omega+1}) }[/math], while [math]\displaystyle{ PTO(\mathsf{U(ID}_1\mathsf{)}) = \psi(\Gamma_{\Omega+1}) }[/math].

2. Various Formulas

• Let ν > 0. If a ∈ T₀ contains no symbol D_μ with ν < μ, then "a ∈ W₀" is provable in ID_ν.
• ID_ω is contained in [math]\displaystyle{ \Pi^1_1 - CA + BI }[/math].
• If a [math]\displaystyle{ \Pi^0_2 }[/math]-sentence [math]\displaystyle{ \forall x \exists y \varphi(x, y) (\varphi \in \Sigma^0_1) }[/math] is provable in ID_ν, then there exists [math]\displaystyle{ p \in N }[/math] such that [math]\displaystyle{ \forall n \geq p \exists k \lt H_{D_0D^n_\nu0}(1) \varphi(n, k) }[/math].
• If the sentence A is provable in ID_ν for all ν < ω, then there exists k ∈ N such that [math]\displaystyle{ \vdash_k^{D^k_\nu0} A^N }[/math].

3. Proof-theoretic Ordinal(s)

• The proof-theoretic ordinal of ID_<ν is equal to [math]\displaystyle{ \psi_0(\Omega_\nu) }[/math].
• The proof-theoretic ordinal of ID_ν is equal to [math]\displaystyle{ \psi_0(\varepsilon_{\Omega_\nu+1}) = \psi_0(\Omega_{\nu+1}) }[/math] .
• The proof-theoretic ordinal of [math]\displaystyle{ \widehat{ID}_{\lt \omega} }[/math] is equal to [math]\displaystyle{ \varphi(1, 0, 0) }[/math].
• The proof-theoretic ordinal of [math]\displaystyle{ \widehat{ID}_\nu }[/math] for [math]\displaystyle{ \nu \lt \omega }[/math] is equal to [math]\displaystyle{ \varphi(\varphi(\nu, 0), 0) }[/math].
• The proof-theoretic ordinal of [math]\displaystyle{ \widehat{ID}_{\varphi(\alpha, \beta)} }[/math] is equal to [math]\displaystyle{ \varphi(1, 0, \varphi(\alpha+1, \beta-1)) }[/math].
• The proof-theoretic ordinal of [math]\displaystyle{ \widehat{ID}_{\lt \varphi(0, \alpha)} }[/math] for [math]\displaystyle{ \alpha \gt 1 }[/math] is equal to [math]\displaystyle{ \varphi(1, \alpha, 0) }[/math].
• The proof-theoretic ordinal of [math]\displaystyle{ \widehat{ID}_{\lt \nu} }[/math] for [math]\displaystyle{ \nu \geq \varepsilon_0 }[/math] is equal to [math]\displaystyle{ \varphi(1, \nu, 0) }[/math].
• The proof-theoretic ordinal of [math]\displaystyle{ ID_\nu\# }[/math] is equal to [math]\displaystyle{ \varphi(\omega^\nu, 0) }[/math].
• The proof-theoretic ordinal of [math]\displaystyle{ ID_{\lt \nu}\# }[/math] is equal to [math]\displaystyle{ \varphi(0, \omega^{\nu+1}) }[/math].
• The proof-theoretic ordinal of [math]\displaystyle{ W\textrm{-}ID_{\varphi(\alpha, \beta)} }[/math] is equal to [math]\displaystyle{ \psi_0(\Omega_{\varphi(\alpha, \beta)}\times\varphi(\alpha+1, \beta-1)) }[/math].
• The proof-theoretic ordinal of [math]\displaystyle{ W\textrm{-}ID_{\lt \varphi(\alpha, \beta)} }[/math] is equal to [math]\displaystyle{ \psi_0(\varphi(\alpha+1, \beta-1)^{\Omega_{\varphi(\alpha, \beta-1)}+1}) }[/math].
• The proof-theoretic ordinal of [math]\displaystyle{ U(ID_\nu) }[/math] is equal to [math]\displaystyle{ \psi_0(\varphi(\nu, 0, \Omega+1)) }[/math].
• The proof-theoretic ordinal of [math]\displaystyle{ U(ID_{\lt \nu}) }[/math] is equal to [math]\displaystyle{ \psi_0(\Omega^{\Omega+\varphi(\nu, 0, \Omega)}) }[/math].
• The proof-theoretic ordinal of ID₁ (the Bachmann-Howard ordinal) is also the proof-theoretic ordinal of [math]\displaystyle{ \mathsf{KP} }[/math], [math]\displaystyle{ \mathsf{KP\omega} }[/math], [math]\displaystyle{ \mathsf{CZF} }[/math] and [math]\displaystyle{ \mathsf{ML_{1}V} }[/math].
• The proof-theoretic ordinal of W-ID_ω ([math]\displaystyle{ \psi_0(\Omega_\omega\varepsilon_0) }[/math]) is also the proof-theoretic ordinal of [math]\displaystyle{ \mathsf{W-KPI} }[/math].
• The proof-theoretic ordinal of ID_ω (the Takeuti-Feferman-Buchholz ordinal) is also the proof-theoretic ordinal of [math]\displaystyle{ \mathsf{KPI} }[/math], [math]\displaystyle{ \Pi^1_1 - \mathsf{CA} + \mathsf{BI} }[/math] and [math]\displaystyle{ \Delta^1_2 - \mathsf{CA} + \mathsf{BI} }[/math].
• The proof-theoretic ordinal of ID_<ω^ω ([math]\displaystyle{ \psi_0(\Omega_{\omega^\omega}) }[/math]) is also the proof-theoretic ordinal of [math]\displaystyle{ \Delta^1_2 - \mathsf{CR} }[/math].
• The proof-theoretic ordinal of ID_<ε0 ([math]\displaystyle{ \psi_0(\Omega_{\varepsilon_0}) }[/math]) is also the proof-theoretic ordinal of [math]\displaystyle{ \Delta^1_2 - \mathsf{CA} }[/math] and [math]\displaystyle{ \Sigma^1_2 - \mathsf{AC} }[/math].