Subsystems of Second Order Arithmetic

In this section we present some background material concerning $\mathsf{ATR}_0$ and related systems. We present little more than what is needed for our main result, the provability of CKDT in $\mathsf{ATR}_0$. For a broad survey of subsystems of second order arithmetic, see [16]. For detailed information on $\mathsf{ATR}_0$, see [6], [14], [15], [16], and [17].

All of the systems which we shall consider are first-order theories in the language of second order arithmetic. This is a first-order language with two sorts of variables: number variables i, j, k, m, n, ..., and set variables U, V, W, X, Y, Z, .... Number variables are intended to range over the set of natural numbers $\omega=\{0,1,2,\dots\}$, while set variables are intended to range over subsets of $\omega$. Numerical terms are built up as usual from number variables, the constant symbols 0and 1, and the binary operations of addition and multiplication. The atomic formulas of the language are t₁=t₂, t₁<t₂, and $t_1\in X$, where t₁ and t₂ are numerical terms and X is any set variable. Formulas are built up from atomic formulas by means of propositional connectives, number quantifiers $\forall n$and $\exists n$ where n is any number variable, and set quantifiers $\forall X$ and $\exists X$ where X is any set variable. A sentence is a formula with no free variables. The universal closure of a formula is the sentence obtained from the formula by prefixing it with universal quantifiers on all of its free number variables and free set variables. Note that X=Y is not a formula of our language. Rather, equality for sets is defined by extensionality:

$$X=Y\,\,\,\equiv\,\,\,\forall n\,(n\in X\leftrightarrow n\in Y)\,.$$

All of the systems which we shall consider include the Basic Arithmetical Axioms and the Restricted Induction Axiom, expressing elementary properties of the natural number system. The Basic Arithmetical Axioms are the universal closures of the formulas $n+1\neq0$, $m+1=n+1\rightarrow m=n$, m+0=m, m+(n+1)=(m+n)+1, $m\cdot 0=0$, $m\cdot(n+1)=m\cdot n+m$, $\sim m<0$, and $m<n+1\leftrightarrow (m<n\vee m=n)$. The Restricted Induction Axiom is the universal closure of

$$(0\in X\wedge\forall n\,(n\in X\rightarrow n+1\in X)) \rightarrow\forall n\,(n\in X)\,.$$

The Comprehension Scheme consists of the universal closures of all formulas of the form

$$\exists X\,\forall n\,(n\in X\leftrightarrow\varphi(n))$$ (1)

where $\varphi(n)$ is any formula in which X does not occur freely. The idea here is that the given instance of the Comprehension Scheme asserts the existence of an explicitly defined set $X=\{n:\varphi(n)\}$consisting of all natural numbers n such that $\varphi(n)$ holds. Second order arithmetic, also called Z₂, is the first-order theory whose axioms are the Basic Arithmetical Axioms, the Restricted Induction Axiom, and the Comprehension Scheme.

A theorem of Z₂ is any sentence which is deducible from the axioms of Z₂. A subsystem of Z₂ is any first-order theory T in the language of Z₂whose axioms are included in the theorems of Z₂. A theorem of T is any sentence which is deducible from the axioms of T. Theorems of T are also said to be provable in T. At all times we employ the usual axioms and deduction rules of classical first-order logic, with equality for the numerical sort. The intended model of the language of Z₂ is

$$(P(\omega),\omega,+,\cdot,0,1,<,=)$$

where $(\omega,+,\cdot,0,1,<,=)$ is the standard natural number system and $P(\omega)$ is the power set of $\omega$. Clearly all of the axioms of Z₂ are true in the intended model. If T is any subsystem of Z₂, a model of T is any structure ${\mathcal M}$ such that all of the axioms of T are true in ${\mathcal M}$. Here we are employing the well known Tarski truth definition for models of a first-order theory. By the Gödel completeness theorem for first-order logic, the theorems of T are precisely the sentences which are true in all models of T.

An $\omega$-model of T is a model ${\mathcal M}$ of Twhose numerical part is the standard natural number system. Thus we have

$${\mathcal M}=({\cal S},\omega,+,\cdot,0,1,<,=)$$

where ${\cal S}\subseteq P(\omega)$. We shall sometimes identify ${\mathcal M}$ with ${\cal S}$.

