Derivatives of normal functions and omega-models

TL;DR

This paper explores the relationship between the well-ordering principle for derivatives of normal functions on ordinals and the existence of large countable omega-models, establishing an equivalence between these concepts.

Contribution

It demonstrates the equivalence between the well-ordering principle for derivatives of normal functions and the existence of arbitrarily large countable omega-models.

Findings

Well-ordering principle for derivatives of normal functions is equivalent to the existence of large omega-models.

Establishes a new connection between ordinal functions and model theory.

Provides a foundational result in the theory of normal functions and models.

Abstract

In this note the well-ordering principle for the derivative of normal functions on ordinals is shown to be equivalent to the existence of arbitrarily large countable coded omega-models of the well-ordering principle for the function.

Equations

$$\mathrm{LO}(X)$$

$$\mathrm{Prg}[{<}_X,Y]$$

$$\mathrm{TI}({<}_X,Y)$$

$$\mathrm{WO}(X)$$

$$\mathrm{WOP}(\mathsf{g}):\iff \forall X\left(\mathrm{WO}(X)\to \mathrm{WO}(\mathsf{g}(X))\right)$$

$$\omega$$

$$\mathrm{WOP}({\mathsf{g}}^{\prime })$$

$$\mathsf{g}(X)\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$\mathrm{WOP}(\phi [\mathsf{g}{]}_{\alpha })$$

$$\alpha [\mathsf{g}(c_1),\dots ,\mathsf{g}(c_n)]{<}_{\mathsf{g}(X)}\beta [\mathsf{g}(c_1),\dots ,\mathsf{g}(c_n)]$$

$${\beta }_1,\dots ,{\beta }_n{<}_{{\mathsf{g}}^{\prime }(X)}{\mathsf{g}}^{\prime }(c)$$

$${\omega }^{{\mathsf{g}}^{\prime }(\beta )}$$

$${\mathsf{g}}^{\prime }(0)$$

$${\mathsf{g}}^{\prime }(c+1)$$

$$C(a):\iff M\models \forall Y\left(Prg[{<}_2,Y]\to \forall x{<}_2{\mathsf{g}}^{\prime }(a)Y(x)\right)$$

