Theories of iterated inductive definitions

{{Multiple issues|

}}

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:W. Buchholz, "An Independence Result for $(\Pi^1_1\textrm{-CA})\textrm{+BI}$ ", Annals of Pure and Applied Logic vol. 33 (1987).

$\forall y \forall x (\mathfrak{M}_y(P^\mathfrak{M}_y, x) \rightarrow x \in P^\mathfrak{M}_y)$
$\forall y (\forall x (\mathfrak{M}_y(F, x) \rightarrow F(x)) \rightarrow \forall x (x \in P^\mathfrak{M}_y \rightarrow F(x)))$ for every L_ID-formula F(x)
$\forall y \forall x_0 \forall x_1(P^\mathfrak{M}_{$

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

$\forall y \forall x (Z_y(P^\mathfrak{M}_y, x) \rightarrow x \in P^\mathfrak{M}_y)$
$\forall x (\mathfrak{M}_u(F, x) \rightarrow F(x)) \rightarrow \forall x (P^\mathfrak{M}_ux \rightarrow F(x))$ for every L_ID-formula F(x) and each u < ν
$\forall y \forall x_0 \forall x_1(P^\mathfrak{M}_{$

= Explanation / alternate definition =

== ID<sub>1</sub> ==

A set $I \subseteq \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_\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 x F(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 \N \mid \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<sub>ν</sub> ==

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_\N$ by the addition of a binary predicate constant J_A for every X-positive $L_\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^\mu_A$ 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^\mu_A) \subseteq J^\mu_A$
$(ID_\nu)^2: \forall \mu \prec \nu; A^\mu(F) \subseteq F \rightarrow J^\mu_A \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^\gamma_A), \mu, x)$ , where $x$ is the distinguished variable. We see that these express that each $J^\mu_A$ , for $\mu \prec \nu$ , is the least fixed point (among definable sets) for the operator $\Gamma^\mu_A(S) = \{n \in \N | (\N, (J^\gamma_A)_{\gamma \prec \mu}\}$ . Note how all the previous sets $J^\gamma_A$ , for $\gamma \prec \mu$ , are used as parameters.

We then define $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 \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^0_2$ -sentence $\forall x \exists y \varphi(x, y) (\varphi \in \Sigma^0_1)$ is provable in ID_ν, then there exists $p \in N$ such that $\forall n \geq p \exists k < H_{D_0D^n_\nu0}(1) \varphi(n, k)$ .
If the sentence A is provable in ID_ν for all ν < ω, then there exists k ∈ N such that $\vdash_k^{D^k_\nu0} 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^1_2 - \mathsf{CA} + \mathsf{BI}$ .
The proof-theoretic ordinal of ID_<ω^ω ( $\psi_0(\Omega_{\omega^\omega})$ ) is also the proof-theoretic ordinal of $\Delta^1_2 - \mathsf{CR}$ .
The proof-theoretic ordinal of ID_<ε0 ( $\psi_0(\Omega_{\varepsilon_0})$ ) is also the proof-theoretic ordinal of $\Delta^1_2 - \mathsf{CA}$ and $\Sigma^1_2 - \mathsf{AC}$ .

References

[http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.573.420&rep=rep1&type=pdf An independence result for $\Pi^1_1 - CA + BI$ ]
[https://www.springer.com/gp/book/9783540111702 Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies]
Iterated inductive definitions in nLab
[https://www.sciencedirect.com/science/article/abs/pii/S0049237X08708474 Lemma for the intuitionistic theory of iterated inductive definitions]
[https://www.sciencedirect.com/science/article/abs/pii/S0049237X08707699 Iterated Inductive Definitions and $\Sigma^1_2 - AC$ ]
[https://gist.github.com/AndrasKovacs/8d445c8457ea0967e807c726b2ce5a3a Large countable ordinals and numbers in Agda]
Ordinal analysis in nLab

Category:Ordinal numbers

Category:Proof theory

Category:Set theory

Category:Mathematical logic