Theories of iterated inductive definitions

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

• ${\displaystyle \forall y\forall x({\mathfrak {M}}_{y}(P_{y}^{\mathfrak {M}},x)\rightarrow x\in P_{y}^{\mathfrak {M}})}$
• ${\displaystyle \forall y(\forall x({\mathfrak {M}}_{y}(F,x)\rightarrow F(x))\rightarrow \forall x(x\in P_{y}^{\mathfrak {M}}\rightarrow F(x)))}$ for every L_ID-formula F(x)
• ${\displaystyle \forall y\forall x_{0}\forall x_{1}(P_{<y}^{\mathfrak {M}}x_{0}x_{1}\leftrightarrow x_{0}<y\land x_{1}\in P_{x_{0}}^{\mathfrak {M}})}$

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

• ${\displaystyle \forall y\forall x(Z_{y}(P_{y}^{\mathfrak {M}},x)\rightarrow x\in P_{y}^{\mathfrak {M}})}$
• ${\displaystyle \forall x({\mathfrak {M}}_{u}(F,x)\rightarrow F(x))\rightarrow \forall x(P_{u}^{\mathfrak {M}}x\rightarrow F(x))}$ for every L_ID-formula F(x) and each u < ν
• ${\displaystyle \forall y\forall x_{0}\forall x_{1}(P_{<y}^{\mathfrak {M}}x_{0}x_{1}\leftrightarrow x_{0}<y\land x_{1}\in P_{x_{0}}^{\mathfrak {M}})}$

A set ${\displaystyle I\subseteq \mathbb {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 ID₁, ${\displaystyle L_{ID_{1}}}$, is obtained from that of first-order number theory, ${\displaystyle L_{\mathbb {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:

• ${\displaystyle F(x)=\{x\in N\mid 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 xF(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:

• ${\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 \mathbb {N} \mid \mathbb {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}}$.

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

We then define ${\textstyle ID_{\prec \nu }=\bigcup _{\xi \prec \nu }ID_{\xi }}$.

${\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 \mathbb {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})}$.