$${\rm D}_{\mathcal{Q}}(i,n)=\left\{\begin{array}[]{ll}X_{i}(n)&n\in(\mathcal{Q})_{i}\\ \bar{X}_{i}(n)&n\not\in(\mathcal{Q})_{i}\end{array}\right.$$

$$\Gamma ,{\bar{E}}_i(n),E_i(n)$$

$$\Gamma ,L$$

$$\Gamma ,A_0\vee A_1\Gamma ,A_0\vee A_1,A_i\Gamma ,A_0\wedge A_1\text{lx@proof@logical@and}\Gamma ,A_0\Gamma ,A_1\Gamma ,\exists xA(x)\Gamma ,\exists xA(x),A(n)\Gamma ,\forall xA(x)\{\Gamma ,A(n):n<\omega \}$$

$$\Gamma ,\exists YA(Y)\Gamma ,\exists YA(Y),A(X_i)\text{mbox}\Gamma ,\forall YA(Y)\Gamma ,A(Z)$$

$$\Gamma ,E_i(m)\{\Gamma ,E_i(n):n{<}_{i}m\text{mbox}istrue\}$$

$$\Gamma \text{lx@proof@logical@and}\Gamma ,\mathrm{LO}({<}_i)\Gamma ,\forall x{E}_i(x)\exists Y\neg \mathrm{TI}({<}_{{\mathsf{g}}_i},Y),\Gamma$$

$$\Gamma ,E(m)\{\Gamma ,E(n):n\prec m\text{mbox}istrue\}$$

$$\forall xE(x):\alpha \forall xE(x):{\alpha }^{\prime }\{E(m):{\alpha }_m{\}}_{m\in \mathbb{N}}$$

$$n_0\prec \cdots \prec n_{j-1}\prec n_j(=m)\prec n_{j+1}\prec \cdots n_m$$

$${\Gamma }_{n_{j+1}}:{\beta }_{n_{j+1}}{\Gamma }_{n_{j+1}}:{\beta }_{n_{j+1}}^{\prime }\{{\Gamma }_{n_{j+1}},E(n):\beta {\}}_{n\prec n^{\prime }}$$

$${\Gamma }_{n_{j+1}},E(m):\beta$$

$$\forall i{<}_{\omega }m[f(n_{i+1})=f(n_i)+{\omega }^{{\beta }_{n_{i+1}}}]$$

$${⊢}^b\Delta ,\Gamma \text{lx@proof@logical@and}\cdots {⊢}^{c_n}{\Delta }_n,{\Gamma }_n\cdots$$

$${⊢}_0^{{\mathsf{g}}^{\prime }(b)}\Delta ,\Gamma \text{lx@proof@logical@and}\cdots {⊢}_0^{{\mathsf{g}}^{\prime }(c_n)}{\Delta }_n,{\Gamma }_n\cdots$$

$${⊢}^b\Delta ,\Gamma \text{lx@proof@logical@and}{⊢}^{c^{\prime }}\Delta ,\Gamma ,\mathrm{LO}({<}_i){⊢}^c\Delta ,\Gamma ,\forall x{E}_i(x){⊢}^d\Delta ,\Gamma ,\exists Y\neg \mathrm{TI}({<}_{{\mathsf{g}}_i},Y)$$

$${⊢}_0^{{\mathsf{g}}^{\prime }(c)}\Delta ,\forall x{E}_i(x),\Gamma$$

$${⊢}_0^{{\mathsf{g}}^{\prime }(c)}\forall x{E}_i(x)$$

Full text

1 Well-ordering principles

In this note we are concerned with a proof-theoretic strength of a $\Pi^{1}_{2}$-statement ${\rm WOP}({\sf g})$ saying that ‘for any well-ordering $X$, ${\sf g}(X)$ is a well-ordering’, where ${\sf g}:\mathcal{P}(\mathbb{N})\to\mathcal{P}(\mathbb{N})$ is a computable functional on sets $X$ of natural numbers. $\langle n,m\rangle$ denotes an elementary recursive pairing function on $\mathbb{N}$.

Definition 1.1

$X\subset\mathbb{N}$ defines a binary relation $<_{X}:=\{(n,m):\langle n,m\rangle\in X\}$.

[TABLE]

For a functional ${\sf g}:\mathcal{P}(\mathbb{N})\to\mathcal{P}(\mathbb{N})$,

[TABLE]

The theorem due to J.-Y. Girard is a base for further results on the strengths of the well-ordering principles ${\rm WOP}({\sf g})$.

Theorem 1.2

(Girard[3], also cf. [4])*

Over ${\rm RCA}_{0}$, ${\rm ACA}_{0}$ is equivalent to ${\rm WOP}(\lambda X.\omega^{X})$.*

The following theorem summarizes some known results on the strengths of ${\rm WOP}({\sf g})$ for ${\sf g}$ larger than the exponential function. ${\rm ACA}_{0}^{+}$ is an extension of ${\rm ACA}_{0}$ by the axiom of the existence of the $\omega$-th jump of a given set. $\varphi\alpha\beta=\varphi_{\alpha}(\beta)$ denotes the binary Veblen function starting with $\omega^{\alpha}$.

Theorem 1.3

(Marcone and Montalbán[5])* *

Over ${\rm RCA}_{0}$, ${\rm ACA}_{0}^{+}$ is equivalent to ${\rm WOP}(\lambda X.\varepsilon_{X})$. 2. 2.

(H. Friedman)* *

Over ${\rm RCA}_{0}$, ${\rm ATR}_{0}$ is equivalent to ${\rm WOP}(\lambda X.\varphi X0)$.

Theorem 1.3 is proved in [5] computability theoretically. M. Rathjen noticed that the principle ${\rm WOP}({\sf g})$ is tied to the existence of countable coded $\omega$-models.

Definition 1.4

A countable coed $\omega$-model of a second-order arithmetic $T$ is a set $Q\subset\mathbb{N}$ such that $M(Q)\models T$, where $M(Q)=\langle\mathbb{N},\{(Q)_{n}\}_{n\in\mathbb{N}},+,\cdot,0,1,<\rangle$ with $(Q)_{n}=\{m\in\mathbb{N}:\langle n,m\rangle\in Q\}$.

Let $X\in_{\omega}Y:\Leftrightarrow(\exists n[X=(Y)_{n}])$ and $X=_{\omega}Y:\Leftrightarrow(\forall Z(Z\in_{\omega}X\leftrightarrow Z\in_{\omega}Y))$. **

It is not hard to see that over ${\rm ACA}_{0}$, ${\rm ACA}_{0}^{+}$ is equivalent to the fact that there exists an arbitrarily large countable coded $\omega$-model of ${\rm ACA}_{0}$, cf. [1] and Lemma 1.8 below. The fact means that there is a countable coded $\omega$-model $Q$ of ${\rm ACA}_{0}$ containing a given set $X$, i.e., $X=(Q)_{0}$. From this characterization, Afshari and Rathjen[1] gives a purely proof-theoretic proof of Theorem 1.3.1. Their proof is based on Schütte’s method of complete proof search in $\omega$-logic. The proof is extended by Rathjen and Weiermann[7] to give an alternative proof of Theorem 1.3.2. Furthermore Rathjen[6] lifts Theorem 1.3.1 up to $\Gamma$-function and ${\rm ATR}_{0}$ as follows.

Definition 1.5

A continuous and strictly increasing function on ordinals is said to be a normal function.

For a normal function $f$, its derivative $f^{\prime}$ is a normal function enumerating the fixed points of the function $f$. **

The $(\alpha+1)$-th branch $\varphi_{\alpha+1}:\beta\mapsto\varphi_{\alpha+1}(\beta)$ of the Veblen function is the derivative $(\varphi_{\alpha})^{\prime}$ of the previous one $\varphi_{\alpha}$, and for limit $\lambda$, $\varphi_{\lambda}$ enumerates the common fixed points of the functions $\varphi_{\alpha}\,(\alpha<\lambda)$. The $\Gamma$-function $\alpha\mapsto\Gamma_{\alpha}$ is the derivative of the normal function $\alpha\mapsto\varphi\alpha 0$.

Theorem 1.6

(Rathjen[6])*

Over ${\rm RCA}_{0}$, ${\rm WOP}(\lambda X.\Gamma_{X})$ is equivalent to the existence of arbitrarily large countable coded $\omega$-models of ${\rm ATR}_{0}$.*

In view of Theorem 1.2, Theorem 1.3.1 is equivalently stated: over ${\rm RCA}_{0}$, ${\rm WOP}(\lambda X.\varepsilon_{X})$ is equivalent to the existence of arbitrarily large countable coded $\omega$-models of ${\rm WOP}(\lambda X.\omega^{X})$. Moreover relying on 1.3.2, Theorem 1.6 states that over ${\rm RCA}_{0}$, ${\rm WOP}(\lambda X.\Gamma_{X})$ is equivalent to the existence of arbitrarily large countable coded $\omega$-models of ${\rm WOP}(\lambda X.\varphi X0)$. Here is a striking similarity: $\lambda\alpha.\varepsilon_{\alpha}$ is the derivative of the function $\lambda\alpha.\omega^{\alpha}$, and $\lambda\alpha.\Gamma_{\alpha}$ is the one of $\lambda\alpha.\varphi\alpha 0$.

Definition 1.7

$T^{+}$ denotes the extension of a second-order arithmetic $T$ by the axiom stating that

[TABLE]

Note that when $T$ is axiomatized by a $\Pi^{1}_{2}$-sentence over ${\rm RCA}_{0}$, $T^{+}$ is axiomatized by the $\Pi^{1}_{2}$-sentence (1) over ${\rm RCA}_{0}$.

These results suggest us a general fact:

[TABLE]

In this note we confirm it for a variety of normal functions ${\sf g}$. Theorem 1.3.1 follows from (2) for ${\sf g}(\alpha)=\omega^{\alpha}$, and Theorem 1.6 from Theorem 1.3.2 and (2) for ${\sf g}(\alpha)=\varphi_{\alpha}(0)$.

We assume that the normal function ${\sf g}$ enjoys the following conditions. The computability of the functional ${\sf g}$ and the linearity of ${\sf g}(X)$ for linear orderings $X$ are assumed. Moreover ${\sf g}(X)$ is assumed to be a term structure over constants ${\sf g}(c)\,(c\in X)$ and some function symbols $f$. For the term structures ${\sf G}(X)=\left({\sf g}(X),<_{{\sf g}(X)};f,\ldots\right)$ we need two facts: First if $\left(X,<_{X}\right)$ is a substructure of $\left(Y,<_{Y}\right)$, then ${\sf G}(X)$ is a substructure of ${\sf G}(Y)$. Second $\langle{\sf g}(c):c\in X\rangle$ is an indiscernible sequence for ${\sf G}(X)$. These two postulates allow us to extend an order preserving map $f$ between linear orderings $X,Y$ to an order preserving map $F$ between ${\sf g}(X)$ and ${\sf g}(Y)$, cf. Proposition 2.2:

[TABLE]

Moreover we assume that $\left({\sf g}^{\prime}(X);0,+,\lambda\alpha.\omega^{\alpha}\right)$ is a substructure of the term structure ${\sf G}^{\prime}(X)$ for the derivative ${\sf g}^{\prime}$. Then (2) is shown in Theorem 2.4.

Next (2) suggests us a result on common fixed points. Let $\varphi[{\sf g}]_{\alpha}(\beta)$ denote the $\alpha$-th Veblen function starting with $\varphi[{\sf g}]_{0}(\beta)={\sf g}(\beta)$. For $\alpha>0$

[TABLE]

Under a mild condition on the Veblen hierarchy $\{\varphi[{\sf g}]_{\alpha}\}_{\alpha}$, we confirm (3) in Theorem 5.2.

Next consider ${\rm WOP}(\varphi_{\alpha})$ with $\varphi_{\alpha}=\varphi[{\sf g}]_{\alpha}$ for the most familiar ${\sf g}(\beta)=\omega^{\beta}$.

Let ${\rm TJ}(X)$ denote the Turing jump of sets $X$. ${\rm Hier}_{\alpha}(X,Y)$ designates that $\{(Y)_{\beta}\}_{\beta<\alpha}$ is the Turing jump hierarchy starting with $X=(Y)_{0}$ for the least element [math] in the ordering $<$: for any non-zero $\beta<\alpha$, if $\beta=\gamma+1$, then $(Y)_{\beta}={\rm TJ}((Y)_{\gamma})$, and when $\beta$ is limit, $(Y)_{\beta}=\sum_{\gamma<\beta}(Y)_{\gamma}$.

The following Lemma 1.8 is shown in [5], Theorem 1.9, and it yields Theorem 1.3.2.

Lemma 1.8

([5]).

Over ${\rm ACA}_{0}+{\rm WO}(\alpha)$, ${\rm WOP}(\varphi_{\alpha})$ is equivalent to $\forall X\exists Y\,{\rm Hier}_{\omega^{\alpha}}(X,Y)$.

Proof.  It is well known that ${\rm WOP}(\varphi_{\alpha})$ follows from $\forall X\exists Y\,{\rm Hier}_{\omega^{\alpha}}(X,Y)+{\rm WO}(\alpha)$.

Let $A(\alpha):\Leftrightarrow[{\rm WOP}(\varphi_{\alpha})\to\forall X\exists Y\,{\rm Hier}_{\omega^{\alpha}}(X,Y)]$. It suffices to show in ${\rm ACA}_{0}$ that $A(\alpha)$ assuming $A(\beta)$ holds for any $\beta<\alpha$ in any countable coded $\omega$-models of ${\rm ACA}_{0}$. Then ${\rm WO}(\alpha)$ yields $A(\alpha)$.

Assume that $A(\beta)$ holds for any $\beta<\alpha$ in any countable coded $\omega$-models of ${\rm ACA}_{0}$. Suppose ${\rm WOP}(\varphi_{\alpha})$ for $\alpha>0$. Then by (3) we have $(\forall\beta<\alpha{\rm WOP}(\varphi_{\beta}))^{+}$. Given a set $X$, pick a countable coded $\omega$-model $Z$ of $\forall\beta<\alpha{\rm WOP}(\varphi_{\beta})$ such that $X\in_{\omega}Z$. $Z$ is an $\omega$-model of ${\rm ACA}_{0}$ by Theorem 1.2). By the assumption we obtain $\forall\beta<\alpha\forall X\exists!Y\,{\rm Hier}_{\omega^{\beta}}(X,Y)$ in $Z$. Given a set $X$ let $W=\{\langle\gamma,m\rangle:\gamma<\omega^{\alpha},Z\models\exists Y[{\rm Hier}_{\gamma}(X,Y)\land m\in(Y)_{\gamma}]\}$. $W$ is a set by ${\rm ACA}_{0}$. If $\alpha$ is a limit number, then $\forall\beta<\alpha{\rm Hier}_{\omega^{\beta}}(X,W)$ yields ${\rm Hier}_{\omega^{\alpha}}(x,W)$. When $\alpha=\beta+1$, we see by induction on $k<\omega$ that $\forall k<\omega{\rm Hier}_{\omega^{\beta}k}(X,W)$, and hence ${\rm Hier}_{\omega^{\alpha}}(x,W)$. $\Box$