An arithmetical formula is a formula which contains no set quantifiers. Note that an arithmetical formula may contain free set variables, as well as free and bound number variables and number quantifiers. A $\Sigma^1_1$ (respectively $\Pi^1_1$) formula is one of the form $\exists X\,\theta$ (respectively $\forall X\,\theta$) where X is any set variable and $\theta$ is any arithmetical formula. More generally, for $k\in\omega$, a formula is said to be $\Sigma^1_k$ (respectively $\Pi^1_k$) if it is of the form $\exists X_1\,\forall X_2\dots X_k\,\,\theta$ (respectively $\forall X_1\,\exists X_2\dots X_k\,\,\theta$) where $\theta$ is arithmetical. Thus a $\Sigma^1_k$ or $\Pi^1_k$ formula consists of k alternating set quantifiers followed by a formula containing no set quantifiers. In a $\Sigma^1_k$ formula the initial set quantifier is existential, while in a $\Pi^1_k$ formula it is universal (assuming k>0).

The Arithmetical Comprehension Scheme consists of all instances of the Comprehension Scheme (1) in which the formula $\varphi(n)$ is arithmetical.

Definition 2.1   $\hbox{\em ACA}_0$ is the subsystem of Z₂ whose axioms are the Basic Arithmetical Axioms, the Restricted Induction Axiom, and the Arithmetical Comprehension Scheme.

The letters ACA stand for arithmetical comprehension axiom. More generally, for $k\in\omega$, we define $\Pi^1_k$- $\mathsf{CA}_0$ to be the subsystem of Z₂ consisting of $\mathsf{ACA}_0$ plus all instances of the Comprehension Scheme (1) in which the formula $\varphi(n)$ is $\Pi^1_k$. One could define $\Sigma^1_k$- $\mathsf{CA}_0$ similarly, but nothing new is obtained, since $\Sigma^1_k$- $\mathsf{CA}_0$ is easily seen to be logically equivalent to $\Pi^1_k$- $\mathsf{CA}_0$. Note also that $\Pi^1_0$- $\mathsf{CA}_0$ is the same as $\mathsf{ACA}_0$. It can be shown that, for all $k\in\omega$, $\Pi^1_{k+1}$- $\mathsf{CA}_0$ is stronger than $\Pi^1_k$- $\mathsf{CA}_0$. In particular, $\Pi^1_1$- $\mathsf{CA}_0$ is stronger than $\mathsf{ACA}_0$.

$\Pi^1_1$- $\mathsf{CA}_0$ and $\mathsf{ACA}_0$ are two of the most important subsystems of Z₂. There are at least two other important subsystems, $\mathsf{RCA}_0$ and $\mathsf{WKL}_0$, both of which are weaker than $\mathsf{ACA}_0$. Although $\mathsf{RCA}_0$ and $\mathsf{WKL}_0$ are of great interest, we shall not define these systems here because they are not essential to our purpose.

When reasoning within a subsystem of Z₂, we use the symbol $\mathbb{N}$ to denote the set of natural numbers within the system, i.e. $\mathbb{N} =\{n:n=n\}$. Thus $\forall n\,(n\in\mathbb{N} )$ is provable in $\mathsf{ACA}_0$. We introduce the numerical pairing function

$$(m,n)=(m+n)^2+m\,.$$

The usual properties such as

$$\forall i\,\forall j\,\forall m\,\forall n\,\, ((i,j)=(m,n)\leftrightarrow(i=m\wedge j=n))$$

can be proved as theorems of $\mathsf{ACA}_0$. We shall also need a set pairing function,

$$(X,Y)=X\oplus Y=\{2n:n\in X\}\cup\{2n+1:n\in Y\}\,$$

and again the usual properties can be proved in $\mathsf{ACA}_0$.

Reasoning within $\mathsf{ACA}_0$ and using the numerical pairing function, we may view any set $Y\subseteq\mathbb{N}$as encoding a countable sequence of sets $\left\langle(Y)_n:n\in\mathbb{N}\right\rangle$ where

$$(Y)_n=\{m:(m,n)\in Y\}\,.$$

The Countable Choice Scheme consists of the universal closures of all formulas of the form

