Submitted Successfully!
To reward your contribution, here is a gift for you: A free trial for our video production service.
Thank you for your contribution! You can also upload a video entry or images related to this topic.
Version Summary Created by Modification Content Size Created at Operation
1 handwiki -- 1879 2022-10-25 01:46:29

Do you have a full video?

# Confirm

Are you sure to Delete?
Cite
HandWiki. Buchholz's ID Hierarchy. Encyclopedia. Available online: https://encyclopedia.pub/entry/31036 (accessed on 17 April 2024).
HandWiki. Buchholz's ID Hierarchy. Encyclopedia. Available at: https://encyclopedia.pub/entry/31036. Accessed April 17, 2024.
HandWiki. "Buchholz's ID Hierarchy" Encyclopedia, https://encyclopedia.pub/entry/31036 (accessed April 17, 2024).
HandWiki. (2022, October 25). Buchholz's ID Hierarchy. In Encyclopedia. https://encyclopedia.pub/entry/31036
HandWiki. "Buchholz's ID Hierarchy." Encyclopedia. Web. 25 October, 2022.
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 $\displaystyle{ 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.

set theory logic idν

## 1. Definition

### 1.1. Original Definition

The formal theory IDω (and IDν in general) is an extension of Peano Arithmetic, formulated in the language LID, by the following axioms:

• $\displaystyle{ \forall y \forall x (\mathfrak{M}_y(P^\mathfrak{M}_y, x) \rightarrow x \in P^\mathfrak{M}_y) }$
• $\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))) }$ for every LID-formula F(x)
• $\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}) }$

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

• $\displaystyle{ \forall y \forall x (Z_y(P^\mathfrak{M}_y, x) \rightarrow x \in P^\mathfrak{M}_y) }$
• $\displaystyle{ \forall x (\mathfrak{M}_u(F, x) \rightarrow F(x)) \rightarrow \forall x (P^\mathfrak{M}_ux \rightarrow F(x)) }$ for every LID-formula F(x) and each u < ν
• $\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}) }$

### 1.2. Explanation / Alternate Definition

#### ID1