2 Term structures

Let us compare the proof-theoretic strength ${\rm WOP}({\sf g}^{\prime})$ with ${\rm WOP}({\sf g})$ for normal function ${\sf g}$. First of all, both ${\sf g}^{\prime}$ and ${\sf g}$ need to be definable to express formulas ${\rm WOP}({\sf g}^{\prime})$ and ${\rm WOP}({\sf g})$ in $\Pi^{1}_{2}$-formulas. Moreover the fact that ${\sf g}$ sends linear orderings $X$ to linear orderings ${\sf g}(X)$ should be provable in an elementary way. However we need stronger conditions.

${\sf g}$ sends a binary relation $<_{X}$ on a set $X$ to a binary relation $<_{{\sf g}(X)}={\sf g}(<_{X})$ on a set ${\sf g}(X)$. We assume that ${\sf g}(X)$ is a Skolem hull, i.e., a term structure over constants ${\sf g}(c)\,(c\in\{0\}\cup X)$ with the least element [math] in the order $<_{X}$, and some (possibly infinite number of) function symbols $f\in\mathcal{F}$. Let us assume that each function symbol except $+$ has a fixed arity. Some function symbol $f\in\mathcal{F}$ may not be totally defined. In other words $f(\beta_{1},\ldots,\beta_{n})$ may be an illegal expression for $\beta_{1},\ldots,\beta_{n}\in{\sf g}(X)$, i.e., $f(\beta_{1},\ldots,\beta_{n})\not\in{\sf g}(X)$.

Definition 2.1

${\sf g}(X)$ is said to be a computably linear term structure if there are three $\Sigma^{0}_{1}(X)$-formulas ${\sf g}(X),<_{{\sf g}(X)},=$ for which all of the following facts are provable in ${\rm RCA}_{0}$: let $\alpha,\beta,\gamma,\ldots$ range over terms.

1. (a)

(Computability) Each of ${\sf g}(X)$, $<_{{\sf g}(X)}$ and $=$ is $\Delta^{0}_{1}(X)$-definable. ${\sf g}(X)$ is a computable set, and $<_{{\sf g}(X)}$ and $=$ are computable binary relations. 2. (b)

(Congruence) $=$ is a congruence relation on the structure $\langle{\sf g}(X);<_{{\sf g}(X)},f,\ldots\rangle$.

Let us denote ${\sf g}(X)/=$ the quotient set.

In what follows assume that $<_{X}$ is a linear ordering on $X$. 3. (c)

(Linearity) $<_{{\sf g}(X)}$ is a linear ordering on ${\sf g}(X)/=$. 4. (d)

(Increasing) ${\sf g}$ is strictly increasing: $c<_{X}d\Rightarrow{\sf g}(c)<_{{\sf g}(X)}{\sf g}(d)$. 5. (e)

(Continuity) ${\sf g}$ is continuous: Let $\alpha<_{{\sf g}(X)}{\sf g}(c)$ for a limit $c\in X$ and $\alpha\in{\sf g}(X)$. Then there exists a $d<_{X}c$ such that $\alpha<_{{\sf g}(X)}{\sf g}(d)$. 2. 2.

A computably linear term structure ${\sf g}(X)$ is said to be extedible if it enjoys the following two conditions.

1. (a)

(Suborder) If $\langle X,<_{X}\rangle$ is a substructure of $\langle Y,<_{Y}\rangle$, then $\langle{\sf g}(X);=,<_{{\sf g}(X)},f,\ldots\rangle$ is a substructure of $\langle{\sf g}(Y);=,<_{{\sf g}(Y)},f,\ldots\rangle$. 2. (b)

(Indiscernible) $\langle{\sf g}(c):c\in\{0\}\cup X\rangle$ is an indiscernible sequence for linera orderings $\langle{\sf g}(X),<_{{\sf g}(X)}\rangle$: Let $\alpha[{\sf g}(c_{1}),\ldots,{\sf g}(c_{n})],\beta[{\sf g}(c_{1}),\ldots,{\sf g}(c_{n})]\in{\sf g}(X)$ be terms such that constants occurring in them are among the list ${\sf g}(c_{1}),\ldots,{\sf g}(c_{n})$. Then for any increasing sequences $c_{1}<_{X}\ldots<_{X}c_{n}$ and $d_{1}<_{X}\ldots<_{X}d_{n}$