$$(\forall n\,\exists X\,\varphi(n,X))\rightarrow \exists Y\,\forall n\,\,\varphi(n,(Y)_n)$$ (2)

where $\varphi(n,X)$ is any formula in which Y does not occur freely.

Definition 2.2   $\Sigma^1_1$- $\hbox{\em AC}_0$ is the subsystem of Z₂consisting of $\hbox{\em ACA}_0$ plus all instances of the Countable Choice Scheme (2) in which the formula $\varphi(n,X)$ is $\Sigma^1_1$.

The letters AC stand for axiom of choice. It can be shown that the system $\Sigma^1_1$- $\mathsf{AC}_0$ is intermediate in strength between $\mathsf{ACA}_0$ and $\Pi^1_1$- $\mathsf{CA}_0$.

Still reasoning within $\mathsf{ACA}_0$ and using the numerical pairing function, we may view any set $X\subseteq\mathbb{N}$ as encoding a binary relation $R\subseteq\mathbb{N}\times\mathbb{N}$, where $(i\,R\,j)\equiv(i,j)\in X$. We therefore say that X is a linear ordering of $\mathbb{N}$, abbreviated $\hbox{LO}(X)$, if $\forall i\,\forall j\,\forall k\, (((i,j)\in X\wedge(j,k)\in X)\rightarrow(i,k)\in X)$and $\forall i\,(i,i)\notin X$and $\forall i\,\forall j\,(i=j\vee(i,j)\in X\vee(j,i)\in X)$. We say that X is a well ordering of $\mathbb{N}$, abbreviated $\hbox{WO}(X)$, if $\hbox{LO}(X)$ and

$$\forall Y\,((\forall j\, (\forall i\,((i,j)\in X\rightarrow i\in Y)\rightarrow j\in Y)) \rightarrow\forall j\,(j\in Y))\,.$$ (3)

Let $\varphi(n,j,W)$ be any formula with two distinguished free number variables n and j and a distinguished free set variable W. If Z is a set and X is a well ordering of $\mathbb{N}$, we say that Z is obtained by transfinite recursion along Xvia $\varphi(n,j,W)$, abbreviated $\hbox{Rec}(X,\varphi,Z)$, if

$$\forall j\,\forall n\, (n\in(Z)_j\leftrightarrow\varphi(n,j,(Z)^j_X)))$$

where

$$(Z)^j_X=\{(m,i):m\in(Z)_i\wedge(i,j)\in X\}\,.$$

The idea here is that, for each j, the set (Z)_j is defined recursively in terms of the sets (Z)_ifor all i preceding j in the well ordering X. The Transfinite Recursion Scheme consists of the universal closures of all formulas of the form

$$\forall X\,(\hbox{WO}(X)\rightarrow\exists Z\,\hbox{Rec}(X,\varphi,Z))$$ (4)

where Z does not occur freely in $\varphi(n,j,W)$. Thus the Transfinite Recursion Scheme asserts the existence of sets defined by transfinite recursion along arbitrary well orderings of $\mathbb{N}$.

Definition 2.3   $\hbox{\em ATR}_0$ is the subsystem of Z₂ consisting of $\hbox{\em ACA}_0$ plus all instances of the Transfinite Recursion Scheme (4) in which the formula $\varphi$is arithmetical.

The letters ATR stand for arithmetical transfinite recursion. It can be shown that $\mathsf{ATR}_0$ is intermediate in strength between $\Sigma^1_1$- $\mathsf{AC}_0$ and $\Pi^1_1$- $\mathsf{CA}_0$. The system $\mathsf{ATR}_0$ was introduced by Friedman ([5], [4]), who also emphasized its importance for the foundations of mathematics. It is known [16] that many mathematical theorems are provable in $\mathsf{ATR}_0$ and indeed logically equivalent to $\mathsf{ATR}_0$, the equivalence being provable in $\mathsf{ACA}_0$ (in fact in $\mathsf{RCA}_0$). For example, this is the case for the open Ramsey theorem (see [6] and [17]).