A set $\displaystyle{ I \subseteq \N }$ is called inductively defined if for some monotonic operator $\displaystyle{ \Gamma: P(N) \rightarrow P(N) }$, $\displaystyle{ LFP(\Gamma) = I }$, where $\displaystyle{ LFP(f) }$ denotes the least fixed point of $\displaystyle{ f }$. The language of ID1, $\displaystyle{ L_{ID_1} }$, is obtained from that of first-order number theory, $\displaystyle{ L_\N }$, by the addition of a set (or predicate) constant IA for every X-positive formula A(X, x) in LN[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:

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

Then ID1 contains the axioms of first-order number theory (PA) with the induction scheme extended to the new language as well as these axioms:

• $\displaystyle{ (ID_1)^1: A(I_A) \subseteq I_A }$
• $\displaystyle{ (ID_1)^2: A(F) \subseteq F \rightarrow I_A \subseteq F }$

Where $\displaystyle{ F(x) }$ ranges over all $\displaystyle{ L_{ID_1} }$ formulas.

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

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

#### IDν

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

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

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

We then define $\displaystyle{ ID_{\prec \nu} = \bigcup \limits_{\xi \prec \nu}ID_\xi }$.

#### Variants

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

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

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

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

## 2. Various Formulas

• Let ν > 0. If a ∈ T0 contains no symbol Dμ with ν < μ, then "a ∈ W0" is provable in IDν.
• IDω is contained in $\displaystyle{ \Pi^1_1 - CA + BI }$.
• If a $\displaystyle{ \Pi^0_2 }$-sentence $\displaystyle{ \forall x \exists y \varphi(x, y) (\varphi \in \Sigma^0_1) }$ is provable in IDν, then there exists $\displaystyle{ p \in N }$ such that $\displaystyle{ \forall n \geq p \exists k \lt 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 $\displaystyle{ \vdash_k^{D^k_\nu0} A^N }$.

## 3. Proof-theoretic Ordinal(s)

• The proof-theoretic ordinal of ID is equal to $\displaystyle{ \psi_0(\Omega_\nu) }$.
• The proof-theoretic ordinal of IDν is equal to $\displaystyle{ \psi_0(\varepsilon_{\Omega_\nu+1}) = \psi_0(\Omega_{\nu+1}) }$ .
• The proof-theoretic ordinal of $\displaystyle{ \widehat{ID}_{\lt \omega} }$ is equal to $\displaystyle{ \varphi(1, 0, 0) }$.
• The proof-theoretic ordinal of $\displaystyle{ \widehat{ID}_\nu }$ for $\displaystyle{ \nu \lt \omega }$ is equal to $\displaystyle{ \varphi(\varphi(\nu, 0), 0) }$.
• The proof-theoretic ordinal of $\displaystyle{ \widehat{ID}_{\varphi(\alpha, \beta)} }$ is equal to $\displaystyle{ \varphi(1, 0, \varphi(\alpha+1, \beta-1)) }$.
• The proof-theoretic ordinal of $\displaystyle{ \widehat{ID}_{\lt \varphi(0, \alpha)} }$ for $\displaystyle{ \alpha \gt 1 }$ is equal to $\displaystyle{ \varphi(1, \alpha, 0) }$.
• The proof-theoretic ordinal of $\displaystyle{ \widehat{ID}_{\lt \nu} }$ for $\displaystyle{ \nu \geq \varepsilon_0 }$ is equal to $\displaystyle{ \varphi(1, \nu, 0) }$.
• The proof-theoretic ordinal of $\displaystyle{ ID_\nu\# }$ is equal to $\displaystyle{ \varphi(\omega^\nu, 0) }$.
• The proof-theoretic ordinal of $\displaystyle{ ID_{\lt \nu}\# }$ is equal to $\displaystyle{ \varphi(0, \omega^{\nu+1}) }$.
• The proof-theoretic ordinal of $\displaystyle{ W\textrm{-}ID_{\varphi(\alpha, \beta)} }$ is equal to $\displaystyle{ \psi_0(\Omega_{\varphi(\alpha, \beta)}\times\varphi(\alpha+1, \beta-1)) }$.
• The proof-theoretic ordinal of $\displaystyle{ W\textrm{-}ID_{\lt \varphi(\alpha, \beta)} }$ is equal to $\displaystyle{ \psi_0(\varphi(\alpha+1, \beta-1)^{\Omega_{\varphi(\alpha, \beta-1)}+1}) }$.
• The proof-theoretic ordinal of $\displaystyle{ U(ID_\nu) }$ is equal to $\displaystyle{ \psi_0(\varphi(\nu, 0, \Omega+1)) }$.
• The proof-theoretic ordinal of $\displaystyle{ U(ID_{\lt \nu}) }$ is equal to $\displaystyle{ \psi_0(\Omega^{\Omega+\varphi(\nu, 0, \Omega)}) }$.
• The proof-theoretic ordinal of ID1 (the Bachmann-Howard ordinal) is also the proof-theoretic ordinal of $\displaystyle{ \mathsf{KP} }$, $\displaystyle{ \mathsf{KP\omega} }$, $\displaystyle{ \mathsf{CZF} }$ and $\displaystyle{ \mathsf{ML_{1}V} }$.
• The proof-theoretic ordinal of W-IDω ($\displaystyle{ \psi_0(\Omega_\omega\varepsilon_0) }$) is also the proof-theoretic ordinal of $\displaystyle{ \mathsf{W-KPI} }$.
• The proof-theoretic ordinal of IDω (the Takeuti-Feferman-Buchholz ordinal) is also the proof-theoretic ordinal of $\displaystyle{ \mathsf{KPI} }$, $\displaystyle{ \Pi^1_1 - \mathsf{CA} + \mathsf{BI} }$ and $\displaystyle{ \Delta^1_2 - \mathsf{CA} + \mathsf{BI} }$.
• The proof-theoretic ordinal of ID<ω^ω ($\displaystyle{ \psi_0(\Omega_{\omega^\omega}) }$) is also the proof-theoretic ordinal of $\displaystyle{ \Delta^1_2 - \mathsf{CR} }$.
• The proof-theoretic ordinal of ID<ε0 ($\displaystyle{ \psi_0(\Omega_{\varepsilon_0}) }$) is also the proof-theoretic ordinal of $\displaystyle{ \Delta^1_2 - \mathsf{CA} }$ and $\displaystyle{ \Sigma^1_2 - \mathsf{AC} }$.
Information
Subjects:
Contributor MDPI registered users' name will be linked to their SciProfiles pages. To register with us, please refer to https://encyclopedia.pub/register :
View Times: 192
Entry Collection:
Revision: 1 time (View History)
Update Date: 25 Oct 2022
1000/1000