Buchholz's ID Hierarchy

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)\textrm$", Annals of Pure and Applied Logic vol. 33 (1987).
* $\forall y \forall x (\mathfrak_y(P^\mathfrak_y, x) \rightarrow x \in P^\mathfrak_y)$
* $\forall y (\forall x (\mathfrak_y(F, x) \rightarrow F(x)) \rightarrow \forall x (x \in P^\mathfrak_y \rightarrow F(x)))$ for every L_ID-formula F(x)
* $\forall y \forall x_0 \forall x_1(P^\mathfrak_x_0x_1 \leftrightarrow x_0 < y \land x_1 \in P^\mathfrak_)$

The theory ID_ν with ν ≠ ω is defined as:
* $\forall y \forall x (Z_y(P^\mathfrak_y, x) \rightarrow x \in P^\mathfrak_y)$
* $\forall x (\mathfrak_u(F, x) \rightarrow F(x)) \rightarrow \forall x (P^\mathfrak_ux \rightarrow F(x))$ for every L_ID-formula F(x) and each u < ν
* $\forall y \forall x_0 \forall x_1(P^\mathfrak_x_0x_1 \leftrightarrow x_0 < y \land x_1 \in P^\mathfrak_)$

Explanation / alternate definition

ID₁

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_$, 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 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) = \$
* $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_$ formulas.

Note that $(ID_1)^1$ expresses that $I_A$ is closed under the arithmetically definable set operator $\Gamma_A(S) = \$, while $(ID_1)^2$ expresses that $I_A$ is the least such (at least among sets definable in $L_$).

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_$ is obtained from $L_\N$ by the addition of a binary predicate constant J_A for every X-positive $L_\N$, Y/math> 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_$ 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_$ 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) = \$. Note how all the previous sets $J^\gamma_A$, for $\gamma \prec \mu$, are used as parameters.

We then define $ID_ = \bigcup _ID_\xi$.

Variants

$\widehat_\nu$ - $\widehat_\nu$ is a weakened version of $\mathsf_\nu$. In the system of $\widehat_\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_1) = \psi(\Omega^)$, while $PTO(\mathsf_1) = \psi(\varepsilon_)$.

$\mathsf_\nu\#$ is $\widehat_\nu$ weakened even further. In $\mathsf_\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_1\#) = \psi(\Omega^\omega)$, while $PTO(\widehat_1) = \psi(\Omega^)$.

$\mathsf_\nu$ is the weakest of all variants of $\mathsf_\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_1) = \psi_0(\Omega\times\omega)$, while $PTO(\mathsf_1) = \psi(\varepsilon_)$.

$\mathsf_\nu\mathsf$ is an "unfolding" strengthening of $\mathsf_\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_1) = \psi(\varepsilon_)$, while $PTO(\mathsf_1\mathsf) = \psi(\Gamma_)$.

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_(1) \varphi(n, k)$.
* If the sentence A is provable in ID_ν for all ν < ω, then there exists k ∈ N such that $\vdash_k^ 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_) = \psi_0(\Omega_)$ .
* The proof-theoretic ordinal of $\widehat_$ is equal to $\Gamma_0$.
* The proof-theoretic ordinal of $\widehat_\nu$ for $\nu < \omega$ is equal to $\varphi(\varphi(\nu, 0), 0)$.
* The proof-theoretic ordinal of $\widehat_$ is equal to $\varphi(1, 0, \varphi(\alpha+1, \beta-1))$.
* The proof-theoretic ordinal of $\widehat_$ for $\alpha > 1$ is equal to $\varphi(1, \alpha, 0)$.
* The proof-theoretic ordinal of $\widehat_$ 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_\#$ is equal to $\varphi(0, \omega^)$.
* The proof-theoretic ordinal of $W\textrmID_$ is equal to $\psi_0(\Omega_\times\varphi(\alpha+1, \beta-1))$.
*The proof-theoretic ordinal of $W\textrmID_$ is equal to $\psi_0(\varphi(\alpha+1, \beta-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_)$ is equal to $\psi_0(\Omega^)$.
* The proof-theoretic ordinal of ID₁ (the Bachmann-Howard ordinal) is also the proof-theoretic ordinal of $\mathsf$, $\mathsf$, $\mathsf$ and $\mathsf$.
* The proof-theoretic ordinal of W-ID_ω ($\psi_0(\Omega_\omega\varepsilon_0)$) is also the proof-theoretic ordinal of $\mathsf$.
* The proof-theoretic ordinal of ID_ω (the Takeuti-Feferman-Buchholz ordinal) is also the proof-theoretic ordinal of $\mathsf$, $\Pi^1_1 - \mathsf + \mathsf$ and $\Delta^1_2 - \mathsf + \mathsf$.
* The proof-theoretic ordinal of ID_<ω^ω ($\psi_0(\Omega_)$) is also the proof-theoretic ordinal of $\Delta^1_2 - \mathsf$.
* The proof-theoretic ordinal of ID_<ε0 ($\psi_0(\Omega_)$) is also the proof-theoretic ordinal of $\Delta^1_2 - \mathsf$ and $\Sigma^1_2 - \mathsf$.

References

An independence result for $\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 $\Sigma^1_2 - AC$

Large countable ordinals and numbers in Agda
* Ordinal analysis in nLab

{{DEFAULTSORT:Buchholz's_ID_hierarchy
Ordinal numbers
Proof theory
Set theory
Mathematical logic