[TABLE]

Proposition 2.2

Suppose ${\sf g}(X)$ is an extendible term structure. Then the following is provable in ${\rm RCA}_{0}$:* Let both $X$ and $Y$ be linear orderings.*

Let $f:\{0\}\cup X\to\{0\}\cup Y$ be an order preserving map, $n<_{X}m\Rightarrow f(n)<_{Y}f(m)\,(n,m\in\{0\}\cup X)$. Then there is an order preserving map $F:{\sf g}(X)\to{\sf g}(Y)$, $n<_{{\sf g}(X)}m\Rightarrow F(n)<_{{\sf g}(Y)}F(m)$.

Proof.  Let $\alpha[{\sf g}(c_{1}),\ldots,{\sf g}(c_{n})]\in{\sf g}(X)$ be a term such that constants occurring in it are among the list ${\sf g}(c_{1}),\ldots,{\sf g}(c_{n})$ for $c_{i}\in\{0\}\cup X$.

Define $F(\alpha[{\sf g}(c_{1}),\ldots,{\sf g}(c_{n})])=\alpha[{\sf g}(f(c_{1})),\ldots,{\sf g}(f(c_{n}))]$. From (2b) on ${\sf g}(X+Y)$, we see that $F$ is an order preserving map from ${\sf g}(X)$ to ${\sf g}(Y)$. Moreover we see that $\alpha[{\sf g}(c_{1}),\ldots,{\sf g}(c_{n})]=\beta[{\sf g}(c_{1}),\ldots,{\sf g}(c_{n})]\Rightarrow F(\alpha[{\sf g}(c_{1}),\ldots,{\sf g}(c_{n})])=F(\beta[{\sf g}(c_{1}),\ldots,{\sf g}(c_{n})])$. $\Box$

Definition 2.3

Suppose that function symbols $+,\omega$ are in the list $\mathcal{F}$ of function symbols for a computably linear term structure ${\sf g}(X)$. Let $1:=\omega^{0}$, and $2:=1+1$, etc.

${\sf g}(X)$ is said to be an exponential term structure (with respect to function symbols $+,\omega$) if all of the followings are provable in ${\rm RCA}_{0}$.

[math] is the least element in $<_{{\sf g}(X)}$, and $\alpha+1$ is the successor of $\alpha$. 2. 2.

$+$ and $\omega$ enjoy some familiar conditions.

1. (a)

$\alpha<_{{\sf g}(X)}\beta\to\omega^{\alpha}+\omega^{\beta}=\omega^{\beta}$. 2. (b)

$\gamma+\lambda=\sup\{\gamma+\beta:\beta<\lambda\}$ when $\lambda$ is a limit number, i.e., $\lambda\neq 0$ and $\forall\beta<_{{\sf g}(X)}\lambda(\beta+1<_{{\sf g}(X)}\lambda)$. 3. (c)

$\beta_{1}<_{{\sf g}(X)}\beta_{2}\to\alpha+\beta_{1}<_{{\sf g}(X)}\alpha+\beta_{2}$, and $\alpha_{1}<_{{\sf g}(X)}\alpha_{2}\to\alpha_{1}+\beta\leq_{{\sf g}(X)}\alpha_{2}+\beta$. 4. (d)

$(\alpha+\beta)+\gamma=\alpha+(\beta+\gamma)$. 5. (e)

$\alpha<_{{\sf g}(X)}\beta\to\exists\gamma\leq_{{\sf g}(X)}\beta(\alpha+\gamma=\beta)$. 6. (f)

Let $\alpha_{n}\leq_{{\sf g}(X)}\cdots\leq_{{\sf g}(X)}\alpha_{0}$ and $\beta_{m}\leq_{{\sf g}(X)}\cdots\leq_{{\sf g}(X)}\beta_{0}$. Then $\omega^{\alpha_{0}}+\cdots+\omega^{\alpha_{n}}<_{{\sf g}(X)}\omega^{\beta_{0}}+\cdots+\omega^{\beta_{m}}$ iff either $n<m$ and $\forall i\leq n(\alpha_{i}=\beta_{i})$, or $\exists j\leq\min\{n,m\}[\alpha_{j}<_{{\sf g}(X)}\beta_{j}\land\forall i<j(\alpha_{i}=\beta_{i})]$. 3. 3.

Each $f(\beta_{1},\ldots,\beta_{n})\in{\sf g}(X)\,(f\in\mathcal{F})$ as well as ${\sf g}(c)\,(c\in\{0\}\cup X)$ is closed under $+$. In other words the terms $f(\beta_{1},\ldots,\beta_{n})$ and ${\sf g}(c)$ denote additively closed ordinals (additive principal numbers) when $<_{{\sf g}(X)}$ is a well ordering.

In what follows we assume that ${\sf g}(X)$ is an extendible term structure, and ${\sf g}^{\prime}(X)$ is an exponential term structure. Constants in the term structure ${\sf g}^{\prime}(X)$ are ${\sf g}^{\prime}(c)$ for $c\in\{0\}\cup X$, and function symbols in $\mathcal{F}\cup\{0,+\}\cup\{{\sf g}\}$ with a unary function symbol ${\sf g}$. When $\mathcal{F}=\emptyset$, let $\omega^{\alpha}:={\sf g}(\alpha)$. Otherwise we assume that $\omega$ is in the list $\mathcal{F}$. Furthermore assume that ${\rm RCA}_{0}$ proves that

[TABLE]

where ${\sf g}^{n}$ denotes the $n$-th iterate of the function ${\sf g}$, and we are assuming in the last that the successor element $c+1$ of $c$ in $X$ exists. Note that the last two in (5) are true for normal functions ${\sf g}$ when ${\sf g}(0)>0$.

Assume that $<_{X}$ is a linear ordering. Each non-zero term $\beta\in{\sf g}^{\prime}(X)$ is written as a Cantor normal form $\beta=\beta_{1}+\cdots+\beta_{n}$ where $\beta_{n}\leq_{{\sf g}^{\prime}(X)}\ldots\leq_{{\sf g}^{\prime}(X)}\beta_{1}$ and each $\beta_{i}$ is an $f$-term $f(\gamma_{1},\ldots,\gamma_{m})$ with $f\in\mathcal{F}$ or ${\sf g}^{\prime}(c)$. Using the Cantor normal form, we can define the natural (commutative) sum $\alpha\#\beta$ of terms $\alpha,\beta\in{\sf g}^{\prime}(X)$ which enjoys $\alpha\#\beta=\beta\#\alpha$ and $\alpha_{1}<_{{\sf g}^{\prime}(X)}\alpha_{2}\Rightarrow\alpha_{1}\#\beta<_{{\sf g}^{\prime}(X)}\alpha_{2}\#\beta$.

Theorem 2.4

Let ${\sf g}(X)$ be an extendible term structure, and ${\sf g}^{\prime}(X)$ an exponential term structure for which (5) holds.

Then the following two are mutually equivalent over ${\rm ACA}_{0}$:

${\rm WOP}({\sf g}^{\prime})$. 2. 2.

$\left({\rm WOP}({\sf g}^{\prime})\right)^{+}:\Leftrightarrow\forall X\exists Y[X\in Y\land M_{Y}\models{\rm WOP}({\sf g})]$. Namely there exists an arbitrarily large countable coded $\omega$-model of ${\rm WOP}({\sf g})$.

First let us show the easy half. Let sets $X,U$ be given such that ${\rm WO}(<_{0})$ for $<_{0}=<_{X}$. We have ${\rm LO}(<_{{\sf g}^{\prime}(X)})$. Pick a countable coded $\omega$-model $M$ of ${\rm WOP}({\sf g})$ such that $X,U\in M$. Then ${\sf g}(X),{\sf g}^{\prime}(X)\in M$. Let $<_{1}$ be obtained from $<_{0}$ by adding the largest element $\alpha$. This means that $a<_{1}\alpha$ for any $a$ in the field of $<_{0}$. We have ${\rm WO}(<_{1})$ by ${\rm WO}(<_{0})$. We show $Prg[<_{1},C(a)]$ for an arithmetical formula

[TABLE]

for $<_{2}=<_{{\sf g}^{\prime}(<_{1})}$. This yields $C(\alpha)$. Since by (5), $x<_{2}{\sf g}^{\prime}(\alpha)$ for any $x$ in the field of $<_{{\sf g}^{\prime}(X)}=<_{{\sf g}^{\prime}(<_{0})}$, we obtain $M\models\forall Y\left(Prg[<_{{\sf g}^{\prime}(X)},Y]\to\forall x\in{\rm fld}({\sf g}^{\prime}(X))\,Y(x)\right)$. Hence we obtain $M\models\left(Prg[<_{{\sf g}^{\prime}(X)},U]\to\forall x\in{\rm fld}({\sf g}^{\prime}(X))\,U(x)\right)$, i.e., ${\rm TI}(<_{{\sf g}^{\prime}(X)},U)$. Since $U$ is an arbitrary set, we conclude ${\rm WO}(<_{{\sf g}^{\prime}(X)})$.

It remains to show that $Prg[<_{1},C(a)]$. When $a$ is a limit element, this follows from the continuity of the function ${\sf g}^{\prime}(a)$. Assuming $C(a)$, let us show $C(a+1)$. Argue in the model $M$. Suppose $Prg[<_{2},Y]$ and $x<_{2}{\sf g}^{\prime}(a+1)=\sup_{n}{\sf g}^{n}({\sf g}^{\prime}(a)+1)$ by (5). By induction on $n<\omega$ we see that $\forall x<_{2}{\sf g}^{n}({\sf g}^{\prime}(a)+1)\,Y(x)$ using ${\rm WOP}({\sf g})$ and $C(a)$, i.e., ${\rm WO}(<_{2}\!\upharpoonright\!({\sf g}^{\prime}(a)+1))$. Hence we obtain $C(a+1)$. $C(0)$ is seen similarly.

3 Proof search

Conversely assume ${\rm WOP}({\sf g}^{\prime})$. We need to find a countable coded $\omega$-model of ${\rm WOP}({\sf g})$. The idea in [1, 6, 7] is to search a derivation of the negation of ${\rm WOP}({\sf g})$ in $\omega$-logic. Construct a locally correct $\omega$-branching tree in a canonical way. If the search results in a fail, i.e., if the constructed tree is not well-founded, then we can believe in the consistency of ${\rm WOP}({\sf g})$ in $\omega$-logic. In fact we can find a countable coded $\omega$-model of ${\rm WOP}({\sf g})$ from an infinite path through the tree. Otherwise the tree is well-founded, i.e., a derivation in a depth $\alpha$. It turns out that the derivation can be converted to a cut-free deduction with the empty sequent at its root, and in depth bounded by ${\sf g}^{\prime}(\alpha)$. Then by our assumption ${\rm WOP}({\sf g}^{\prime})$, the deduction is well-founded, i.e., a derivation of the empty sequent. We see that this is not the case by transfinite induction up to ${\sf g}^{\prime}(\alpha)$. This shows the consistency of ${\rm WOP}({\sf g})$ in $\omega$-logic based on ${\rm WOP}({\sf g}^{\prime})$. Now details follows.

Let $\mathcal{Q}\subset\mathbb{N}$ be a given set, which is viewed as a family $\{(\mathcal{Q})_{i}:i<\omega\}$ of sets of natural numbers. The language $\mathcal{L}_{\omega}$ here consists of function symbols for elementary recursive functions including [math] and the successor $S$, predicate symbols $=,\neq$ and unary predicate variables $\{X_{i},E_{i}:i<\omega\}$ and their compliments $\bar{X}_{i},\bar{E}_{i}$. Let us write $n<_{i}m$ for $n<_{X_{i}}m$, i.e., for $X_{i}(\langle n,m\rangle)$, and $n<_{{\sf g}_{i}}m$ for $n<_{{\sf g}(X_{i})}m$. Each $E_{i}$ is a fresh variable expressing the well foundedness ${\rm TI}(<_{i},E_{i})$ of the relation $<_{i}$. Recall that each closed term $t$ is identified with its value $t^{\mathbb{N}}$, a numeral.

[TABLE]

and ${\rm Diag}(\mathcal{Q})=\{{\rm D}_{\mathcal{Q}}(i,n):i,n\in\mathbb{N}\}$.

A true literal is one of the form $t_{0}=t_{1}\,(t_{0}^{\mathbb{N}}=t_{1}^{\mathbb{N}})$, $s_{0}\neq s_{1}\,(s_{0}^{\mathbb{N}}\neq s_{1}^{\mathbb{N}})$, and ${\rm D}_{\mathcal{Q}}(i,n)$ for $i,n<\omega$.

Axioms in \mbox{\boldmathG}(\mathcal{Q})+(prg)+(W) are

[TABLE]

and for true literals $L$

[TABLE]

Inference rules are in \mbox{\boldmathG}(\mathcal{Q})+(prg)+(W).

[TABLE]

$(\exists^{2})$ for $i<\omega$ and $(\forall^{2})$ with an eigenvariable $Z$

[TABLE]

and the following two for $i,m<\omega$:

[TABLE]

where by saying that $n<_{i}m$ is true we mean $\langle n,m\rangle\in(\mathcal{Q})_{i}$.

[TABLE]

Let us construct a tree ${\cal T}\subset{}^{<\omega}\omega$ recursively as follows. For $a\in{\cal T}$, $Seq(a)$ is a label attached with the node $a$, which is a sequent at $a$. First put the empty sequent at the root $\emptyset$. Leaf condition on the tree runs: If $Seq(a)$ is an axiom in \mbox{\boldmathG}(\mathcal{Q}), then $a$ is a leaf in ${\cal T}$. The construction is divided to three. Suppose that the tree ${\cal T}$ has been constructed up to a node $a\in{}^{<\omega}\omega$.

Case 0. $lh(a)=3i$ for an $i\geq 0$: Apply the inference $(W)_{i}$ backwards.

Case 1. $lh(a)=3i+1$: Apply one of inferences $(\lor),(\land),(\exists),(\forall\omega),(\exists^{2})$ if it is possible. Otherwise repeat.