An important technique for proving mathematical theorems within $\mathsf{ATR}_0$ is the use of inner models ([6], [10], [17]). Within $\mathsf{ATR}_0$, any subset Z of $\mathbb{N}$ determines a countable set ${\cal S}=\{(Z)_n:n\in\mathbb{N}\}$ of subsets of $\mathbb{N}$. This set of sets ${\cal S}$ may be identified with a countable $\omega$-model ${\mathcal M}=({\cal S},\mathbb{N} ,+,\cdot,0,1,<,=)$and in this way Z may be regarded as a code of the inner model ${\mathcal M}$. In particular, for any set $W\subseteq\mathbb{N}$, we have $W\in{\mathcal M}$ if and only if $\exists n(W=(Z)_n)$. Given such a countable coded $\omega$-model ${\mathcal M}$, we can carry out the Tarski truth definition within $\mathsf{ATR}_0$ to obtain a full satisfaction predicate for ${\mathcal M}$. Here formulas of the language of Z₂are identified with their Gödel numbers. Thus within $\mathsf{ATR}_0$ we may speak of countable coded $\omega$-models of T, where T is any recursively axiomatized subsystem of Z₂.

The following result from [17] will be used to prove our main theorem, in Section 3 below.

Lemma 1   The following is provable in $\hbox{\em ATR}_0$. For any set $W\subseteq\mathbb{N}$, there exists a countable coded $\omega$-model ${\mathcal M}$ of $\Sigma^1_1$- $\hbox{\em AC}_0$ such that $W\in{\mathcal M}$.

Proof. We shall use the formalization within $\mathsf{ATR}_0$ of some facts and techniques from recursive function theory and hyperarithmetical theory [13]. For details of the formalization within $\mathsf{ATR}_0$, see [4], [6], and [17].

We shall use the arithmetical formula

$$\hbox{WO}(X,Z)\,\,\,\equiv\,\,\, \hbox{LO}(X)\wedge\forall Y\,(Y\hbox{ Turing reducible to }Z\rightarrow \hbox{Ind}(X,Y))\,,$$

where $\forall Y\,\hbox{Ind}(X,Y)$ is the formula (3). Trivially we have

$$\forall X\,(\hbox{WO}(X)\leftrightarrow\forall Z\,\hbox{WO}(X,Z))\,.$$

Reasoning within $\mathsf{ATR}_0$, fix a set $W\subseteq\mathbb{N}$. Consider the arithmetical formula

$$\eta(W,X,Z)\,\,\,\equiv\,\,\, \hbox{WO}(X,Z)\,\wedge\,\forall j\,\, ((Z)_j=\hbox{Turing jump of }(W\oplus X)\oplus(Z)^j_X)\,.$$

By arithmetical transfinite recursion we have

$$\forall X\,(\hbox{WO}(X)\rightarrow\exists Z\,\eta(W,X,Z))\,.$$

On the other hand, the formula $\hbox{WO}(X)$ is complete $\Pi^1_1$ and hence not equivalent to any $\Sigma^1_1$ formula (see [13], Chapter 16). In particular, $\hbox{WO}(X)$ is not equivalent to the $\Sigma^1_1$ formula $\exists Z\,\eta(W,X,Z)$. These considerations imply that there exist sets X and Z such that $\eta(W,X,Z)\,\wedge\,{\sim}\hbox{WO}(X)$. Fix such an X and Z.

Using $\hbox{WO}(X,Z)$ and the fact that X is Turing reducible to Z, it is easy to see that the linear ordering X has the following properties: there is a least element, and any element other than the greatest element (if there is one) has an immediate successor. Using ${\sim}\hbox{WO}(X)$, let $J\subseteq\mathbb{N}$ be such that $\hbox{Ind}(X,J)$ fails, and put $I=\{j:\forall i\,((i,j)\in X\rightarrow i\in J)\}$. Then clearly I is a cut in X, i.e. we have $\exists i\,\exists j\,(i\in I\wedge j\notin I)$ and $\forall i\,\forall j\,((i\in I\wedge j\notin I)\rightarrow (i,j)\in X))$ and $\forall i\,(i\in I\rightarrow\exists k\, ((i,k)\in X\wedge k\in I))$and $\forall j\,(j\notin I\rightarrow\exists k\, ((k,j)\in X\wedge k\notin I))$.

