Systems of iterated inductive definitions are important formal systems introduced by Feferman (1970), especially of use in proof-theoretic investigations. They are obviously related as well to inductive types in type theory.
Below we record the main definitions and proof-theoretic results about these systems. See also the table at ordinal analysis.
Let us begin by the case of a non-iterated inductive definition, as incarnated in the system ID$_1$, which axiomatizes the least fixed point of an arithmetically definable positive inductive definition.
A subset $I \subseteq \mathbb{N}$ is called inductively defined if it is the least fixed point of a monotone operator $\Gamma : \mathcal{P}(\mathbb{N}) \to \mathcal{P}(\mathbb{N})$. In order to formalize this situation relative to first-order number theory, we consider operators $\Gamma_A$ defined by positive operator forms.
The language of $ID_1$, $\mathcal{L}_{ID_1}$, is obtained from that of first-order number theory, $\mathcal{L}_{\mathbb{N}}$, by the addition of a set (or predicate) constant $I_A$ for every $X$-positive formula $A(X,x)$ in $\mathcal{L}_{\mathbb{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$. If we take the background logic to be constructive, it is common to require that $X$ only occurs strictly positively (never to the left of an implication).
We allow ourselves a bit of set-theoretic notation, and we consider formulas $F(x)$ in a distinguished free variable $x$ to represent the subclass $\{ x\in\mathbb{N} \mid F(x) \}$. We write $s\in F$ to mean $F(s)$, and if $F$ and $G$ are two such formulas, we write $F \subseteq G$ to mean $\forall x. F(x) \to G(x)$.
Then $ID_1$ contains the axioms of first-order number theory with the induction scheme extended to the new language as well as the axiom
and the scheme
where $F(x)$ ranges over all $\mathcal{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\mathbb{N} \mid \mathbb{N} \vDash A(S,x) \}$, while $(ID_1)^2$ expresses that $I_A$ is the least such (at least among sets definable in $\mathcal{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$.
It is possible to define systems of finitely iterated inductive definitions by simply repeating the process of adding a level of inductive definitions and extending the existing schemas to the new language. It’s important that the constants $I_A$ for the previous levels may occur negatively in the operators for the later levels. So these systems can be defined in stages by (metamathematical) induction on $\mathbb{N}$. However, to define the transfinitely iterated variants another approach is needed.
To define the system of $\nu$-times iterated inductive definitions, where $\nu$ is an ordinal, let ${\prec}$ be a primitive recursive well-ordering of order type $\nu$. We use Greek letters to denote elements of the field of ${\prec}$.
The language of $ID_\nu$, $\mathcal{L}_{ID_\nu}$ is obtained from $\mathcal{L}_{\mathbb{N}}$ by the addition of a binary predicate constant $J_A$ for every $X$-positive $\mathcal{L}_{\mathbb{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_A^\mu$ instead of $J_A(\mu,x)$, thinking of $x$ as a distinguished variable in the latter formula.
The system $ID_\nu$ is now obtained from the system of first-order number theory by expanding the induction scheme to the new language and adding the scheme
expressing transfinite induction along ${\prec}$ for an arbitrary $\mathcal{L}_{ID_\nu}$ formula $F$ as well as the axiom
and the scheme
where $F(x)$ is an arbitary $\mathcal{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 \wedge y\in J_A^\gamma), \mu, x)$, where $x$ is the distinguished variable. We see that these express that each $J_A^\mu$, for $\mu\prec\nu$, is the least fixed point (among definable sets) for the operator $\Gamma_A^\mu(S) = \{ n\in\mathbb{N} \mid (\mathbb{N},(J_A^\gamma)_{\gamma\prec\mu}) \vDash A(S,(J_A^\gamma)_{\gamma\prec\mu},\mu,n) \}$. Note how all the previous sets $J_A^\gamma$, for $\gamma\prec\mu$, are used as parameters.
We define $ID_{\prec\nu} = \bigcup_{\xi\prec\nu} ID_\xi$.
It is for instance possible to define the constructive ordinal number classes $\mathcal{O}_\mu$ for $\mu\le\nu$ in $ID_\nu$. Here we describe the simpler example of the constructive tree classes.
The first tree class $\mathcal{T}_0$ is a non-iterated inductive definition, which informally states that
Elements of $\mathcal{T}_0$ represent $\mathbb{N}$-branching trees. Formally, $\mathcal{T}_0$ is represented by $I_A$ for the operator $A(X,x)$ defined by
The higher tree classes $\mathcal{T}_\mu$, for $\mu\prec\nu$, are given by an iterated inductive definition, which informally states that
Now the elements represent infinite trees branching at each internal node over either $\mathbb{N}$ or one of the previous tree classes $\mathcal{T}_\gamma$, for $\gamma\prec\mu$.
To define these higher tree classes, consider the operator form $A(X,Y,\mu,x)$ defined by the disjunction of the corresponding three clauses:
In the last clause we used the class term $Y^\gamma$, thinking of $y$ in $Y(\gamma,y)$ as the distinguished variable.
The book by Buchholz, Feferman, Pohlers and Sieg (1981) contains most proof-theoretic results concerning these systems. For example, the proof-theoretic ordinal of $ID_\nu$ is $\psi_\Omega(\varepsilon_{\Omega_\nu+1})$ for $\nu$ a limit ordinal, and that of $ID_{\prec\nu}$ is $\psi_\Omega(\Omega_\nu)$ when $\nu=\omega^\rho$ for $\rho$ a limit ordinal.
Girard (1982) gave another analysis of the $ID_\nu$ systems using what he calls $\Pi^1_2$-logic, making heavy use of dilators?.
See ordinal analysis for the relations between some of the $ID_\nu$ and $ID_{\prec\nu}$ systems and other systems.
Buchholz, Feferman, Pohlers and Sieg: Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies, Lecture Notes in Mathematics 897 (1981).
Feferman: Formal theories for transfinite iterations of generalized inductive definitions and some subsystems of analysis. In: Intuitionism and Proof Theory (Proc. Conf., Buffalo, N.Y., 1968). 1970.
Feferman: The proof theory of classical and constructive inductive definitions, a 40 year saga, 1968-2008. In: Ways of Proof Theory. 2013. pdf
Girard: Proof-theoretic investigations of inductive definitions, I. In: Logic and algorithmic (Proc. Conf., Zurich, 1980). 1982.
Pohlers: Subsystems of Set Theory and Second Order Number Theory. In: Handbook of Proof Theory. 1998.
Last revised on October 26, 2016 at 06:58:48. See the history of this page for a list of all contributions to it.