Rules Versus Axioms

Both $\mathsf{IR}$ and $\mathsf{ATR}_0$ are formal systems or theories in the language of second order arithmetic. While $\mathsf{ATR}_0$ is easily defined by means of a finite set of axioms, $\mathsf{IR}$ is more conveniently described in terms of inference rules rather than axioms.

1.

The $\Delta^1_1$ comprehension rule:

$$\begin{array}{c} \forall n\,((\exists X\,\alpha(n,X)) \,\le... ...,(n\in Z\,\leftrightarrow\,\exists X\,\alpha(n,X)) \end{array}$$

2.

The $\Delta^1_1$ comprehension axiom:

$$\begin{array}{c} (\forall n\,((\exists X\,\alpha(n,X)) \,\l... ...\,(n\in Z\,\leftrightarrow\,\exists X\,\alpha(n,X)) \end{array}$$

Here $\alpha$ and $\beta$ are arithmetical formulas.

3.

The hierarchy rule:

$$\begin{array}{c} WO(<_e)\\ [-3pt] \rule{1.2in}{.4pt}\\ \forall X\,\exists Y\,H(<_e,X,Y) \end{array}$$

4.

The hierarchy axiom:

$$\forall Z\,(WO(Z)\,\rightarrow\,\forall X\,\exists Y\,H(Z,X,Y))$$

Here WO(Z) is a $\Pi^1_1$ formula expressing that Z is a well ordering, and H(Z,X,Y) is an arithmetical formula expressing that Y is a Turing jump hierararchy along Z starting at X.

5.

The transfinite induction rule:

$$\begin{array}{c} WO(<_e)\\ [-3pt] \rule{1.5in}{.4pt}\\ TI(<_e,\gamma),\quad\gamma\hbox{ arbitrary} \end{array}$$

6.

The transfinite induction axiom:

$$\begin{array}{c} \forall Z\,(WO(Z)\,\rightarrow\,TI(Z,\gamma))\\ [10pt] \mbox{for arbitrary }\gamma\qquad\qquad \end{array}$$

Here $TI(Z,\gamma)$ expresses transfinite induction along Z with respect to the formula $\gamma$.

We are now ready to define the systems $\mathsf{IR}$ and $\mathsf{ATR}_0$.

1.

$\mathsf{IR}$ consists of the $\Delta^1_1$ comprehension rule + the hierarchy rule + the transfinite induction rule.

2.

$\mathsf{ATR}_0$ consists of the hierarchy axiom. It includes the $\Delta^1_1$ comprehension axiom. It is a system with restricted induction (see Friedman [9]) and so does not include the transfinite induction rule.