By arithmetical comprehension, there exists a countable coded $\omega$-model ${\mathcal M}$ consisting of all sets A such that A is Turing reducible to (Z)_i for some $i\in I$. Clearly $W\in{\mathcal M}$ and $X\in{\mathcal M}$. It is also clear that ${\mathcal M}$ is closed under $\oplus$ and Turing reducibility and the Turing jump operator. From this it follows by Post's theorem ([13], Chapter 14) that ${\mathcal M}$ is an $\omega$-model of $\mathsf{ACA}_0$.

We claim that ${\mathcal M}$ is an $\omega$-model of $\Sigma^1_1$- $\mathsf{AC}_0$. To see this, let $\varphi(n,U)$ be any $\Sigma^1_1$ formula. Let $n_1,\dots,n_k,U_1,\dots,U_m$be the free variables of $\varphi(n,U)$ other than n and U. Fix $a_1,\dots,a_k\in\mathbb{N}$ and $A_1,\dots,A_m\in{\mathcal M}$and suppose that ${\mathcal M}$ satisfies $\forall n\,\exists U\,\bar\varphi(n,U)$, where

$$\bar\varphi(n,U)\,\,\,\equiv\,\,\, \varphi(n,U)[n_1/a_1,\dots,n_k/a_k,U_1/A_1,\dots,U_m/A_m]\,.$$

Let us write

$$\varphi(n,U)\,\,\,\equiv\,\,\,\exists V\,\theta(n,U,V)$$

where $\theta(n,U,V)$ is arithmetical, and put

$$\bar\theta(n,U,V)\,\,\,\equiv\,\,\, \theta(n,U,V)[n_1/a_1,\dots,n_k/a_k,U_1/A_1,\dots,U_m/A_m]\,.$$

Then ${\mathcal M}$ satisfies $\forall n\,\exists U\,\exists V\,\bar\theta(n,U,V)$. It follows that for each $n\in\mathbb{N}$ there exists $i\in I$ such that

$$\exists U\,\exists V\,(\bar\theta(n,U,V)\,\wedge\, U\hbox{ and }V\hbox{ are Turing reducible to }(Z)_i)\,.$$ (5)

Hence by $\hbox{WO}(X,Z)$ we have that for each $n\in\mathbb{N}$ there exists a least such iwith respect to the linear ordering of $\mathbb{N}$ given by X. Define $f:\mathbb{N}\to\mathbb{N}$ by f(n)= the least $i\in\mathbb{N}$with respect to the linear ordering X such that (5) holds. Since $f(n)\in I$ for all $n\in\mathbb{N}$, it follows that f is Turing reducible to (Z)_j for any $j\notin I$. Hence by $\hbox{WO}(X,Z)$ there exists $k\in\mathbb{N}$ such that k is the least upper bound, with respect to the linear ordering X, of the range of f. Since $f(n)\in I$ for all $n\in\mathbb{N}$, it follows that $k\in I$. Thus we have a set $(Z)_k\in{\mathcal M}$ such that $\forall n\,\exists U\,\exists V\,(\bar\theta(n,U,V)\,\wedge\, \hbox{$U$\space and $V$\space are Turing reducible to $(Z)_k$ })$. We can now use arithmetical comprehension within ${\mathcal M}$to find a set $T\in{\mathcal M}$ such that $\forall n\,\bar\theta(n,((T)_n)_0,((T)_n)_1)$. Putting $Y=\{(m,n):((m,0),n)\in T\}$, we obtain $Y\in{\mathcal M}$ such that $\forall n\,\bar\theta(n,(Y)_n,((T)_n)_1)$. Thus ${\mathcal M}$ satisfies $\exists Y\,\forall n\,\exists V\,\bar\theta(n,(Y)_n,V)$, i.e. $\exists Y\,\forall n\,\bar\varphi(n,(Y)_n)$. Thus ${\mathcal M}$ is an $\omega$-model of $\Sigma^1_1$- $\mathsf{AC}_0$ and the proof of Lemma 1 is complete.

Remark. The assertion considered in the previous lemma (``for all W there exists a countable coded $\omega$-model of $\Sigma^1_1$- $\mathsf{AC}_0$ containing W'') is in fact equivalent to $\mathsf{ATR}_0$ over $\mathsf{RCA}_0$. This is shown in [17].