Case 2. $lh(a)=3\langle n,i\rangle+2$ for $n,i<\omega$: Apply the inference $(prg)_{i}$ backwards if it is possible. Otherwise repeat.

If the tree ${\cal T}$ is not well-founded, then let $\mathcal{P}$ be an infinite path through ${\cal T}$. Let $(M)_{i}\subset\mathbb{N}$ be a set such that for any $n\in\mathbb{N}$, $(X_{i}(n))\in\mathcal{P}\Rightarrow n\not\in(M)_{i}$ and $(\bar{X}_{i}(n))\in\mathcal{P}\Rightarrow n\in(M)_{i}$. Then for any $n$ for which one of $X_{i}(n),\bar{X}_{i}(n)$ is in $\mathcal{P}$, we obtain $n\in(\mathcal{Q})_{i}\Leftrightarrow n\in(M)_{i}$. For other $n$, $n\in(M)_{i}$ is arbitrarily determined for $i\neq 0$: set $(M)_{0}:=(\mathcal{Q})_{0}$.

$M$ is shown to be a countable coded $\omega$-model of ${\rm WOP}({\sf g})$ as follows. The search procedure is fair, i.e., each formula is eventually analyzed on every path as in [1, 6, 7]. We see from the fairness that $M\not\models A$ by induction on the number of occurrences of logical connectives in formulas $A$ on the path $\mathcal{P}$.

4 Cut elimination

In what follows assume that ${\cal T}$ is well founded. Since we are working in ${\rm ACA}_{0}$, we know that the Kleene-Brouwer ordering $<_{KB}$ on ${\cal T}$ is a well-ordering, cf. [8]. Let $\Lambda=otp(<_{KB})$ denote the order type of the well-ordering $<_{KB}$. We have ${\rm WO}({\sf g}^{\prime}(\Lambda))$ by ${\rm WOP}({\sf g}^{\prime})$ and ${\rm WO}(\Lambda)$.

For $b<\Lambda$ let us write $\vdash^{b}\Gamma$ when there exists a derivation of $\Gamma$ in \mbox{\boldmathG}(\mathcal{Q})+(prg)+(W) whose depth is bounded by $b$. On the other side for $\alpha<{\sf g}^{\prime}(\Lambda)$, $\vdash^{\alpha}_{0}\Gamma$ designates that there exists a derivation of $\Gamma$ in \mbox{\boldmathG}(\mathcal{Q})+(prg) of depth $\alpha$. In the derivation no inference $(W)_{i}$ occurs. Specifically for a function $\pi$ on ${}^{<\omega}\omega$, $\pi\vdash^{\alpha}_{0}\Gamma$ designates that there exists a derivation of the sequent $\Gamma$ in \mbox{\boldmathG}(\mathcal{Q})+(prg) with the repetition rule $(Rep)$ in depth $\alpha$, and this fact is witnessed by the function $\pi$. The last means the following. For each $a\in{}^{<\omega}\omega$, either $\pi(a)=*$ designating that $a$ is not in the naked tree for the derivation, or $\pi(a)=(Seq(a),Rule(a),Mfml(a),Sfml(a),ord(a))$, where $Seq(a)$ denotes the sequent at the node $a$, $Rule(a)$ the inference rule whose lower sequent is $Seq(a)$, $Mfml(a)$ is the main (principal) formula of $Rule(a)$, $Sfml(a)$ the minor (auxiliary or side) formulas of $Rule(a)$ and $ord(a)<\Lambda$.

The following Theorem 4.1 is due to G. Takeuti[9, 10]111Actually Takeuti proved a similar result when we have in hand a finite proof figure of transfinite induction in PA. Under the assumption we can take an order preserving map $f$ elementarily recursive in the ordering, cf. [2]..

Theorem 4.1

The following is provable in ${\rm RCA}_{0}+{\rm WO}(\alpha)$:*

Suppose that $\prec$ is a linear ordering with the least element [math], and $<$ denotes the well-ordering up to $\omega^{\alpha}$. $(prg)_{\prec}$ denotes the sequent calculus with inference rules $(prg)_{\prec}$ and the repetition rule $(Rep)$.*

[TABLE]

Suppose $\pi\vdash_{0}^{\alpha}\forall x\,E(x)$. Then there exists an embedding $f$ such that $n\prec m\Rightarrow f(n)<f(m)$, $f(m)<\omega^{\alpha}$ for any $n,m$, and $f$ is $\alpha$-recursive in the function $\pi$ and the relations $\prec,<$.

Proof.  Let us write $\Gamma:\alpha$ for $\vdash^{\alpha}_{0}\Gamma$, and $<_{\omega}$ for the usual $\omega$-ordering in the proof. First search the $\omega$-rule $(\forall\omega)$ nearest to the root in the derivation $\pi$:

[TABLE]

where $\alpha_{m}<\alpha^{\prime}\leq\alpha$ and there are some (possibly none) $(Rep)$’s below the $(\forall\omega)$. Such an $(\forall\omega)$ exists by ${\rm WO}(\alpha)$. By induction on $m$, we define a derivation $\rho_{m}$ of $\Gamma_{m}:\beta_{m}$ for a finite set $\Gamma_{m}\subset\{E(n):n\in\mathbb{N}\}$ such that $E(m)\in\Gamma_{m}$ and $\forall n[E(n)\in\Gamma_{m}\Rightarrow m\preceq n]$ as follows. If $\forall n<_{\omega}m(n\prec m)$, then $\rho_{m}=\pi_{m}$ and $\beta_{m}=\alpha_{m}$. Otherwise let

[TABLE]

with $\{n_{i}:i\leq m\}=\{0,\ldots,m\}$ and $j<_{\omega}m$.

Search the nearest inference $(prg)_{\prec}$ in $\rho_{n_{j+1}}$:

[TABLE]

where $\beta<\beta_{n_{j+1}}^{\prime}\leq\beta_{n_{j+1}}$, $E(n^{\prime})\in\Gamma_{n_{j+1}}$ is the main formula of the inference $(prg)_{\prec}$. We have $m\prec n_{j+1}\preceq n^{\prime}$. Define $\rho_{m}$ be the following

[TABLE]

with $\beta_{m}=\beta<\beta_{n_{j+1}}$.

Define a function $f(m)$ by induction on $m$ as follows. $f(0)=\omega^{\beta_{0}}=\omega^{\alpha_{0}}$ for the least element [math] with respect to $\prec$. For $m\neq 0$, $f(m)=f(n_{j-1})+\omega^{\beta_{m}}$ with the largest element $n_{j-1}<_{\omega}m$ with respect to $\prec$ in (6). Let us show that $f$ is a desired embedding. In (6), it suffices to show by induction on $m$ that

[TABLE]

First by the definition of $f$ we have $f(m)=f(n_{j-1})+\omega^{\beta_{m}}$ with $m=n_{j}$. On the other hand we have $f(m)+\omega^{\beta_{n_{j+1}}}=f(n_{j-1})+\omega^{\beta_{m}}+\omega^{\beta_{n_{j+1}}}=f(n_{j-1})+\omega^{\beta_{n_{j+1}}}=f(n_{j+1})$ by $\beta_{m}<\beta_{n_{j+1}}$ and IH. This shows (7), and our proof is completed. $\Box$

