
\section{Introduction}

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 the elementary recursive pairing function 
$\langle n,m\rangle=\frac{(n+m)(n+m+1)}{2}+m$ on $\mathbb{N}$.

\begin{definition}
{\rm
$X\subset\mathbb{N}$ defines a binary relation 
$<_{X}:=\{(n,m): \langle n,m\rangle\in X\}$.
\begin{eqnarray*}
{\rm Prg}[<_{X},Y] & :\Leftrightarrow & \forall m\left(\forall n<_{X}m\,Y(n)\to Y(m)\right)
\\
{\rm TI}[<_{X},Y] & :\Leftrightarrow & {\rm Prg}[<_{X},Y] \to\forall n\, Y(n)
\\
{\rm TI}[<_{X}] & :\Leftrightarrow & \forall Y\,{\rm TI}[<_{X},Y]
\\
{\rm WO}(X) & :\Leftrightarrow & {\rm LO}(X) \land {\rm TI}[<_{X}]
\end{eqnarray*}
where ${\rm LO}(X)$ denotes a $\Pi^{0}_{1}$-formula stating that $<_{X}$ is a linear ordering.

For a functional ${\sf g}: \mathcal{P}(\mathbb{N})\to\mathcal{P}(\mathbb{N})$,
\[
{\rm WOP}({\sf g}) :\Leftrightarrow \forall X\left( {\rm WO}(X)\to {\rm WO}({\sf g}(X)) \right)
\]
}
\end{definition}

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})$.
For second order arithmetics ${\rm RCA}_{0}$, ${\rm ACA}_{0}$, etc. see \cite{Simpson}.
For a set $X\subset\mathbb{N}$, $\omega^{X}$ denotes an ordering on $\mathbb{N}$ canonically defined
such that its order type is $\omega^{\alpha}$ when $<_{X}$ is a well-ordering of type $\alpha$.

\begin{theorem}\label{th:Girardp.299}{\rm (Girard\cite{Girard})}
\\
Over ${\rm RCA}_{0}$, ${\rm ACA}_{0}$ is equivalent to ${\rm WOP}(\lambda X.\omega^{X})$.
\end{theorem}

In the following theorem 
${\rm ACA}_{0}^{+}$ denotes an extension of ${\rm ACA}_{0}$ by the axiom of the existence of
the $\omega$-th jump of a given set.

