Theories of iterated inductive definitions

From HandWiki

In set theory and logic, Buchholz's ID hierarchy is a hierarchy of subsystems of first-order arithmetic. The systems/theories [math]\displaystyle{ ID_\nu }[/math] 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 LID, 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 LID-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 \land 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 LID-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 \land x_1 \in P^\mathfrak{M}_{x_0}) }[/math]

Explanation / alternate definition

ID1

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 ID1, [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 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:

  • [math]\displaystyle{ F(x) = \{x \in N \mid 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 ID1 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 \mid \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 JA 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 \land 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 _{\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].

Results

  • Let ν > 0. If a ∈ T0 contains no symbol Dμ with ν < μ, then "a ∈ W0" 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].

Proof-theoretic ordinals

  • 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{ \Gamma_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 ID1 (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].

References



Retrieved from "https://handwiki.org/wiki/index.php?title=Theories_of_iterated_inductive_definitions&oldid=2640191"