Let us call a sequent $\Delta$ an E-sequent if $\Delta\subset\{\forall x\,E_{i}(x),E_{i}(n):i,n<\omega\}$. An $E$-free formula is a formula in which no $E_{i}$ occurs.

Lemma 4.2

For an $E$-sequent $\Delta$ and an $E$-free sequent $\Gamma$, if $\vdash^{b}\Delta,\Gamma$ for $b<\Lambda$, then $\vdash^{{\sf g}^{\prime}(b)}_{0}\Delta,\Gamma$.

Proof by induction on $b<\Lambda$.

Case 1. $\Delta,\Gamma$ is an axiom: There is nothing to prove.

Case 2. $\Delta,\Gamma$ is a lower sequent of an inference such that its principal formula is in $\Delta\cup\Gamma$:

[TABLE]

By IH we have $\vdash^{{\sf g}^{\prime}(c_{n})}_{0}\Delta_{n},\Gamma_{n}$. From ${\sf g}^{\prime}(c_{n})<{\sf g}^{\prime}(b)$ we obtain

[TABLE]

When there is no upper sequents, i.e., when $(E_{i}(m))\in\Delta$ with the minimal $m$ with respect to $<_{i}$, we have $\vdash^{0}_{0}\Delta,\Gamma$.

Case 3. $\Delta,\Gamma$ is a lower sequent of an inference $(W)_{i}$.

[TABLE]

where $c^{\prime},c,d<b$.

If ${\rm LO}(<_{i})$ is false, i.e., $<_{(\mathcal{Q})_{i}}$ is not a linear ordering, then we see that $\vdash^{c^{\prime}}\Delta,\Gamma$ with $c^{\prime}<b$. IH yields the assertion.

In what follows assume that $<_{(\mathcal{Q})_{i}}$ is a linear ordering. By IH we have for the $E$-sequent $\Delta\cup\{\forall x\,E_{i}(x)\}$

[TABLE]

If $\vdash^{{\sf g}^{\prime}(c)}_{0}\Delta,\Gamma$, then we obtain the assertion. Assume that this is not the case. Then we claim that

[TABLE]

This is seen by induction on ${\sf g}^{\prime}(c)<{\sf g}^{\prime}(\Lambda)$ as follows. If $\Delta,\forall x\,E_{i}(x),\Gamma$ is an axiom, then so is $\Gamma$, i.e., either a true literal is in $\Gamma$ or $\{L,\bar{L}\}\subset\Gamma$ for a literal $L$. Then $\vdash^{{\sf g}^{\prime}(c)}_{0}\Delta,\Gamma$. Next assume that $\Delta,\forall x\,E_{i}(x),\Gamma$ is derived by an inference whose principal formula is in $\Delta\cup\Gamma$.

[TABLE]

We can assume that there exists an $n$ for which $\vdash^{b_{n}}_{0}\Delta_{n},\Gamma_{n}$ does not hold. By IH we obtain $\vdash^{b_{n}}_{0}\forall x\,E_{i}(x)$. Finally let

[TABLE]

We can assume that $\vdash^{b_{n}}_{0}\Delta,\Gamma$ does not hold for any $n$. Then we show that $\vdash^{b_{n}}_{0}E_{i}(n)$ holds for any $n$ by induction on $b_{n}$. Consider the case

[TABLE]

By IH we see that $\vdash^{a_{n}}_{0}E_{i}(n)$ for any $n<_{i}m$. Thus (8) is shown.

Let $\beta_{0}={\sf g}^{\prime}(c)$. By Theorem 4.1 there is an embedding $f$ such that $n<_{i}m\Rightarrow f(n)<f(m)$, $f(m)<\omega^{\beta_{0}}$ for any $n,m$, and $f$ is $\beta_{0}$-recursive in the computable function $\pi$ for the derivation witnessing the fact (8) and the relations $<_{i},<$.

By Proposition 2.2 let $F$ be an order preserving map from ${\sf g}(<_{i})$ to $<$: $n<_{{\sf g}_{i}}m\Rightarrow F(n)<F(m)$, $F(m)<{\sf g}(\omega^{\beta_{0}})$, and $F$ is computable from $f$.

The following shows that $\vdash^{G(m)+3}_{0}\lnot Prg[<_{{\sf g}_{i}},Z],E(m)$ with a fresh variable $Z$ and $G(m)=\omega+1+4F(m)$ by induction on $F(m)$:

[TABLE]

where $n\not<_{{\sf g}_{i}}m$ denotes the formula $\lnot({\sf g}(X_{i}))(\langle n,m\rangle)$, which is a $\Delta_{1}$-formula in $X_{i}$. Thus for $G(m)+3<{\sf g}(\omega^{\beta_{0}})$ we obtain

[TABLE]