\begin{theorem}\label{th:MontalbanMarcone}{\rm (Marcone and Montalb\'an\cite{MontalbanMarcone})}
Over ${\rm RCA}_{0}$, ${\rm ACA}_{0}^{+}$ is equivalent to ${\rm WOP}(\lambda X.\varepsilon_{X})$.
\end{theorem}

Theorem \ref{th:MontalbanMarcone} is proved
in \cite{MontalbanMarcone} computability theoretically.
M. Rathjen noticed that the principle ${\rm WOP}({\sf g})$ is tied to the existence of
\textit{countable coded $\omega$-models}.

\begin{definition}
{\rm
A \textit{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))$.
}
\end{definition}
It is not hard to see that over ${\rm ACA}_{0}$,
the existence of the $\omega$-th jump is equivalent to
the fact that there exists an arbitrarily large countable coded $\omega$-model of ${\rm ACA}_{0}$, cf.\,\cite{AfshariRathjen}.
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\cite{AfshariRathjen} gives 
a purely proof-theoretic proof of Theorem \ref{th:MontalbanMarcone}.
Their proof is based on Sch\"utte's method of complete proof search in $\omega$-logic, cf.\,\cite{Schutte}.

In \cite{MontalbanMarcone}, a further equivalence is established for the binary Veblen function.
In M. Rathjen, et.\,al.\cite{AfshariRathjen,RathjenWeiermannRM,RathjenHFriedman} and
\cite{Arai17} the well-ordering principles are investigated proof-theoretically.
Note that in Theorem \ref{th:Girardp.299} the proof-theoretic ordinal 
$|{\rm ACA}_{0}|=|{\rm WOP}(\lambda X.\omega^{X})|=\varepsilon_{0}$ is the least fixed point of the function 
$\lambda x.\omega^{x}$.
Moreover the ordinal $|{\rm ACA}_{0}^{+}|=|{\rm WOP}(\lambda X.\varepsilon_{X})|$ in 
\cite{MontalbanMarcone,AfshariRathjen} is the least fixed point of the function $\lambda x.\varepsilon_{x}$, and
$|{\rm ATR}_{0}|=|{\rm WOP}(\lambda X.\varphi X0)|=\Gamma_{0}$ in \cite{RathjenWeiermannRM} 
one of $\lambda x.\varphi_{x}(0)$.
These results suggest a general result that
the well-ordering principle for normal functions ${\sf g}$ on ordinals
is equal to the least fixed point of ${\sf g}$.

In this note we confirm this conjecture
under a mild condition on normal function ${\sf g}$, 
cf.\,Definition \ref{df:omegag} for the extendible term structures.

We assume that the strictly increasing 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
to be provable elementarily,
and if $X$ is a well-ordering of type $\alpha$, then ${\sf g}(X)$ is also a well-ordering of type ${\sf g}(\alpha)$.
Moreover
${\sf g}(X)$ is assumed to be a \textit{term structure} over
constants ${\sf g}(c)\, (c\in X)$, function constants $+,\omega$, and possibly other function constants.

\begin{theorem}\label{th:prfthordwop}
Let ${\sf g}(X)$ be an extendible term structure, and 
${\sf g}^{\prime}(X)$ an exponential term structure for which (\ref{df:omegag.4}) holds below.


Then the proof-theoretic ordinal of the second order arithmetic
${\rm WOP}({\sf g})$ over ${\rm ACA}_{0}$
is equal to the least fixed point ${\sf g}^{\prime}(0)$ of the ${\sf g}$-function,
$|{\rm ACA}_{0}+{\rm WOP}({\sf g})|=\min\{\alpha:{\sf g}(\alpha)=\alpha\}=\min\{\alpha>0:\forall\beta<\alpha({\sf g}(\beta)<\alpha)\}$.
\end{theorem}

On the other side the proof of the harder direction of Theorem 4 in \cite{Arai17} 
should be corrected as pointed out by A. Freund.
The theorem is stated as follows.

\begin{theorem}\label{th:derivativemodel}
Let ${\sf g}(X)$ be an extendible term structure, and 
${\sf g}^{\prime}(X)$ an exponential term structure for which (\ref{df:omegag.4}) holds.


Then the following two are mutually equivalent over ${\rm ACA}_{0}$:
\begin{enumerate}
\item\label{th:derivativemodel.1}
${\rm WOP}({\sf g}^{\prime})$.
\item\label{th:derivativemodel.2}
$\left({\rm WOP}({\sf g})\right)^{+}
:\Leftrightarrow \forall X\exists \mathcal{Q}[X\in_{\omega}\mathcal{Q} \land 
M(\mathcal{Q})\models{\rm ACA}_{0}+{\rm WOP}({\sf g})]$.
\end{enumerate}
\end{theorem}







Let us mention the contents of the paper.
In the next section \ref{sect:termstr}, ${\sf g}(X)$ is defined as a term structure.
Exponential term structures and extendible ones are defined.
The easy direction in Theorem \ref{th:prfthordwop} is shown.
In section \ref{sect:proofschema} we prove Theorems \ref{th:prfthordwop} and \ref{th:derivativemodel},
assuming an elimination theorem \ref{lem:WPbndtransf} of the well-ordering principle
in infinitary sequent calculi. 
In section \ref{sect:CE} we prove the elimination theorem \ref{lem:WPbndtransf}.







\section{Term structures}\label{sect:termstr}
Let us reproduce definitions on term structure from \cite{Arai17}.

The fact that ${\sf g}$ sends
linear orderings $X$ to linear orderings ${\sf g}(X)$ should be provable in an elementary way.
${\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 further assume that ${\sf g}(X)$ is a Skolem hull, i.e., a term structure over
constants $0$ and ${\sf g}(c)\, (c\in \{0\}\cup X)$ with the least element $0$ in the order $<_{X}$,
the addition $+$, the exponentiation $\omega^{x}$, and possibly other function constants 
in a list $\mathcal{F}$.
When $\mathcal{F}=\emptyset$, let $\omega^{\alpha}:={\sf g}(\alpha)$.
Otherwise we assume that $\lambda \xi.\,\omega^{\xi}$ is in the list $\mathcal{F}$.


\begin{definition}\label{df:gtmstr}
{\rm
\begin{enumerate}
\item
${\sf g}(X)$ is said to be a \textit{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.
\begin{enumerate}
\item(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.

\item(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$.

 \item(Linearity)
 $<_{{\sf g}(X)}$ is a linear ordering on ${\sf g}(X)/=$ with the least element $0$.

\item(Increasing)
${\sf g}$ is strictly increasing:
$c<_{X}d \Rarw {\sf g}(c)<_{{\sf g}(X)}{\sf g}(d)$.


\item(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)$.
\end{enumerate}

\item
A computably linear term structure ${\sf g}(X)$ is said to be \textit{extendible} if it enjoys
the following two conditions.
\begin{enumerate}
\item(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$.

\item(Indiscernible)
\\
$\langle {\sf g}(c): c\in\{0\}\cup X\rangle$ is an indiscernible sequence for 
linear orderings $\langle{\sf g}(X),<_{{\sf g}(X)}\rangle$:
Let $\alpha[0,{\sf g}(c_{1}),\ldots,{\sf g}(c_{n})], \beta[0,{\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 $0,{\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}$, the following holds.
\begin{eqnarray}
&&
\alpha[0,{\sf g}(c_{1}),\ldots,{\sf g}(c_{n})]<_{{\sf g}(X)}\beta[0,{\sf g}(c_{1}),\ldots,{\sf g}(c_{n})]
\label{eq:indiscerng}
\\
& \Leftrightarrow &
\alpha[0,{\sf g}(d_{1}),\ldots,{\sf g}(d_{n})]<_{{\sf g}(X)}\beta[0,{\sf g}(d_{1}),\ldots,{\sf g}(d_{n})]
\nonumber
\end{eqnarray}

\end{enumerate}
\end{enumerate}
}
\end{definition}




\begin{proposition}\label{prp:dilate}
{\rm 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\Rarw 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\Rarw F(n)<_{{\sf g}(Y)}F(m)$,
which extends $f$ in the sense that $F({\sf g}(n))={\sf g}(f(n))$.
\end{proposition}
{\bf Proof}.\hspace{2mm}
This is seen from the indiscernibility (\ref{eq:indiscerng}), cf.\,\cite{Arai17}.
\hspace*{\fill} $\Box$



\begin{definition}\label{df:omegag}
{\rm Suppose that function symbols $+, \lambda \xi.\,\omega^{\xi}$ 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 \textit{exponential} term structure 
(with respect to function symbols $+,\lambda \xi.\,\omega^{\xi}$) if all of the followings are provable in ${\rm RCA}_{0}$.
\begin{enumerate}
 \item\label{df:omegag.1}
 $0$ is the least element in $<_{{\sf g}(X)}$, and $\alpha+1$ is the successor of $\alpha$.
 \item\label{df:omegag.2}
 $+$ and $\lambda \xi.\,\omega^{\xi}$ enjoy the following familiar conditions.
 \begin{enumerate}
 \item
  $\alpha<_{{\sf g}(X)}\beta\to \omega^{\alpha}+\omega^{\beta}=\omega^{\beta}$.
  \item
 $\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)$.
 \item
  $\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$.
  \item
  $(\alpha+\beta)+\gamma=\alpha+(\beta+\gamma)$.
  \item
  $\alpha<_{{\sf g}(X)}\beta\to\exists\gamma\leq_{{\sf g}(X)}\beta(\alpha+\gamma=\beta)$.
  \item
  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})]$.
 \end{enumerate}

\item\label{df:omegag.3}
Each $f(\beta_{1},\ldots,\beta_{n})\in{\sf g}(X)\, (+\neq 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.

\end{enumerate}
}
\end{definition}

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 $0$ and
${\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}$.
We are assuming that a function constant $\lambda \xi.\,\omega^{\xi}$ is in the list $\mathcal{F}\cup\{{\sf g}\}$.
Furthermore assume that ${\rm RCA}_{0}$ proves that
\begin{eqnarray}
\beta_{1},\ldots,\beta_{n}<_{{\sf g}^{\prime}(X)}{\sf g}^{\prime}(c) & \to &
 f(\beta_{1},\ldots,\beta_{n})<_{{\sf g}^{\prime}(X)}{\sf g}^{\prime}(c) \,(f\in\mathcal{F}\cup\{+,{\sf g}\})
 \nonumber
 \\
\omega^{{\sf g}^{\prime}(\beta)} & = & {\sf g}({\sf g}^{\prime}(\beta))={\sf g}^{\prime}(\beta)
\nonumber
\\
{\sf g}^{\prime}(0) & = & \sup_{n}{\sf g}^{n}(0)
\label{df:omegag.4}
\\
{\sf g}^{\prime}(c+1) & = & \sup_{n}{\sf g}^{n}({\sf g}^{\prime}(c)+1)\, (c\in\{0\}\cup X)
\nonumber
\end{eqnarray}
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.
The last two in (\ref{df:omegag.4}) hold for normal functions ${\sf g}$ when ${\sf g}(0)>0$.

Note that ${\sf g}^{\prime}(c)$ is an epsilon number when $<_{{\sf g}^{\prime}(X)}$
is a well-ordering since the exponential function is in $\mathcal{F}\cup\{{\sf g}\}$.
\\


We show the easy direction in Theorem \ref{th:prfthordwop}.
Let $<$ be an order of type ${\sf g}^{\prime}(0)$, which is defined from a family of structures
${\sf g}(X_{n})$ where the order types of $X_{n}$ is $\gamma_{n}+1$ defined as follows.
A series of ordinals $\{\gamma_{n}\}_{n}<{\sf g}^{\prime}(0)$ is defined recursively by $\gamma_{0}=0$ and 
$\gamma_{n+1}={\sf g}(\gamma_{n})$.
Then ${\rm WOP}({\sf g})$ yields inductively ${\rm TI}[<_{\gamma_{n}}]$ for initial segments of type $\gamma_{n}$.
Hence $|{\rm WOP}({\sf g})|\geq{\sf g}^{\prime}(0):=\min\{\alpha>0:\forall\beta<\alpha({\sf g}(\beta)<\alpha)\}$.


\section{Proof schema}\label{sect:proofschema}
In this section we give a proof schema of Theorems \ref{th:prfthordwop} and \ref{th:derivativemodel},
each of these is based on an elimination theorem \ref{lem:WPbndtransf} of the well-ordering principle
in infinitary sequent calculi. 


Formulas in our infinitary sequent calculi are generated from
literals $\top$(truth), $\bot:\equiv\bar{\top}$(absurdity),
$P(n),\bar{P}(n),E_{i}(n),\bar{E}_{i}(n), X_{i}(n),\bar{X}_{i}(n)\,(i,n\in\mathbb{N})$
by applyig
infinitary disjunction $\bigvee_{n\in\mathbb{N}}A_{n}$, 
infinitary conjunction $\bigwedge_{n\in\mathbb{N}}A_{n}$
and second-order quantifications $\exists X,\forall X$.
Binary disjunctions $A_{0}\lor A_{1}$ are understood to be
$\bigvee_{n}B_{n}$ with $B_{0}\equiv A_{0}$ and $B_{1+n}\equiv A_{1}$,
and similarly for binary conjunctions.
A formula is said to be a well-formed formula, wff in short if
there is no free occurrence of `bound variables' $X_{i},\bar{X}_{i}$ in it.
 The negation $A$ of a wff $A$ is defined recursively by the de Morgan's law and the elimination
 of double negations.
Each wff is assumed to be a translation $A^{\infty}$ of
a formula $A$ without free first-order variables in the language of second-order arithmetic.
The translation is defined recursively as follows.
For an arithmetic literal $L$,
 $L^{\infty}\equiv \top$ if $L$ is true in the standard model $\mathbb{N}$,
 $L^{\infty}\equiv\bot$ otherwise.
 For a closed terms $t$ and $R\in\{P,\bar{P},E_{i},\bar{E}_{i},X_{i},\bar{X}_{i}: i\in\mathbb{N}\}$,
 $R(t)^{\infty}\equiv R(n)$ with the value $n$ of the closed term $t$ in $\mathbb{N}$.
 $(A_{0}\lor A_{1})^{\infty}\equiv(A_{0}^{\infty}\lor A_{1}^{\infty})$, and similarly for conjunctions.
 $(\exists x\,A(x))^{\infty}\equiv\bigvee_{n}A(\bar{n})^{\infty}$ for the $n$-th numeral $\bar{n}$.
 $(\forall x\,A(x))^{\infty}$ is defined to be an infinitary conjunction similarly.
 $(\exists X\,A(X))^{\infty}\equiv(\exists X\, A(X)^{\infty})$, and similarly for 
 the second-order universal quantifiers.
A formula is said to be a \textit{first-order} if no second-order quantifier occurs in it,
while it is \textit{arithmetical} if it is the translation of 
a formula in the language of the first-order arithmetic.
i.e., neither the predicate constant $P$ nor second-order variable occurs in it.

Each first-order formula $A$ defines a binary relation $n<_{A}m:\Leftrightarrow A(\langle n,m\rangle)$.
The principle is formulated in the inference rule $(WP)$ together with a rule
for the progressiveness ${\rm Prg}[<_{A},E_{A}]$ of $E_{A}$ with respect to $<_{A}$:
\[
\infer[(WP)]{\Gamma}
{
\{
\Gamma, E_{A}(n)
: n\in\mathbb{N}
\}
&
\lnot{\rm TI}[<_{{\sf g}_{A}}],\Gamma
}
\]
where
$E_{A}$ is a variable proper to the relation $<_{A}$, and does not occur in $\Gamma$.
$n<_{{\sf g}_{A}}m:\Leftrightarrow{\sf g}(A)(\langle n,m\rangle)$.

Our proof proceeds as follows.
Given cut-free derivations of $\Gamma, E_{A}(n)$ without the rule $(WP)$,
suppose that we can obtain an embedding $f$ from the relation $<_{A}$ to an ordinal $\alpha$
such that $n<_{A}m\Rarw f(n)<f(m)<\alpha$.
Then the embedding $f$ can be extended to an embedding $F$ from the relation
$<_{{\sf g}_{A}}$ to an ordinal ${\sf g}(\alpha)$ by Proposition \ref{prp:dilate}.
The embedding $F$ yields the transfinite induction ${\rm TI}[<_{{\sf g}_{A}}]$ 
for the relation $<_{{\sf g}_{A}}$.
Eliminating the false formula $\lnot{\rm TI}[<_{{\sf g}_{A}}]$,
we obtain $\Gamma$.

However in order to extract such an embedding $f$ from
derivations,
we have to fix a meaning of the relation $<_{A}$.
In other words, we need to interpret the predicate constant $P$ and free-variables $E_{i}$
occurring in the formula $A$ so that these denote sets of natural numbers.
This motivates Definition \ref{df:GQ} below.



\begin{definition}\label{df:GQ}
{\rm
Let $\mathcal{E}\subset\mathbb{N}$ be a family of sets
$\mathcal{E}_{i}=\{n\in\mathbb{N}: \langle i,n\rangle\in\mathcal{E}\}$.
Each variable $E_{i}$ is understood to denote 
the set $\mathcal{E}_{i}$.
Let
\[
{\rm Diag}(\mathcal{E}_{i})=
\{E_{i}(n): n\in\mathcal{E}_{i}\}\cup
\{\bar{E}_{i}(n): n\not\in\mathcal{E}_{i}\}.
\]

The predicate $P$
denotes a set $\mathcal{P}\subset\mathbb{N}$.
\[
{\rm Diag}(\mathcal{P})=\{P(n): n\in\mathcal{P}\}\cup\{\bar{P}(n) : n\not\in\mathcal{P}\}.
\]


${\rm Diag}(\mathcal{P},\mathcal{E})={\rm Diag}(\mathcal{P})\cup\bigcup_{i\in\mathbb{N}}{\rm Diag}(\mathcal{E}_{i})$ is identified with the countable coded $\omega$-model 
$\langle\mathbb{N};\mathcal{P},\mathcal{E}_{i}\rangle_{i\in\mathbb{N}}$, and
${\rm Diag}(\mathcal{P},\mathcal{E})\models A:\Leftrightarrow\langle\mathbb{N};\mathcal{P},\mathcal{E}\rangle_{i\in\mathbb{N}}\models A$ for 
first-order formulas $A$.
For $\Sigma^{1}_{1}$-formulas $\exists X\, F(X)$ with first-order matrices $F$,
define
${\rm Diag}(\mathcal{P},\mathcal{E})\models\exists X\, F(X)$ iff
there exists a first-order formula $A(x)$ in the language of arithmetic
such that
${\rm Diag}(\mathcal{P},\mathcal{E})\models F(A)$,
where
$F(A)$ denotes the result of replacing literals $X(n)$ [$\bar{X}(n)$] in $F(X)$ by
$A(n)^{\infty}$ [by $\lnot A(n)^{\infty}$], resp.


For a finite set $\Gamma$ of first-order formulas, 
$Var(\Gamma)$ denotes the set of second-order variables $E_{i}$
occurring in $\Gamma$.
For a family $\mathcal{E}^{X}$ of finite sets $\mathcal{E}^{X}_{i}$, let
\[
\Delta(\mathcal{E}^{X};\Gamma):= \{E_{i}(n): n\in\mathcal{E}^{X}_{i}, E_{i}\in Var(\Gamma),i\in\mathbb{N}\}
\]
}
\end{definition}


\begin{definition}\label{df:calculi}
{\rm
Let $\mathcal{P}\subset\mathbb{N}$ be a set of natural numbers, and
 $\mathcal{E}$ a family of sets $\mathcal{E}_{i}\subset\mathbb{N}$.
We define two cut-free infinitary one-sided sequent calculi
${\rm Diag}(\mathcal{P})+(prg)^{\infty}+(WP)$, and
${\rm Diag}(\mathcal{P},\emptyset)+(prg)^{\emptyset}$ as follows.


Let 
$\mathcal{E}^{X}$ be a family of \textit{finite} sets 
$\mathcal{E}^{X}_{i}\subset\mathbb{N}\,(i\in\mathbb{N})$,
$\beta,\alpha$ ordinals, and $\Gamma$ a sequent, i.e., a finite set of formulas (in negation normal from).
We define a derivability relation
$\vdash^{\beta}_{\alpha}\Gamma$ in the calculus
${\rm Diag}(\mathcal{P})+(prg)^{\infty}+(WP)$,
and one
$\mathcal{E}^{X}\vdash^{\beta}\Gamma$
in 
${\rm Diag}(\mathcal{P},\emptyset)+(prg)^{\emptyset}$
as follows,
where the depth of the derivation is bounded by $\beta$,
and the depth of the \textit{nested applications} of the inferences
 $(WP)$
is bounded by $\alpha$ in the witnessed derivation in ${\rm Diag}(\mathcal{P})+(prg)^{\infty}+(WP)$.
\\
{\bf Axioms} or initial sequents:
\begin{enumerate}
\item
For $L\equiv\top$ and $L\in {\rm Diag}(\mathcal{P})$,
both $\vdash^{\beta}_{\alpha}\Delta,L$ 
and $\mathcal{E}^{X}\vdash^{\beta}\Delta,L$ hold.

\item
$\vdash^{\beta}_{\alpha}\Delta,\bar{L},L$ for literals
$L\in\{E_{i}(n): i,n\in\mathbb{N}\}$.


\item
$\mathcal{E}^{X}\vdash^{\beta}\Delta,\bar{L}$ for literals
$L\in\{E_{i}(n): i,n\in\mathbb{N}\}$.

\end{enumerate}
{\bf Inference rules}:  
The following inference rules $(\bigvee), (\bigwedge),(Rep),(\exists^{2}_{1st}),(\forall^{2})$
are shared by two calculi.
The left part $\mathcal{E}^{X}$ of $\vdash$ should be deleted for
the calculus ${\rm Diag}(\mathcal{P})+(prg)^{\infty}+(WP)$,
and the subscript $\alpha$ is irrelevant to the calculus 
${\rm Diag}(\mathcal{P},\emptyset)+(prg)^{\infty}$ in the following.
Let $\gamma<\beta$
\[
\infer[(\bigvee)]{\mathcal{E}^{X}\vdash^{\beta}_{\alpha}\Gamma,\bigvee_{n}A_{n}}
{\mathcal{E}^{X}\vdash^{\gamma}_{\alpha}\Gamma,\bigvee_{n}A_{n},A_{i}}
\,\,
\infer[(\bigwedge)]{\mathcal{E}^{X}\vdash^{\beta}_{\alpha}\Gamma,\bigwedge_{n}A_{n}}
{
\{
\mathcal{E}^{X}\vdash^{\gamma}_{\alpha}\Gamma,\bigwedge_{n}A_{n}, A_{i}
:i\in\mathbb{N}\}
}
\,\,
\infer[(Rep)]{\mathcal{E}^{X}\vdash^{\beta}_{\alpha}\Gamma}
{\mathcal{E}^{X}\vdash^{\gamma}_{\alpha}\Gamma}
\]
\[
\infer[(\exists^{2}_{1st})]{\mathcal{E}^{X}\vdash^{\beta}_{\alpha}\exists X F(X),\Gamma}
{
\mathcal{E}^{X}\vdash^{\gamma}_{\alpha}F(A),\exists X F(X),\Gamma}
\mbox{\hspace{5mm}}
\infer[(\forall^{2})]{\mathcal{E}^{X}\vdash^{\beta}_{\alpha}\Gamma,\forall X\, F(X)}
{
\mathcal{E}^{X}\vdash^{\gamma}_{\alpha}\Gamma,\forall X\, F(X), F(E)
}
\]
where in $(\exists^{2}_{1st})$, $A(x)$ is a first-order formula, and
in $(\forall^{2})$, $E$ is an eigenvariable not occurring in $\Gamma\cup\{\forall X F(X)\}$.

A first-order formula $A$ defines a binary relation $n<_{A}m:\Leftrightarrow A(\langle n,m\rangle)$.
Let 
$n<_{{\sf g}_{A}}m:\Leftrightarrow {\sf g}(A)(\langle n,m\rangle)$.
For each first-order formulas $A$, $\beta_{0}<\beta$ and $\alpha_{0}<\alpha$, we have
the following:
\[
\infer[(WP)]{\vdash^{\beta}_{\alpha}\Gamma}
{
\{
\vdash^{\beta_{0}}_{\alpha_{0}}\Gamma, E_{A}(n)
: n\in\mathbb{N}
\}
&
\vdash^{\beta_{0}}_{\alpha_{0}}\lnot{\rm TI}[<_{{\sf g}_{A}}],\Gamma
}
\]
where
the variable $E_{A}$ with the G\"odel number $i=\lceil A\rceil$ does not occur in $\Gamma$.


\begin{enumerate}
\item
For each first-order formulas $A$, $\beta_{0}<\beta$, we have
the following.
Let $<_{A}^{*}$ denote the transitive closure of the relation $<_{A}$ for a first-order formula $A$.

\[
\infer[(prg)^{\infty}]{\vdash^{\beta}_{\alpha}\Gamma,E_{A}(m)}
{
\{
\vdash^{\beta_{0}}_{\alpha}
\Gamma,E_{A}(m),n\not<^{*}_{A}m,E_{A}(n)
:n\in\mathbb{N}
\}
}
\]
where $E_{A}\equiv E_{i}$ with the G\"odel number $i=\lceil A\rceil$ of the formula $A$,
and  $Var(A)\subset Var(\Gamma)$.


\item
Let $A$ be a first-order formula with the G\"odel number $i=\lceil A\rceil$.
$n<^{*,\emptyset}_{A}m$ denotes the transitive closure of the relation 
$n<^{\emptyset}_{A}m:\Leftrightarrow {\rm Diag}(\mathcal{P},\emptyset)\models A(\langle n,m\rangle)$.
If
\begin{equation}\label{eq:normal}
m\in\mathcal{E}^{X}_{i}
\end{equation}
then the inference $(prg)^{\emptyset}$ can be applied for $\beta_{0}<\beta$:
\[
\infer[(prg)^{\emptyset}]{((\mathcal{E}^{X}_{j})_{j\neq i},\mathcal{E}^{X}_{i})\vdash^{\beta}\Gamma,E_{A}(m)}
{
\{((\mathcal{E}^{X}_{j})_{j\neq i},\mathcal{E}^{X}_{i}\cup\{n\})\vdash^{\beta_{0}}\Gamma,E_{A}(m),E_{A}(n):n<^{*,\emptyset}_{A}m
\}
}
\]
where  
we assume that the variable $E_{A}\equiv E_{i}$ does not occur in $A$,
and $Var(A)\subset Var(\Gamma)$.

\end{enumerate}
}
\end{definition}
The rule $(prg)^{\infty}$ states the fact that the set
$E_{A}$ is progressive with respect to the relation 
$<^{*}_{A}$, i.e.,
${\rm Prg}[<^{*}_{A},E_{A}]$.
It is convenient for us
in proving Theorem \ref{th:TakeutimultiTI} in section \ref{sect:CE}
to have the weaker statement 
${\rm Prg}[<^{*}_{A},E_{A}]$ instead of the
stronger ${\rm Prg}[<_{A},E_{A}]$.
$(WP)$ together with $(prg)$
yields the well-ordering principle for ${\sf g}$.


\begin{definition}\label{df:attach}
{\rm
Let $\pi$ be a derivation witnessing the fact
${\rm Diag}(\mathcal{P})+(prg)^{\infty}+(WP)\vdash^{\beta}_{\alpha}\Gamma_{0}$,
and $T(\pi)\subset{}^{<\omega}\mathbb{N}$ the underlying tree of $\pi$.
Let us assign recursively a family $\mathcal{E}^{X}(\sigma)=\mathcal{E}^{X}(\sigma;\pi)$
of \textit{finite} sets
$\mathcal{E}^{X}_{i}(\sigma)$
to each node $\sigma\in T(\pi)$ in a bottom-up way as follows.
In the definition,
$\mathcal{E}^{X}(\sigma)\vdash\Gamma$ designates that
$\mathcal{E}^{X}(\sigma)$ is assigned to the node $\sigma$ at which
the sequent $\Gamma$ is placed.
In this case we write $\sigma:\Gamma$.

To the end-sequent, i.e., the bottom sequent $\emptyset:\Gamma_{0}$,
assign the set $\mathcal{E}_{i}^{X}(\emptyset)=\{n: E_{i}(n)\in\Gamma_{0}\}$.

Suppose that finite sets $(\mathcal{E}^{X}_{j}(\sigma))_{j\neq i}$ are assigned to the lower sequent $\sigma:\Gamma$
of a rule $(WP)$ for the relation $<_{A}$ with $i=\lceil A\rceil$.
For the $n$-th left upper sequents $\sigma*(n):\Gamma,E_{A}(n)$, assign the family 
$((\mathcal{E}^{X}_{j}(\sigma))_{j\neq i},\{n\})$
with $\mathcal{E}^{X}_{i}(\sigma*(n))=\{n\}$.
For the right upper sequent $\sigma*(\omega):\lnot{\rm TI}[<_{{\sf g}_{A}}],\Gamma$, 
assign the family $(\mathcal{E}^{X}_{j}(\sigma))_{j\neq i}$.
{\small
\[
\infer[(WP)]{(\mathcal{E}^{X}_{j}(\sigma))_{j\neq i}\vdash\Gamma}
{
\{
((\mathcal{E}^{X}_{j}(\sigma))_{j\neq i},\{n\})\vdash\Gamma, E_{A}(n)
: n\in\mathbb{N}
\}
&
(\mathcal{E}^{X}_{j}(\sigma))_{j\neq i}\vdash\lnot{\rm TI}[<_{{\sf g}_{A}}],\Gamma
}
\]
}
where
the variable $E_{A}$ with $i=\lceil A\rceil$ does not occur in $\Gamma$.

Next suppose that a family 
$((\mathcal{E}^{X}_{j}(\sigma))_{j\neq i},\mathcal{E}^{X}_{i}(\sigma))\,(i=\lceil A\rceil)$
 is assigned to
the lower sequent $\sigma:\Gamma,E_{A}(m)$ of the rule $(prg)^{\infty}$.
For each number $n$,
assign the family $((\mathcal{E}^{X}_{j}(\sigma))_{j\neq i},\mathcal{E}^{X}_{i}(\sigma)\cup\{n\})$
to the $n$-th upper sequent $\sigma*(n):\Gamma,E_{A}(m),n\not<^{*}_{A}m,E_{A}(n)$ with
$\mathcal{E}^{X}_{i}(\sigma*(n))=\mathcal{E}^{X}_{i}(\sigma)\cup\{n\}$.
\[
\infer[(prg)^{\infty}]{((\mathcal{E}^{X}_{j}(\sigma))_{j\neq i},\mathcal{E}^{X}_{i}(\sigma))\vdash\Gamma,E_{A}(m)}
{
\{
((\mathcal{E}^{X}_{j}(\sigma))_{j\neq i},\mathcal{E}^{X}_{i}\cup\{n\})\vdash
\Gamma,E_{A}(m),n\not<^{*}_{A}m,E_{A}(n)
:n\in\mathbb{N}
\}
}
\]
where $E_{A}\equiv E_{i}$ with the G\"odel number $i=\lceil A\rceil$ of the formula $A$.

For rules other than $(WP), (prg)^{\infty}$,
the upper sequents receive the same family as the lower sequent receives.
For example
\[
\infer[(\exists^{2}_{1st})]{\mathcal{E}^{X}(\sigma)\vdash\exists X F(X),\Gamma}
{\mathcal{E}^{X}(\sigma)\vdash F(A),\exists X F(X),\Gamma}
\]
where $Var(A)\subset Var(\Gamma,F)$.

A family $\mathcal{E}^{X}(\sigma)$ has been assigned to each node 
$\sigma\in T(\pi)$ in the tree of the derivation $\pi$ showing
the fact ${\rm Diag}(\mathcal{P})+(prg)^{\infty}+(WP)\vdash^{\beta}_{\alpha}\Gamma_{0}$.
}
\end{definition}



Let us define an ordinal function $F(\beta,\alpha)$ for giving an upper bound in eliminating
the well-ordering principle.
For normal function ${\sf g}(\alpha)$ in Theorems \ref{th:prfthordwop} and \ref{th:derivativemodel}, 
and ordinals $\beta,\alpha$,
let us 
define ordinals $F(\beta,\alpha)$ recursively on $\alpha$ as follows.
$F(\beta,0)=\omega^{1+\beta}$,
\begin{equation}\label{eq:Fsuccessor}
F(\beta,\alpha+1)=F\left({\sf g}(\omega^{2(F(\beta,\alpha)+\beta)+1})+1+\beta,\alpha\right)+{\sf g}(\omega^{2(F(\beta,\alpha)+\beta)+1})+1
\end{equation}
and $F(\beta,\lambda)=\sup\{F(\beta,\alpha)+1:\alpha<\lambda\}$ for limit ordinals $\lambda$.


\begin{proposition}\label{prp:Fg}
\begin{enumerate}
\item\label{prp:Fg.1}
$\gamma<\beta \Rarw F(\gamma,\alpha)\leq F(\beta,\alpha)$, and 
$\gamma<\alpha\Rarw F(\beta,\gamma)<F(\beta,\alpha)$.

\item\label{prp:Fg.3}
$F(\beta,\omega(1+\alpha))={\sf g}^{\prime}(\alpha)$ for $\beta<{\sf g}^{\prime}(\alpha)$.

\item\label{prp:Fg.5}
If $\beta<{\sf g}^{\prime}(\alpha)$ and $\gamma<\omega(1+\alpha)$, then $F(\beta,\gamma)<{\sf g}^{\prime}(\alpha)$.
\end{enumerate}
\end{proposition}
{\bf Proof}.\hspace{2mm}
\ref{prp:Fg}.\ref{prp:Fg.1}.
This follows from the fact that each of functions $\beta\mapsto\alpha+\beta$,
$\beta\mapsto\omega^{\beta}$ and $\beta\mapsto{\sf g}(\beta)$
is strictly increasing.
\\
\ref{prp:Fg}.\ref{prp:Fg.5}.
This follows from the fact that ${\sf g}^{\prime}(\alpha)$ is closed under $\lambda x.\omega^{x}$ and ${\sf g}$.
\hspace*{\fill} $\Box$
\\

\noindent
The following Elimination theorem \ref{lem:WPbndtransf} of the inference $(WP)$ is a crux for us.

\begin{theorem}\label{lem:WPbndtransf}{\rm (Elimination of (WP))}\\
Suppose that for a finite set $\Phi$ of $\Sigma^{1}_{1}$-formulas
$\vdash^{\beta}_{\alpha}\Phi,\Gamma$ holds in the calculus
${\rm Diag}(\mathcal{P})+(prg)^{\infty}+(WP)$ 
for $\sigma:\Phi,\Gamma$ in a witnessing derivation $\pi$
in which the condition (\ref{eq:normal}) is enjoyed for each $(prg)^{\infty}$.
Moreover assume that 
$\Gamma\subset\Delta(\mathcal{E}^{X}(\sigma);\Phi,\Gamma)$, and
${\rm Diag}(\mathcal{P},\emptyset)\not\models B$ for any $B\in\Phi$.


Then 
$\mathcal{E}^{X}(\sigma)\vdash^{F(\beta,\alpha)+\beta}_{0}\Delta(\mathcal{E}^{X}(\sigma);\Phi,\Gamma)$ holds
in the calculus
${\rm Diag}(\mathcal{P},\emptyset)+(prg)^{\emptyset}+(WP)$.
\end{theorem}
In proving Theorem \ref{lem:WPbndtransf},
a key is an extension, Theorem \ref{th:TakeutimultiTI} below,
 of a result due to G. Takeuti\cite{TRemark,PT2}, 
cf.\,Theorem 5 in \cite{Arai17}.





\begin{theorem}\label{th:TakeutimultiTI}
{\rm The following is provable in ${\rm ACA}_{0}+{\rm WO}(\alpha)$:}
\\
Let $n\prec m$ be a binary relation on $\mathbb{N}$, 
and $n\prec^{*}m$ the transitive closure of
the relation $n\prec m$.
$(prg)^{D}_{\prec}$ denotes the following inference rule for a predicate $E$.
\[
\infer[(prg)^{D}_{\prec}]{\mathcal{E}^{X}\vdash^{\beta}\Gamma,E(m)}
{
\{
\mathcal{E}^{X}\cup\{n\}\vdash^{\beta_{0}}\Gamma,E(m),E(n):n\prec^{*}m
\}
}
\]
where the condition (\ref{eq:normal}),
$m\in\mathcal{E}^{X}$, is enjoyed with  a finite set $\mathcal{E}^{X}$.
$\mathcal{E}^{X}\vdash^{\beta}\Gamma$ denotes the derivability relation
in a calculus ${\rm Diag}(\emptyset)+(prg)^{D}_{\prec}$,
in which ${\rm Diag}(\emptyset)=\{\bar{E}(n): n\in\mathbb{N}\}$.

Assume that there exists an ordinal $\alpha$ for which 
$\{n\}\vdash^{\alpha}E(n)$ holds
for any natural number $n$.


Then there exist an embedding $f$ such that 
$n\prec m \Rarw f(n)<f(m)$, $f(m)<\omega^{\alpha+1}$
for any $n,m\in\mathbb{N}$.
\end{theorem}


Proofs of Theorems \ref{lem:WPbndtransf} and \ref{th:TakeutimultiTI}
are postponed in section \ref{sect:CE}.



In what follows we work in ${\rm ACA}_{0}^{+}$.
the set $\{\lceil A\rceil : {\rm Diag}(\mathcal{P},\mathcal{E})\models A\}$ of
the satisfaction relation ${\rm Diag}(\mathcal{P},\mathcal{E})\models A$ for first-order formulas $A$
is then computable from the $\omega$-th jump of the set $\mathcal{P}$.



\subsection{Proof of Theorem \ref{th:prfthordwop}}\label{subsec:Thm3}

First let us prove Theorem \ref{th:prfthordwop}.
In this subsection the predicate $P$ plays no role, and ${\rm Diag}(\mathcal{P})$ is omitted.
Let us introduce a finitary calculus $\mbox{\boldmath$G$} _{2}+(prg)+(WPL)$ obtained from
a calculus $\mbox{\boldmath$G$} _{2}$ for the predicative second-order logic with inference rules $(\exists^{2}_{1st})$
and $(\forall^{2})$ by adding the following rules $(VJ),(prg),(WPL)$ as follows.
The following inference $(VJ)$ for complete induction schema for first-order formulas $A$
and the successor function $S(x)$ with an eigenvariable $x$.
\[
\infer[(VJ)]{\Gamma}
{
\Gamma,A(0)
&
\lnot A(x),\Gamma,A(S(x))
&
\lnot A(t),\Gamma
}
\]
For first-order formulas $A$ and
the eigenvariable $x$:
\[
\infer[(prg)]{\Gamma,E_{A}(t)}
{
\Gamma,E_{A}(t),x\not<^{*}_{A}t, E_{A}(x)
}
\mbox{\hspace{5mm}}
\infer[(WPL)]{\Gamma}
{
\Gamma, E_{A}(x)
&
\Gamma, {\rm LO}(<_{A})
&
\lnot{\rm TI}[<_{{\sf g}_{A}}],\Gamma
}
\]
where $E_{A}\equiv E_{i}$ with $i=\lceil A\rceil$, in $(prg)$,
$x$ is the eigenvariable not occurring freely in $\Gamma,E_{A}(t)$, and
$Var(A)\subset Var(\Gamma)$.
In $(WPL)$, the variable $E_{A}$ does not occur in $\Gamma$ (nor in $A$).
The initial sequents are $\Gamma,\bar{L},L$ for literals $L$.


We can assume that in a finitary proof,
a variable $E$ occurs in an upper sequent of an inference, but not in the lower sequent
only when the inference is a $(\forall^{2})$, and
the variable $E$ is the eigenvariable of the inference.
Moreover if the end-sequent contains no second-order free variable, then
the variable $E_{A}$ can be assumed not to occur in the lower sequent $\Gamma$ of the rule
$(WPL)$ for the relation $<_{A}$.

The axiom of arithmetic comprehension is deduced from the inference rule $(\exists^{2}_{1st})$,
and the axiom ${\rm WOP}({\sf g})$ for the well-ordering principle of ${\sf g}$
is deduced from the inference rules $(prg)$ and  $(WPL)$.


Assume that ${\rm TI}[\prec]$ is provable from ${\rm WOP}({\sf g})$ in ${\rm ACA}_{0}$
for an arithmetical 
relation $\prec$.
Let $\Delta_{0}$ denote a set of negations of axioms for first-order arithmetic except complete induction.
By eliminating $(cut)$'s we obtain a proof of $\Delta_{0},E_{\prec}(x)$ in 
$\mbox{\boldmath$G$} _{2}+(prg)+(WPL)$, where
$E_{\prec}\equiv E_{i}$ with $i=\lceil x_{0}\prec x_{1}\rceil$.


Let us embed the finitary calculus $\mbox{\boldmath$G$} _{2}+(prg)+(WPL)$ to 
an intermediate infinitary calculus
$(prg)^{\infty}+(WP)+(cut)_{1st}$,
which is obtained from $(prg)^{\infty}+(WP)$ 
by
adding the cut inference $(cut)_{1st}$ with
a first-order cut formulas $A$:
\[
\infer[(cut)_{1st}]{\Gamma,\Delta}
{
\Gamma,\lnot A^{\infty}
&
A^{\infty},\Delta
}
\]


The logical depth $\mbox{{\rm dg}}(A)<\omega$ of first-order formulas $A$ is defined recursively by
$\mbox{{\rm dg}}(L)=0$ for literals $L$, 
$\mbox{{\rm dg}}(A_{0}\lor A_{1})=\mbox{{\rm dg}}(A_{0}\land A_{1})=\max\{\mbox{{\rm dg}}(A_{0}),\mbox{{\rm dg}}(A_{1})\}+1$, and $\mbox{{\rm dg}}(\exists x\, A(x)),\mbox{{\rm dg}}(\forall x\, A(x))\}=\mbox{{\rm dg}}(A(0))+1$.
Then let $\mbox{{\rm dg}}(A^{\infty}):=\mbox{{\rm dg}}(A)$.
Let $\Gamma(x,\ldots)$ be a sequent possibly with free first-order variables $x,\ldots$.
Assuming
$\mbox{\boldmath$G$} _{2}+(prg)+(WPL)\vdash\Gamma(x,\ldots)$, we see easily
that there exist $d,p,k,m<\omega$ 
such that
$(prg)^{\infty}+(WP)+(cut)_{1st}\vdash^{\omega k+m}_{d,p}\Gamma(n,\ldots)^{\infty}$ holds 
for any natural numbers $n,\ldots$,
where the first subscript 
$d$ indicates that the number of nested applications of the rule $(WPL)$
is bounded by $d$, and the second $p$ designates that
any (first-order) cut-formula $A^{\infty}$ occurring in the witnessing derivation has the logical depth
$\mbox{{\rm dg}}(A^{\infty})<p$.
 Note that each variable $E$ occurring in the induction formula $A$ of a $(VJ)$ 
 can be assumed to occur
 also in the lower sequent $\Gamma$.
We see that there exist $d,p<\omega$ such that
$(prg)^{\infty}+(WP)+(cut)_{1st}\vdash^{\omega^{2}}_{d,p}\Delta_{0},E_{\prec}(n)$
holds for any natural number $n$.
Eliminating the false arithmetic $\Delta_{0}$,
we obtain
$(prg)^{\infty}+(WP)+(cut)_{1st}\vdash^{\omega^{2}}_{d,p}E_{\prec}(n)$.

Let $2_{0}(\beta)=\beta$ and $2_{p+1}(\beta)=2^{2_{p}(\beta)}$ for $p<\omega$.

\begin{proposition}\label{prp:ce1st}
Suppose 
$(prg)^{\infty}+(WP)+(cut)_{1st}\vdash^{\beta}_{d,p}\Gamma$.
Then
$(prg)^{\infty}+(WP)\vdash^{2_{p}(\beta)}_{2_{p}(d),0}\Gamma$.
\end{proposition}
{\bf Proof}.\hspace{2mm}
Let $A$ be one of formulas $\exists x\, B$, $B\lor C$, $\bar{E}_{i}(n)$
and arithmetic literals.
We see by induction on $\alpha$ that
if $(prg)^{\infty}+(WP)+(cut)_{1st}\vdash^{\beta}_{d,p}\Gamma,\lnot A^{\infty}$
and $(prg)^{\infty}+(WP)+(cut)_{1st}\vdash^{\alpha}_{e,p}A^{\infty},\Delta$
with $\mbox{{\rm dg}}(A)\leq p$,
then
$(prg)^{\infty}+(WP)+(cut)_{1st}\vdash^{\beta+\alpha}_{d+e,p}\Gamma,\Delta$.

From the fact we see the proposition by induction on $p<\omega$.
\hspace*{\fill} $\Box$
\\

\noindent
By Proposition \ref{prp:ce1st} we obtain an ordinal $\beta<\varepsilon_{0}$ and $c<\omega$ for which
$(prg)^{\infty}+(WP)+(cut)_{1st}\vdash^{\beta}_{c,0}E_{\prec}(n)$, i.e.,
$(prg)^{\infty}+(WP)\vdash^{\beta}_{c}E_{\prec}(n)$ holds for any $n$.

In a witnessing derivation $\pi$ of the fact $(prg)^{\infty}+(WP)\vdash^{\beta}_{c}E_{\prec}(n)$,
the condition (\ref{eq:normal}) may be violated.
Let us convert the derivation $\pi$ to a derivation $\pi^{\top}$ as follows.

\begin{definition}
{\rm
For a formula $A$ and a family $\mathcal{E}=(\mathcal{E}_{i})_{i}$ of sets,
$A(\mathcal{E})$ denotes the result of replacing each literal $E_{i}(m)$ by $\top$
when $m\not\in\mathcal{E}_{i}$.
$A(\mathcal{E})$ is defined recursively as follows.
Let $i=\lceil A\rceil$.
\[
\left((E_{A}(m))(\mathcal{E}), (\bar{E}_{A}(m))(\mathcal{E})\right)\equiv\left\{
\begin{array}{ll}
(\top,\bot) & \mbox{if } m\not\in\mathcal{E}_{i}
\\
(E_{A(\mathcal{E})}(m),\bar{E}_{A(\mathcal{E})}(m)) & \mbox{if } m\in\mathcal{E}_{i}
\end{array}
\right.
\]
$L(\mathcal{E})\equiv L$ when $L\in\{\top,\bot,X_{i}(n),\bar{X}_{i}(n):i,n\in\mathbb{N}\}$.
$(\bigvee_{n}A_{n})(\mathcal{E}\equiv\bigvee_{n}(A_{n}(\mathcal{E}))$ and
$(\bigwedge_{n}A_{n})(\mathcal{E}\equiv\bigwedge_{n}(A_{n}(\mathcal{E}))$.
$(\exists X\, F(X))(\mathcal{E})\equiv \exists X (F(X)(\mathcal{E}))$ and
$(\forall X\, F(X))(\mathcal{E})\equiv \forall X (F(X)(\mathcal{E}))$.
For a sequent $\Gamma$, let $\Gamma(\mathcal{E})=\{A(\mathcal{E}):A\in\Gamma\}$.

For each node $\sigma:\Gamma$ in the derivation $\pi$,
let
\[
A^{\sigma}:\equiv A(\mathcal{E}^{X}(\sigma)), \, \Gamma^{\sigma}:=\{A^{\sigma}:A\in\Gamma\}
\]
}
\end{definition}

\begin{proposition}\label{prp:top}
Let $\pi$ be a derivation witnessing the fact $\{n\}\vdash^{\beta}_{c}E_{\prec}(n)$ in 
$(prg)^{\infty}+(WP)$.
Then there exists a derivation $\pi^{\top}$ witnessing the same fact in
$(prg)^{\infty}+(WP)$ such that
$\mathcal{E}^{X}_{A^{\sigma}}(\sigma;\pi^{\top})=\mathcal{E}^{X}_{A}(\sigma;\pi)$
for each $\sigma\in T(\pi^{\top})\subset T(\pi)$, and
the condition (\ref{eq:normal}) is enjoyed for each rule $(prg)^{\infty}$ occurring in $\pi^{\top}$.
\end{proposition}
{\bf Proof}.\hspace{2mm}
This is seen by induction on the tree order on the well-founded tree $T(\pi)$.
Each axiom $\sigma:\Gamma,\bar{L},L$ turns either to $\sigma:\Gamma^{\sigma},\bar{L},L$
or to $\sigma:\Gamma^{\sigma},\bot,\top$.

Consider a rule $(prg)^{\infty}$ in $\pi$.
\[
\infer[(prg)^{\infty}]{((\mathcal{E}^{X}_{j}(\sigma;\pi))_{j\neq i},\mathcal{E}^{X}_{i}(\sigma;\pi))\vdash\Gamma,E_{A}(m)}
{
\{
((\mathcal{E}^{X}_{j}(\sigma;\pi))_{j\neq i},\mathcal{E}^{X}_{i}(\sigma;\pi)\cup\{n\})\vdash
\Gamma,E_{A}(m),n\not<^{*}_{A}m,E_{A}(n)
:n\in\mathbb{N}
\}
}
\]
where $E_{A}\equiv E_{i}$ with the G\"odel number $i=\lceil A\rceil$ of the formula $A$.
If $m\in\mathcal{E}^{X}_{A}(\sigma;\pi)$, then $m\in\mathcal{E}^{X}_{A^{\sigma}}(\sigma;\pi^{\top})=\mathcal{E}^{X}_{A}(\sigma;\pi)$,
and
\[
\infer[(prg)^{\infty}]{((\mathcal{E}^{X}_{j}(\sigma))_{j\neq i},\mathcal{E}^{X}_{i}(\sigma))\vdash\Gamma^{\sigma},E_{A^{\sigma}}(m)}
{
\{
((\mathcal{E}^{X}_{j}(\sigma))_{j\neq i},\mathcal{E}^{X}_{i}\cup\{n\})\vdash
\Gamma^{\sigma},E_{A^{\sigma}}(m),n\not<^{*}_{A^{\sigma}}m,E_{A^{\sigma}}(n)
:n\in\mathbb{N}
\}
}
\]
Otherwise $(E_{A}(m))^{\sigma}\equiv\top$.
$\Gamma^{\sigma},\top$ is an axiom. Discard the upper part.

From the construction of $\pi^{\top}$ we see easily that
$\mathcal{E}^{X}_{A^{\sigma}}(\sigma;\pi^{\top})=\mathcal{E}^{X}_{A}(\sigma;\pi)$ for each node 
$\sigma\in T(\pi^{\top})\subset T(\pi)$, and
the condition (\ref{eq:normal}) is enjoyed for each rule $(prg)^{\infty}$ occurring in $\pi^{\top}$.
\hspace*{\fill} $\Box$
\\

By Proposition \ref{prp:top}
we obtain a derivation $\pi^{\top}$ witnessing the fact $\{n\}\vdash^{\beta}_{c}E_{\prec}(n)$ in
$(prg)^{\infty}+(WP)$ such that
the condition (\ref{eq:normal}) is enjoyed for each rule $(prg)^{\infty}$ occurring in $\pi^{\top}$.

We see from Theorem \ref{lem:WPbndtransf}
 that in the calculus ${\rm Diag}(\emptyset)+(prg)^{\emptyset}$,
$\{n\}\vdash^{\alpha}_{0}E_{\prec}(n)$ holds for any $n$, and the ordinal
$\alpha=F(\beta,c)+\beta$, where 
$\{n\}=\mathcal{E}_{i}^{X}(\pi)$ with $i=\lceil x_{0}\prec x_{1}\rceil$ and
$\Delta(\{n\},\emptyset;E_{\prec}(n))=\{E_{\prec}(n)\}$.

Theorem \ref{th:TakeutimultiTI} yields an embedding
$f$ such that $n\prec m \Rarw f(n)<f(m)<\omega^{\alpha+1}$.

On the other hand we have $\omega^{\alpha+1}=\omega^{F(\beta,c)+\beta+1}<{\sf g}^{\prime}(0)$
by Proposition \ref{prp:Fg}.\ref{prp:Fg.5} and $\beta<\varepsilon_{0}\leq{\sf g}^{\prime}(0)$.
Thus Theorem \ref{th:prfthordwop} is proved.



\subsection{Corrections to \cite{Arai17}}\label{sect:correction}
The proof of the harder direction of Theorem 4 in \cite{Arai17} 
should be corrected as pointed out by A. Freund.
In this subsection the predicate $P$ will denote a given set of natural numbers.
Let us augment another countable list $Y_{i},\bar{Y}_{i}\,(i\in\mathbb{N})$ of
second-order free variables.
First-order formulas may contain these variables $Y$.

Assuming ${\rm WOP}({\sf g}^{\prime})$, we need to show the existence of a countable coded $\omega$-model 
$(\mathcal{P},(\mathcal{Q})_{i})_{i<\omega}$ of ${\rm ACA}_{0}+{\rm WOP}({\sf g})$ for a given set $\mathcal{P}\subset\mathbb{N}$.
In what follows argue in ${\rm ACA}_{0}+{\rm WOP}({\sf g}^{\prime})$.
Since ${\rm WOP}({\sf g}^{\prime})$ implies ${\rm WOP}(\lambda X.\varepsilon_{X})$, which in turn
yields ${\rm ACA}_{0}^{+}$ by Theorem \ref{th:MontalbanMarcone},
we are working in ${\rm ACA}_{0}^{+}+{\rm WOP}({\sf g}^{\prime})$, and we can assume the
existence of the $\omega$-th jump of any sets.



Let us search a derivation of the contradiction $\emptyset$ in the following infinitary calculus
${\rm Diag}(\mathcal{P})+(prg)^{\infty}+(WP)+(ACA)$, in which the variables $E_{i}$ are not interpreted.
The calculus is obtained from the infinitary 
calculus $(prg)^{\infty}+(WP)$
 by
 adding the following rule $(ACA)$ for arithmetic comprehension axiom:
\[
\infer[(ACA)]{\Gamma}
{
Y_{j}\neq A,\Gamma
}
\]
where $A$ is a first-order formula, 
$Y_{j}$ is the eigenvariable not occurring in $\Gamma\cup\{A\}$, and
$Y_{j}\neq A:\Leftrightarrow (\lnot\forall x[Y_{j}(x)\leftrightarrow A(x)])^{\infty}$.
Note that variables $E_{i},Y_{i}$ are uninterpreted in the calculus.

A tree ${\cal T}\subset{}^{<\omega}\mathbb{N}$ is constructed recursively as follows.
At each node $\sigma$, a sequent and a family $\mathcal{E}^{X}(\sigma)$ of finite sets are assigned.
At the bottom $\emptyset$, we put the empty sequent, and $\mathcal{E}^{X}(\sigma)=\emptyset$.
The assignment $\mathcal{E}^{X}(\sigma)$ is done similarly as in Definition \ref{df:attach}.

Suppose that the tree ${\cal T}$ has been constructed up to a node $\sigma\in{}^{<\omega}\mathbb{N}$. 
Let $\{A_{i}\}_{i}$ be an enumeration of all first-order formulas (abstracts).
\\
{\bf Case 0}. The length $lh(\sigma)=3i$:
Apply one of inferences $(\bigvee),(\bigwedge),(\exists^{2}_{1st})$,
and $(prg)^{\infty}$ if it is possible.
Otherwise repeat, i.e., apply an inference $(Rep)$.

When $(\exists^{2}_{1st})$ is applied backwards, a first-order $A_{j}$ is chosen so that $j$ is the least 
such that
$A_{j}$ has not yet been tested for the major formula $\exists X\, F(X)$ of the $(\exists^{2}_{1st})$, and
$Var(A_{j})\subset Var(\Gamma\cup\{F\})\cup\{P\}$.
\[
\infer[(\exists^{2}_{1st})]{\Gamma,\exists X\, F(X)}
{
\Gamma,\exists X\,F(X),F(A_{j})
}
\]
When $(prg)^{\infty}$ is applied backwards to a formula $E_{A}(m)$ with $i=\lceil A\rceil$,
the condition (\ref{eq:normal}), $m\in\mathcal{E}^{X}_{i}(\sigma)$,
and $Var(A)\subset Var(\Gamma)$
 have to be met.
Otherwise repeat.
\[
\infer[(prg)^{\infty}]{((\mathcal{E}^{X}_{j}(\sigma))_{j\neq i},\mathcal{E}^{X}_{i}(\sigma))\vdash\Gamma,E_{A}(m)}
{
\{
((\mathcal{E}^{X}_{j}(\sigma))_{j\neq i},\mathcal{E}^{X}_{i}(\sigma)\cup\{n\})\vdash\Gamma,n\not<^{*}_{A}m, E_{A}(n)
:n\in\mathbb{N}
\}
}
\]
{\bf Case 1}. $lh(\sigma)=3\langle i,n\rangle+1$: 
Apply the inference $(ACA)$ backwards with the first-order $A\equiv A_{i}$
and an eigenvariable $Y_{j}$
 if $Var(A)\subset Var(\Gamma)\cup\{P\}$.
 \[
\infer[(ACA)]{\Gamma}
{
Y_{j}\neq A,\Gamma
}
\]
Otherwise repeat
\\
{\bf Case 2}. $lh(\sigma)=3i+2$:
Apply the inference $(WP)$ backwards with the relation $<_{A_{i}}$.
\\

If the tree ${\cal T}$ is not well-founded, then let $\mathcal{R}$ be an infinite path through ${\cal T}$.
We see for any $i,n$ that
at most one of 
 $Q(n)$ or $\bar{Q}(n)$ is on $\mathcal{R}$
 for $Q\in\{E_{i},Y_{i},P:i\in\mathbb{N}\}$,
and 
$[(P(n))\in\mathcal{R}\Rarw n\not\in\mathcal{P}]\,\&\,[(\bar{P}(n))\in\mathcal{R}\Rarw n\in\mathcal{P}]$
 due to the axioms
$\Gamma,L$ with $L\in{\rm Diag}(\mathcal{P})$.
Let $(\mathcal{Q})_{i}$ be the set defined by
$n\in(\mathcal{Q})_{2i} \Leftrightarrow (E_{i}(n))\not\in\mathcal{R}$
and
$n\in(\mathcal{Q})_{2i+1} \Leftrightarrow (Y_{i}(n))\not\in\mathcal{R}$.

$(\mathcal{P},(\mathcal{Q})_{i})_{i\in\mathbb{N}}$ is shown to be a countable coded $\omega$-model of 
${\rm ACA}_{0}+{\rm WOP}({\sf g})$ as follows.
The search procedure is fair, i.e., each formula is eventually analyzed on every path.
To ensure fairness, formulas in sequents $\Gamma$ are assumed to stand in a queue.
The head of the queue is analyzed in {\bf Case 0}, and the analyzed formula moves to the end of the queue
in the next stage.
We see from the fairness that
${\rm Diag}(\mathcal{P},(\mathcal{Q})_{i})_{i\in\mathbb{N}}\not\models A$ 
first by induction on the number of occurrences of 
logical connectives in first-order
formulas $A$ on the path $\mathcal{R}$,
and then for $\Pi^{1}_{1}$-formulas ${\rm TI}[<_{A}]$ and $\Sigma^{1}_{1}$-formulas
$\lnot{\rm TI}[<_{{\sf g}_{A}}]$.
Moreover
${\rm Diag}(\mathcal{P},(\mathcal{Q})_{i})_{i\in\mathbb{N}}\models{\rm ACA}_{0}$ since the inference rules $(ACA)$
are analyzed for every $A_{i}$.
Finally we show
${\rm Diag}(\mathcal{P},(\mathcal{Q})_{i})_{i\in\mathbb{N}}\models{\rm WOP}({\sf g})$.
Assume that ${\rm Diag}(\mathcal{P},(\mathcal{Q})_{i})_{i\in\mathbb{N}}\models{\rm WO}[<_{A}]$
for a first-order $A$.
The path $\mathcal{R}$ passes through an inference $(WP)$ for the relation $<_{A}$.
If $\mathcal{R}$ passes through the rightmost upper sequent
$\lnot{\rm TI}[<_{{\sf g}_{A}}]$, then
 ${\rm Diag}(\mathcal{P},(\mathcal{Q})_{i})_{i\in\mathbb{N}}\not\models\lnot{\rm TI}[<_{{\sf g}_{A}}]$,
 i,e.,  ${\rm Diag}(\mathcal{P},(\mathcal{Q})_{i})_{i\in\mathbb{N}}\models{\rm TI}[<_{{\sf g}_{A}}]$,
 and we are done.
Suppose that $\mathcal{R}$ passes through an $n_{0}$-th upper sequent
$((\mathcal{E}_{j}^{X}(\sigma_{0}))_{j\neq i},\mathcal{E}^{X}_{i}(\sigma_{0}))\vdash\Gamma_{0},E_{A}(n_{0})$ 
and $E_{A}=E_{i}$ with $i=\lceil A\rceil$.
Since the condition (\ref{eq:normal}), $n_{0}\in\mathcal{E}^{X}_{i}(\sigma_{0})=\{n_{0}\}$ is met,
the formula $E_{A}(n_{0})$ is analyzed after a number of steps at a $(prg)^{\infty}$,
and $\mathcal{R}$ passes through an $n_{1}$-th branch
$((\mathcal{E}_{j}^{X}(\sigma_{1}))_{j\neq i},\mathcal{E}^{X}_{i}(\sigma_{1}))\vdash\Gamma_{1},
n_{1}\not<_{A}^{*}n_{0},E_{A}(n_{1}),E_{A}(n_{0})$.
We obtain ${\rm Diag}(\mathcal{P},(\mathcal{Q})_{i})_{i\in\mathbb{N}}\not\models n_{1}\not<_{A}^{*}n_{0}$,
 i.e., $n_{1}<_{A}^{*,\mathcal{P},\mathcal{Q}}n_{0}$.
 Also $\{n_{0},n_{1}\}\subset\mathcal{E}_{i}^{X}(\sigma_{1})$.
In this way we obtain an infinite descending chain 
$\cdots<_{A}^{*,\mathcal{P},\mathcal{Q}}n_{2}<_{A}^{*,\mathcal{P},\mathcal{Q}}n_{1}<_{A}^{*,\mathcal{P},\mathcal{Q}}n_{0}$ from $\mathcal{R}$, contradicting the assumption 
${\rm WO}[<^{\mathcal{P},\mathcal{Q}}]$.
\\


In what follows assume that the tree ${\cal T}$ is well-founded.
Let $\Lambda$ denote the least epsilon number
larger than the order type of the Kleene-Brouwer ordering $<_{KB}$
on the well-founded tree ${\cal T}$.
We have ${\rm WO}({\sf g}^{\prime}(\Lambda))$
by ${\rm WOP}({\sf g}^{\prime})$ and ${\rm WO}(\Lambda)$.

For $b<\Lambda$  let us write $S+(ACA)\vdash^{b}_{c}\Gamma$ 
when there exists a derivation of $\Gamma$ in 
${\rm Diag}(\mathcal{P})+(prg)^{\infty}+(WP)+(ACA)$ such that
its depth is bounded by $b$, the depth of nested applications of the rules $(WP)$
 is bounded by $c$, and the condition (\ref{eq:normal}) is enjoyed for each 
 inference $(prg)^{\infty}$ in the derivation, where a family $\mathcal{E}^{X}(\sigma)$ of finite sets
 is assigned to each node $\sigma$ in the derivation tree as in Definition \ref{df:attach}.
 
For the inference
\[
\infer[(ACA)]{\Gamma}
{
Y_{j}\neq A,\Gamma
}
\]
substitute $A$ for the eigenvaraible $Y_{j}$, 
and deduce the valid formula $A= A$ logically in a finite number of steps, and
then a $(cut)_{1st}$ yields the lower sequent $\Gamma$.
Axioms $\Gamma,\bar{Y}_{j}(n),Y_{j}(n)$ turns to another valid sequent
$\Gamma^{\prime}, \lnot A(n),A(n)$.
In $(WP)$, if $Y_{j}$ occurs in $B(Y_{j})$, then the variable $E_{B(Y_{j})}\equiv E_{i}$ with 
$i=\lceil B(Y_{j})\rceil$
should be renamed to $E_{B(A)}\equiv E_{k}$ with $k=\lceil B(A)\rceil$.
{\small
\[
\infer{\Gamma(Y_{j})}
{
\Gamma(Y_{j}), E_{B(Y_{j})}(n)
&
\lnot{\rm TI}[<_{{\sf g}_{B(Y_{j})}}],\Gamma(Y_{j})
}
\leadsto
\infer{\Gamma(A)}
{
\Gamma(A), E_{B(A)}(n)
&
\lnot{\rm TI}[<_{{\sf g}_{B(A)}}],\Gamma(A)
}
\]
}
Thus we obtain 
${\rm Diag}(\mathcal{P})+(prg)^{\infty}+(WP)+(cut)_{1st}\vdash^{\omega+b}_{b}\emptyset$
from ${\rm Diag}(\mathcal{P})+(prg)^{\infty}+(WP)+(ACA)\vdash^{b}_{b}\emptyset$,
and
${\rm Diag}(\mathcal{P})+(prg)^{\infty}+(WP)\vdash^{2_{p}(\omega+b)}_{2_{p}(b)}\emptyset$
for a $p<\omega$ as in Proposition \ref{prp:ce1st}.

Here the condition (\ref{eq:normal}) is forced in the search.


Theorem \ref{lem:WPbndtransf} yields 
$\emptyset\vdash^{\delta}_{0}\emptyset$
with $\delta=F(2_{p}(\omega+b),2_{p}(b))+2_{p}(\omega+b)$
 and $\mathcal{E}^{X}(\emptyset)=\Delta(\emptyset;\emptyset)=\emptyset$.
This means that in the $\omega$-logic, there exists a cut-free derivation of $\emptyset$ in depth
$\delta<{\sf g}^{\prime}(\Lambda)$, which is seen 
 from Proposition \ref{prp:Fg}.\ref{prp:Fg.5} and $b<\Lambda$.
We see by induction up to the ordinal ${\sf g}^{\prime}(\Lambda)$ that
this is not the case.
Therefore the tree ${\cal T}$ must not be well-founded.
Thus our proof of Theorem \ref{th:derivativemodel} is completed.





\section{Elimination of the inference for well-ordering principle}\label{sect:CE}
It remains to show Theorems \ref{th:TakeutimultiTI} and \ref{lem:WPbndtransf}.
\\

\noindent
({\bf Proof} of Theorem \ref{th:TakeutimultiTI}).
We can assume that the transitive closure $\prec^{*}$ of the relation $n\prec m$
is irreflexive.
Namely there is no sequence $(n_{0},\ldots,n_{k})\,(k\geq 1)$
such that $n=n_{0}=n_{k}$ and $\forall j<k(n_{j+1}\prec n_{j})$.
Suppose that there exists such a sequence.
By the assumption we obtain
$\{n_{0}\}\vdash^{\alpha_{0}}E(n_{0})$ for $\alpha_{0}=\alpha$.
Any positive literal $E(n_{0})$ is not an axiom in 
${\rm Diag}(\emptyset)$.
We see from $n_{0}\in\{n_{0}\}$ by induction on ordinals $\alpha_{0}$ that
there must be an inference $(prg)_{\prec}^{D}$ in the witnessed derivation,
and we obtain $\{n_{0},n_{1}\}\vdash^{\alpha_{1}}E(n_{0}),E(n_{1})$ for 
an $\alpha_{1}<\alpha_{0}$.
Again $P(n_{0}),P(n_{1})$ is not an axiom in
${\rm Diag}(\emptyset)$.
In this way we would obtain an infinite descending chain $\{\alpha_{m}\}_{m<\omega}$
of ordinals such that  $\{n_{j}\}_{j<k}\vdash^{\alpha_{m}}_{0}\{P(n_{j}):j<k\}$.




By recursion on $m$, we define 
a non-empty finite set $\mathcal{E}(m)$, and
an ordinal $\beta(m)\leq\alpha$ for which the followings hold for
$\Delta(\mathcal{E}(m)):=\{E(n): n\in\mathcal{E}(m)\}$.
\begin{eqnarray}
&&
\mathcal{E}(m)\subset\{n: m\preceq^{*}n\leq m\}
\,\&\,
\mathcal{E}(m)\vdash^{\beta(m)}\Delta(\mathcal{E}(m))
\nonumber
\\
&&
\forall n<m(m\prec^{*}n \to \beta(m)<\beta(n))
\label{eq:Takeutimulti}
\end{eqnarray}
{\bf Case 1}. $\lnot\exists n<m(m\prec^{*}n)$:
Let $\mathcal{E}(m)=\{m\}$
and $\beta(m)=\alpha$.
Then the conditions in (\ref{eq:Takeutimulti}) are fulfilled with 
$\Delta(\mathcal{E}(m))=\{E(m)\}$.
\\
{\bf Case 2}. Otherwise:
Pick a $k<m$ such that $m\prec^{*}k$ and
$\beta(k)=\min\{\beta(n): n<m, m\prec^{*}n\}$.

Then let $\mathcal{E}(m)=\mathcal{E}(k)\cup\{m\}$.
On the other hand we have $\mathcal{E}(k)\vdash^{\beta(k)}\Delta(\mathcal{E}(k))$.
The sequent $\Delta(\mathcal{E}(k))$ is not an axiom in ${\rm Diag}(\emptyset)$.
Search the lowest inference $(prg)_{\prec}^{D}$ 
in the derivation showing the fact $\mathcal{E}(k)\vdash^{\beta(k)}\Delta(\mathcal{E}(k))$:
\[
 \infer[(prg)_{\prec}^{D}]{\mathcal{E}(k)\vdash^{\beta^{\prime}}\Delta(\mathcal{E}(k))}
 {
  \{
  \mathcal{E}(k)\cup\{n\}\vdash^{\beta_{0}}\Delta(\mathcal{E}(k)), E(n): n\prec^{*} k^{\prime}
   \}
}
\]
where 
$\beta_{0}<\beta^{\prime}\leq\beta(k)$,
there may be some $(Rep)$'s below the inference $(prg)_{\prec}^{D}$,
and
$E(k^{\prime})\in\Delta(\mathcal{E}(k))$ is the main formula of the inference 
$(prg)_{\prec}^{D}$.
We have $m\prec^{*}k\preceq^{*}k^{\prime}$, and $m\prec^{*}k^{\prime}$.
Pick the $m$-th branch in the upper sequents.
We obtain $\mathcal{E}(m)\vdash^{\beta(m)}\Delta(\mathcal{E}(m))$
for $\beta(m):=\beta_{0}<\beta(k)$.
The conditions in (\ref{eq:Takeutimulti}) are fulfilled.

Now define a function $f(m)$ as follows.
\[
f(m)=\max\{\omega^{\beta(m_{0})}\#\cdots\#\omega^{\beta(m_{k})}: m_{0}\prec^{*}\cdots\prec^{*}m_{k}=m, 
m_{0},\ldots,m_{k-1}<m\}
\]
where $\#$ denotes the natural sum.
Note that the set 
$\{(m_{0},\ldots,m_{k}): m_{0}\prec^{*}\cdots\prec^{*}m_{k}=m, 
m_{0},\ldots,m_{k-1}<m\}$ is finite since $\prec^{*}$ is irreflexive.

We show the function $f$ is a desired embedding between $\prec^{*}$ and $<$.
Assume $m\prec^{*}n$, and let $m_{0},\ldots,m_{k}$ be a sequence such that
$f(m)=\omega^{\beta(m_{0})}\#\cdots\#\omega^{\beta(m_{k})}$,
with $m_{0}\prec^{*}\cdots\prec^{*}m_{k}=m$ and 
$m_{0},\ldots,m_{k-1}<m$.
We obtain $m_{i}\prec^{*}n$ for any $i\leq k$.
Let us partition the set $\{0,\ldots,k\}$ into two sets
$A=\{i\leq k: n<m_{i}\}$ and $B=\{i\leq k: m_{i}<n\}$.
Note that $m_{i}\neq n$ since $\prec^{*}$ is irreflexive.

By (\ref{eq:Takeutimulti}) we obtain $\beta(m_{i})<\beta(n)$ for each $i\in A$, and hence
$\#\{\omega^{\beta(m_{i})}:i\in A\}<\omega^{\beta(n)}$,
where
$\#\{\alpha_{1},\ldots,\alpha_{n}\}=\alpha_{1}\#\cdots\#\alpha_{n}$.

On the other hand we have 
$\#\{\omega^{\beta(m_{i})}:i\in B\}\leq
\max\{\omega^{\beta(n_{0})}\#\cdots\#\omega^{\beta(n_{\ell})}: n_{0}\prec^{*}\cdots\prec^{*}n_{\ell-1}, 
n_{0},\ldots,n_{\ell-1}<n\}$.
Therefore we conclude
$f(m)<f(n)$.
\hspace*{\fill} $\Box$


\begin{lemma}\label{lem:bndwset}
For each $j\leq\ell$, let $<_{j}$ be a first-order formula with $j=\lceil <_{j}\rceil$.
Let $\mathcal{E}^{X}=(\mathcal{E}^{X}_{j})_{j<\ell}$ be finite
sets, and $\mathcal{E}^{X}_{\ell}$ a finite set.
Let $\Gamma\subset\bigcup_{j<\ell}\Delta(\mathcal{E}^{X}_{j})$ be a sequent
and
$\Gamma_{\ell}\subset\Delta(\mathcal{E}^{X}_{\ell})=\{E_{\ell}(n): n\in\mathcal{E}^{X}_{\ell}\}$
a sequent.

In the calculus ${\rm Diag}(\mathcal{P},\emptyset)+(prg)^{\mathcal{E}}$,
assume that 
$(\mathcal{E}^{X},\mathcal{E}^{X}_{\ell})\vdash^{\alpha}\Gamma,\Gamma_{\ell}$
for $\mathcal{E}^{X}=(\mathcal{E}^{X}_{j})_{j<\ell}$.
Then either
$\mathcal{E}^{X}\vdash^{\alpha}\Gamma$ holds, or
$\mathcal{E}^{X}_{\ell}\vdash^{\alpha}\Gamma_{\ell}$ holds.
\end{lemma}
{\bf Proof}.\hspace{2mm}
We show the lemma by induction on $\alpha$.
Assume that
$(\mathcal{E}^{X},\mathcal{E}^{X}_{\ell})\vdash^{\alpha}\Gamma$ does not hold.
The set $\Gamma\cup\Gamma_{\ell}$ consisting of positive literals $E_{i}(n)$, is not an axiom
in ${\rm Diag}(\mathcal{P},\emptyset)+(prg)^{\emptyset}$.


Consider the case when the last inference is a $(prg)^{\emptyset}$
for a $<_{j}$:
\[
\infer[(prg)^{\emptyset}]{(\mathcal{E}^{X},\mathcal{E}^{X}_{\ell})\vdash^{\alpha}\Gamma,\Gamma_{\ell}}
{
\{
(\mathcal{E}^{X},\mathcal{E}^{X}_{\ell})_{j,m}\vdash^{\beta}\Gamma,\Gamma_{\ell},E_{j}(\bar{m})
: m<^{*,\emptyset}_{j} n
\}
}
\]
where $E_{j}(\bar{n})$ is in $\Gamma\cup\Gamma_{\ell}$,
and $(\mathcal{E}^{X},\mathcal{E}^{X}_{\ell})_{j,m}$ denotes
the sequence $(\mathcal{E}^{X},\mathcal{E}^{X}_{\ell})$ except
$\mathcal{E}^{X}_{j}$ is replaced by $\mathcal{E}^{X}_{j}\cup\{m\}$.
We have (\ref{eq:normal}), $n\in\mathcal{E}^{X}_{j}$.

First consider the case $j\neq\ell$.
By the assumption we see that there exists an 
$m<^{*,\emptyset}_{j} n$
such that $(\mathcal{E}^{X},\mathcal{E}^{X}_{\ell})_{j,m}\vdash^{\beta}\Gamma,E_{j}(\bar{m}),E_{j}(\bar{n})$
does not hold. IH yields 
$(\mathcal{E}^{X},\mathcal{E}^{X}_{\ell})\vdash^{\beta}\Gamma_{\ell}$.

Second consider the case $j=\ell$.
We see from the assumption that
for each $m<^{*,\emptyset}_{\ell} n$,
$(\mathcal{E}^{X},\mathcal{E}^{X}_{\ell})_{\ell,m}\vdash^{\beta}\Gamma_{\ell},E_{\ell}(\bar{m})$ holds.
Then an inference $(prg)^{\emptyset}$ yields
$(\mathcal{E}^{X},\mathcal{E}^{X}_{\ell})\vdash^{\alpha}\Gamma_{\ell}$.
\hspace*{\fill} $\Box$
\\

\noindent
({\bf Proof} of Theorem \ref{lem:WPbndtransf}).
Let us prove Theorem \ref{lem:WPbndtransf}
by induction on $\beta$.
Suppose that in the calculus ${\rm Diag}(\mathcal{P})+(prg)^{\infty}+(WP)$,
$\vdash^{\beta}_{\alpha}\Phi,\Gamma$ holds in a derivation $\pi$
for a sequent $\sigma:\Phi,\Gamma$ such that
$\Phi$ is a $\Sigma^{1}_{1}$-formulas with 
${\rm Diag}(\mathcal{P},\emptyset)\not\models \bigvee\Phi$ and
$\Gamma\subset\Delta(\mathcal{E}^{X}(\sigma);\Phi,\Gamma)$.
Moreover the condition (\ref{eq:normal}) is assumed to be
enjoyed for each $(prg)^{\infty}$
occurring in $\pi$.
Let $\mathcal{E}^{X}=\mathcal{E}^{X}(\sigma)$.

If $\Phi,\Gamma$ is an axiom in ${\rm Diag}(\mathcal{P})+(prg)^{\infty}+(WP)$,
then $\Delta(\mathcal{E}^{X};\Gamma)$ is an axiom in ${\rm Diag}(\mathcal{P},\emptyset)+(prg)^{\mathcal{E}}$
since ${\rm Diag}(\mathcal{P},\emptyset)\not\models\bigvee\Phi$.
For example, consider the case when $\{\bar{E}_{i}(m),E_{i}(m)\}\subset\Phi\cup\Gamma$.
Since $\Gamma$ contains positive literals only,
we may assume $\bar{E}_{i}(m)\in\Phi$ and $E_{i}(m)\in\Gamma$.
From ${\rm Diag}(\mathcal{P},\emptyset)\models\bar{E}_{i}(m)$ 
we see that this is not the case.



Consider the last inference in the derivation showing 
$\vdash^{\beta}_{\alpha}\Phi,\Gamma$.
\\
{\bf Case 1}. The last inference is a $(prg)^{\infty}$. For $\gamma<\beta$
and $i=\lceil A\rceil$, we have for an $E_{i}(m)\in\Phi\cup\Gamma$
\[
\infer[(prg)^{\infty}]{((\mathcal{E}^{X}_{j})_{j\neq i},\mathcal{E}^{X}_{i})\vdash^{\beta}_{\alpha}\Phi,\Gamma}
{
\{
((\mathcal{E}^{X}_{j})_{j\neq i},\mathcal{E}^{X}_{i}\cup\{n\})\vdash^{\gamma}_{\alpha}
\Phi,n\not<^{*}_{A}m,\Gamma,E_{i}(n):
n\in\mathbb{N}
\}
}
\]
IH yields 
$((\mathcal{E}^{X}_{j})_{j\neq i},\mathcal{E}^{X}_{i}\cup\{n\})\vdash^{F(\gamma,\alpha)+\gamma}
\Delta_{n}$
for each $n<^{*,\emptyset}_{A}m$,
where $E_{i}(n)\in \Delta_{n}=\Delta((\mathcal{E}^{X}_{j})_{j\neq i},\mathcal{E}^{X}_{i}\cup\{n\};\Phi,n\not<^{*}_{A}m,\Gamma,E_{i}(m),E_{i}(n))$,
and 
$\Delta((\mathcal{E}^{X}_{j})_{j\neq i},\mathcal{E}^{X}_{i}\cup\{n\};\Phi,\Gamma,E_{i}(m))\cup\{E_{i}(n)\}=\Delta_{n}
$.
By the assumption we obtain (\ref{eq:normal}), $m\in\mathcal{E}^{X}_{i}$.
An inference $(prg)^{\emptyset}$ with $F(\gamma,\alpha)+\gamma<F(\beta,\alpha)+\beta$ 
yields
$((\mathcal{E}^{X}_{j})_{j\neq i},\mathcal{E}^{X}_{i})\vdash^{F(\beta,\alpha)+\beta}
\Delta((\mathcal{E}^{X}_{j})_{j\neq i},\mathcal{E}^{X}_{i};\Phi,\Gamma,E_{i}(m))$.
\\

\noindent
{\bf Case 2}. The last inference is a $(WP)$. 
For $\gamma<\beta$, $\alpha_{0}<\alpha$, $Var(A)\subset Var(\Gamma)\cup\{P\}$, $i=\lceil A\rceil$, and
the variable $E_{i}$ not occurring in $\Gamma$, we have
\[
\infer[(WP)]{(\mathcal{E}^{X}_{j})_{j\neq i}\vdash^{\beta}_{\alpha}\Phi,\Gamma}
{
\{
((\mathcal{E}^{X}_{j})_{j\neq i},\{n\})\vdash^{\gamma}_{\alpha_{0}}\Phi,\Gamma, E_{i}(n)
: n\in\mathbb{N}
\}
&
\mathcal{E}^{X}\vdash^{\gamma}_{\alpha_{0}}\lnot{\rm TI}[<_{{\sf g}_{A}}],\Phi,\Gamma
}
\]



For the left upper sequent we have for each $n\in\mathbb{N}$
\[
((\mathcal{E}^{X}_{j})_{j\neq i},\{n\})\vdash^{\gamma}_{\alpha_{0}}\Phi,\Gamma, E_{i}(n)
\]
By IH we obtain 
$((\mathcal{E}^{X}_{j})_{j\neq i},\{n\})\vdash^{F(\gamma,\alpha_{0})+\gamma}\Delta((\mathcal{E}^{X}_{j})_{j\neq i};\Phi,\Gamma),E_{i}(n)$.
Here note that
 $\Delta((\mathcal{E}^{X}_{j})_{j\neq i};\Phi,\Gamma)\cup\{E_{i}(n)\}=\Delta((\mathcal{E}^{X}_{j})_{j\neq i},\{n\};\Phi,\Gamma,E_{i}(n))$.
From Lemma \ref{lem:bndwset} we see that
either
$(\mathcal{E}^{X}_{j})_{j\neq i}\vdash^{F(\gamma,\alpha_{0})+\gamma}\Delta(\mathcal{E}^{X};\Phi,\Gamma)$
or
$((\mathcal{E}^{X}_{j})_{j\neq i},\{n\})\vdash^{F(\gamma,\alpha_{0})+\gamma}E_{i}(n)$ holds.
If $(\mathcal{E}^{X}_{j})_{j\neq i}\vdash^{F(\gamma,\alpha_{0})+\gamma}\Delta(\mathcal{E}^{X};\Phi,\Gamma)$, then we are done.

Assume $((\mathcal{E}^{X}_{j})_{j\neq i},\{n\})\vdash^{F(\gamma,\alpha_{0})+\gamma} E_{i}(n)$,
i.e., $\{n\}\vdash^{F(\gamma,\alpha_{0})+\gamma} E_{i}(n)$
 for every $n$.
By Theorem \ref{th:TakeutimultiTI} we obtain
an embedding $f$
from $<_{A}^{\emptyset}$ to $\omega^{F(\gamma,\alpha_{0})+\gamma+1}$, which yields
an embedding from $<_{{\sf g}(A)}^{\emptyset}$
to $\delta:={\sf g}(\omega^{F(\gamma,\alpha_{0})+\gamma+1})$ by Proposition \ref{prp:dilate}.
Hence we see from ${\rm WO}(\delta)$ that
${\rm Diag}(\mathcal{P},\emptyset)\models {\rm TI}[<_{{\sf g}_{A}},C]$
for any first-order formulas $C$.
Therefore ${\rm Diag}(\mathcal{P},\emptyset)\models \lnot{\rm TI}[<_{{\sf g}_{A}}]$.

Second consider the right upper sequent. 
IH yields 
\[
(\mathcal{E}^{X}_{j})_{j\neq i}\vdash^{F(\gamma,\alpha_{0})+\gamma}\Delta(\mathcal{E}^{X};\Phi,\Gamma)
\]
On the other side Proposition \ref{prp:Fg}.\ref{prp:Fg.1} with (\ref{eq:Fsuccessor}) yields 
$F(\gamma,\alpha_{0})+\gamma\leq F(\gamma,\alpha)+\gamma\leq F(\beta,\alpha)+\beta$.
Hence the assertion $\mathcal{E}^{X}\vdash^{F(\beta,\alpha)+\beta}\Delta(\mathcal{E}^{X};\Phi,\Gamma)$ follows.
\\
{\bf Case 3}. The last inference is other than $(prg)^{\infty}$ and $(WP)$.

Consider first the case when the last inference is a rule for existential second-order quantifier.
\[
\infer[(\exists_{1st}^{2})]{(\mathcal{E}^{X}_{j})_{j\neq i}\vdash^{\beta}_{\alpha}\lnot{\rm TI}[<_{{\sf g}_{A}}],\Phi,\Gamma}
{
(\mathcal{E}^{X}_{j})_{j\neq i}\vdash^{\gamma}_{\alpha} \lnot{\rm TI}[<_{{\sf g}_{A}}],\lnot {\rm TI}[<_{{\sf g}_{A}},C],\Phi,\Gamma
}
\]
where $\gamma<\beta$ and $C$ is a first-order formula such that
$Var(C)\subset Var(A,\Gamma)$.
IH yields
$(\mathcal{E}^{X}_{j})_{j\neq i}\vdash^{F(\gamma,\alpha)+\gamma} \Delta(\mathcal{E}^{X};\Phi,\Gamma)$ for
$\Delta(\mathcal{E}^{X};\Phi,\Gamma)=\Delta(\mathcal{E}^{X};\lnot {\rm TI}[<_{{\sf g}_{A}},C],\Phi,\Gamma)$
by $Var(A,C)\subset Var(\Phi,\Gamma)$.

Second consider the case when the last inference is a rule $(\bigwedge)$
For $\gamma<\beta$ we have
\[
\infer[(\bigwedge)]{\mathcal{E}^{X}\vdash^{\beta}_{\alpha}\Phi,\Gamma}
{
\{
\mathcal{E}^{X}\vdash^{\gamma}_{\alpha}A_{n},\Phi,\Gamma
: n\in\mathbb{N}
\}
}
\]
where $\bigwedge_{n}A_{n}$ is in the set $\Phi$.
Let $n$ be the least number such that ${\rm Diag}(\mathcal{P},\emptyset)\not\models A_{n}$.
IH yields 
$\mathcal{E}^{X}\vdash^{F(\gamma,\alpha)+\gamma}\Delta(\mathcal{E}^{X};\Phi,\Gamma)$.

Other cases are similarly seen.
\hspace*{\fill} $\Box$