On the other hand we have by IH $\vdash^{{\sf g}^{\prime}(d)}_{0}\Delta,\Gamma,\exists Y\lnot{\rm TI}(<_{{\sf g}_{i}},Y)$ for the $E$-free sequent $\Gamma\cup\{\exists Y\lnot{\rm TI}(<_{{\sf g}_{i}},Y)\}$. By cut-elimination we obtain $\vdash_{0}^{\beta_{1}}\Delta,\Gamma$ for $\beta_{1}=\omega_{k}({\sf g}(\omega^{\beta_{0}})\#3\#{\sf g}^{\prime}(d))$ for a $k<\omega$ depending only on the formula $\forall Y{\rm TI}(<_{{\sf g}_{i}},Y)$. Now $\beta_{1}=\omega_{k}({\sf g}(\omega^{{\sf g}^{\prime}(c)})\#3\#{\sf g}^{\prime}(d))<{\sf g}^{\prime}(b)$ since $c,d<b$ and ${\sf g}^{\prime}(b)$ is closed under $+,\omega$ and ${\sf g}$ by (5). $\Box$

Let us finish our proof of the harder direction in Theorem 2.4. By our assumption we have $\vdash^{b}\emptyset$ for a $b<\Lambda$ and the empty sequent $\emptyset$. Lemma 4.2 yields $\vdash^{{\sf g}^{\prime}(b)}_{0}\emptyset$. We see that this is not the case by induction on ${\sf g}^{\prime}(b)<{\sf g}^{\prime}(\Lambda)$. Therefore the tree ${\cal T}$ is not well founded.

Finally let us spend a few words on a formalization of the above proof in ${\rm ACA}_{0}$. In the proof one can agree that each infinite derivation is a computable function $\pi$ on the set of finite sequences $a$ of natural numbers. $\pi(a)$ is a bunch of data as described before Theorem 4.1. $\vdash^{\alpha}\Gamma$ denotes the fact that there exists a computable function $\pi$ such that $Seq(\emptyset)=\Gamma$ and $ord(\emptyset)=\alpha$ for the empty sequence $\emptyset$, i.e., the root of the derivation tree. $\vdash^{\alpha}\Gamma$ is arithmetically definable, defined by a $\Sigma^{0}_{3}$-formula. The above proof of Lemma 4.2 is formalizable in ${\rm ACA}_{0}$ with the assumption ${\rm WO}({\sf g}^{\prime}(\Lambda))$.

Remark 4.3

We can show one of equivalences due to Girard[3] in the spirit of Rathjen[1, 6, 7]: ${\rm ACA}_{0}$ is equivalent to ${\rm WFP}(\lambda X.2^{X})$ over ${\rm RCA}_{0}$, where ${\rm WFP}({\sf g}):\Leftrightarrow\forall X\left({\rm WF}(X)\to{\rm WF}({\sf g}(X))\right)$ with ${\rm WF}(X):\Leftrightarrow\forall Y\,{\rm TI}(<_{X},Y)$.

The direction ${\rm ACA}_{0}\to{\rm WFP}(\lambda X.2^{X})$ is well known. The reverse direction is seen as follows. Consider the proof search of the contradiction in a sequent calculus \mbox{\boldmathG}(\mathcal{Q})+(Jcut)+(J). Pick a fresh unary predicate symbol $J$. Let $\exists x\,B(x,y)$ be a fixed $\Sigma_{1}$-formula. \mbox{\boldmathG}(\mathcal{Q})+(Jcut)+(J) is obtained from the sequent calculus \mbox{\boldmathG}(\mathcal{Q}) by adding the following three inference rules $(Jcut),(J),(\bar{J})$.

[TABLE]

$J(n)$ is intended to denote $\exists x\,B(x,n)$. If the tree in the proof search is not well founded, then an infinite path through the tree yields a set $\mathcal{J}$ such that $\forall n[n\in\mathcal{J}\leftrightarrow\exists x\,B(x,n)]$. Thus ${\rm ACA}_{0}$ follows. Suppose contrarily that the tree is well founded, and let $\Lambda$ be the depth of the well founded tree. Then a cut elimination yields a cut-free derivation of the empty sequent in \mbox{\boldmathG}(\mathcal{Q}) in depth $2_{c}(\Lambda)$ for a constant $c$ depending only on the $\Delta_{0}$-formula $B$. From ${\rm WFP}(\lambda X.2^{X})$ we see that the cut-free derivation is well founded, and this is not the case. **

5 Common fixed points

Let $\alpha$ be the order type of a computable well ordering on $\mathbb{N}$. $\varphi[{\sf g}]_{\alpha}(\beta)$ denotes the $\alpha$-th Veblen function starting with $\varphi[{\sf g}]_{0}\beta={\sf g}(\beta)$.

We assume that $\varphi[{\sf g}]_{\alpha}(X)$ is a term structure over constants $\{\varphi[{\sf g}]_{\alpha}(c):c\in X\cup\{0\}\}$ and unary function symbols $\varphi[{\sf g}]_{\beta}\,(\beta<\alpha)$ and the addition $+$. Also a function symbol for the exponential $\omega^{\beta}$ is included when $\varphi[{\sf g}]_{0}={\sf g}$ is not the exponential.

In what follows we assume that each term structure $\varphi[{\sf g}]_{\beta}(X)\,(\beta<\alpha)$ is extendible, and $\varphi[{\sf g}]_{\alpha}$ is exponential. Moreover we assume that the followings are provable in ${\rm RCA}_{0}$, cf. (5).

[TABLE]

We see the following as in Proposition 2.2.

Proposition 5.1

Suppose $\varphi[{\sf g}]_{\beta}(X)$ is an extendible term structure. Then the following is provable in ${\rm RCA}_{0}$:* Let both $X$ and $Y$ be linear orderings.*

Let $f:\{0\}\cup X\to\{0\}\cup Y$ be an order preserving map, $n<_{X}m\Rightarrow f(n)<_{Y}f(m)\,(n,m\in\{0\}\cup X)$. Then there is an order preserving map $F:\varphi[{\sf g}]_{\beta}(X)\to\varphi[{\sf g}]_{\beta}(Y)$, $n<_{\varphi[{\sf g}]_{\beta}(X)}m\Rightarrow F(n)<_{\varphi[{\sf g}]_{\beta}(Y)}F(m)$.

Theorem 5.2

Let each term structure $\varphi[{\sf g}]_{\beta}(X)\,(\beta<\alpha)$ be extendible, and $\varphi[{\sf g}]_{\alpha}$ is exponential for which (9) holds. Then the following two are mutually equivalent over ${\rm ACA}_{0}+{\rm LO}(\alpha)$ for $\alpha>0$.

${\rm WOP}(\varphi[{\sf g}]_{\alpha})$. 2. 2.

$\left(\forall\beta<\alpha{\rm WOP}(\varphi[{\sf g}]_{\beta})\right)^{+}$.

The easier direction states that ${\rm WOP}(\varphi[{\sf g}]_{\alpha})$ follows from $\left(\forall\beta<\alpha{\rm WOP}(\varphi[{\sf g}]_{\beta})\right)^{+}$, and it follows from the fact (9).

The harder direction is seen as in Theorem 2.4 by slight modifications. Suppose ${\rm WOP}(\varphi[{\sf g}]_{\alpha})$ and ${\rm LO}(\alpha)$ for $\alpha>0$. Replace the inference rule $(W)_{i}$ by

[TABLE]

where $\beta<\alpha$ and $n<_{i,\beta}m:\Leftrightarrow n<_{\varphi[{\sf g}]_{\beta}(<_{i})}m$.

Construct fairly a tree in the sequent calculus \mbox{\boldmathG}(\mathcal{Q})+(prg)+\{(W)_{\beta}\}_{\beta<\alpha} ending with the empty sequent. When the tree is not well founded, an infinite path through the tree yields a countable coded $\omega$-model of $\forall\beta<\alpha{\rm WOP}(\varphi[{\sf g}]_{\beta})$.

Suppose that the search tree ${\cal T}$ is well founded with its order type $\Lambda$ in the Kleene-Brouwer ordering. We obtain ${\rm WO}(\varphi[{\sf g}]_{\alpha}(\Lambda))$ by ${\rm WOP}(\varphi[{\sf g}]_{\alpha})$. As in Lemma 4.2 we see the following Lemma 5.3 from Proposition 5.1 and (9): $c,d<b\,\&\,\beta<\alpha\Rightarrow\omega_{k}(\varphi[{\sf g}]_{\beta}(\omega^{\varphi[{\sf g}]_{\alpha}(c)})\#3\#\varphi[{\sf g}]_{\alpha}(d))<\varphi[{\sf g}]_{\alpha}(b)$

Lemma 5.3

For an $E$-sequent $\Delta$ and an $E$-free sequent $\Gamma$, if $\vdash^{b}\Delta,\Gamma$ for $b<\Lambda$, then $\vdash^{\varphi[{\sf g}]_{\alpha}(b)}_{0}\Delta,\Gamma$.

The harder direction in Theorem 5.2 is concluded as follows. By our assumption we have $\vdash^{b}\emptyset$ for a $b<\Lambda$ and the empty sequent $\emptyset$. Lemma 5.3 yields $\vdash^{\varphi[{\sf g}]_{\alpha}(b)}_{0}\emptyset$. We see that this is not the case by induction on $\varphi[{\sf g}]_{\alpha}(b)<\varphi[{\sf g}]_{\alpha}(\Lambda)$. Therefore the tree ${\cal T}$ is not well founded.