数理解析研究所講究録976 巻 1997 年 97-124

97

From the Attic
Toshiyasu Arai
Faculty of Integrated Arts and Sciences
Hiroshima University$(\# l\dot{\mathrm{I}}\#\phi\tilde{\chi}l?)$$\mathrm{A}\mathrm{b}\mathrm{s}\mathrm{t}\mathrm{r}\mathrm{a}\mathrm{c}^{\wedge}\iota$

We gather the following miscelaneous results in proof theory from the attic.
1. A provably well founded elementary ordering admits an elementary order preserving map.

2. A simple proof of an elementary bound for cut elimination in propositional calculus
3. Equivalents for Bar Induction, e.g., reflection schema for$\omega$logic

4. Direct computations in an equatinal calculus PRE
5. Intuitionistic fixed point theories are conservative extensions of $HA$ .

6. Proof theoretic strengths of classical fixed points theories
7. An equivalence between transfinite induction rule and iterated reflection schema over$I\Sigma_{n}$8. Derivation lengths of finite rewrite rules reducing under lexicographic path orders and provably total
functions in theories between
and$I\Sigma_{1}$$I\Sigma_{2}$Each section can be read separately in principle.

1

Provably Well Founded Relations

In this section we show that if an elementary recursive
provably well founded in Peano Arithmetic$PA$ , then there exists an elementary recursive order preserving map
into an initial segment of . This
gives an improvement on a result by Harrington and Takeuti (cf. [24], Theorem 13.6 and [10], p.33).
We say that a binary relation is provably well founded in $PA$ if$\mathrm{r}\mathrm{e}\mathrm{l}\mathrm{a}\mathrm{t}\mathrm{i}_{0}\mathrm{n}\prec \mathrm{i}\mathrm{s}$$f\mathrm{o}\mathrm{f}\prec$$\epsilon_{0}$$\prec$$PA(X)\vdash\forall n(\forall k\prec nX(k)\supset X\langle n))\supset\forall nX(n)$where $PA(X)$ denotes the Peano Arithmetic with an additional unary predicate $X$ . Letelementary recursive
well ordering and ERA the Elementary Recursive Arithmetic.

$<_{\epsilon_{\mathrm{O}}}$

denote a standard$\epsilon_{0}$Theorem 1.1 $If\prec is$ an irreflexive, transitive and provably well founded (not necessarily a total ordering)
relation on , then th.ere exists an ordinal
and an elementary recursive function so that ERA proves
that
$f$

$\alpha<\epsilon_{0}$$\omega$$\forall n$( $n\neq$ n)&\forall n, $m,$ $k(n\prec m\prec k\supset n\prec k)\supset$[ $(n\prec k\supset f(n)<_{\epsilon_{0}}f$ (k)&f]$\forall n,$$k$$(n)<_{\epsilon_{0}}\alpha$

Proof. Work in ERA. From the proof in [24] pp.149-154 we see that there exist an ordinalelementary recursive function so that $h(k)$ is an additive principal number, i.e.,
and$h$and anfor some$\alpha<e_{0}$$h(k)=\omega^{\beta}$$<_{\epsilon_{0}}\omega^{\alpha}$$\beta$(1)$\forall k[\forall n<k(k\prec n\supset h(k)<_{\epsilon_{0}}h(n))]$(Define$<\mathrm{d}\mathrm{e}\mathrm{n}\mathrm{o}\mathrm{t}\mathrm{e}\mathrm{S}$the usual ordering on$\omega$. A definition of the function$f(n)= \max\{<e_{0}h(n\mathrm{o})\#\cdots\# h(n_{l}) :Herefunction

Claim 1.1

$n\prec k\Rightarrow f(n)<_{\epsilon_{0}}f(k)$will be sketched below.)n_{0}\prec\cdots\prec n_{l}=n\ n0, .5 \cdot, n\iota-1<n\}$denotes the maximum with respect to the ordering
is elementary recursive and we have$\max_{<_{e_{0}}}$

$f$

$h$

$<_{\epsilon_{0}}$and note that$\prec$is irreflexive. The

98
so that $f(n)=h(n_{0})\#\cdots\neq h(n_{l}),$Assume $n\prec k$ . Choose a sequence.. . $\prec n_{l}=n\ n_{0},$ $n\iota-1<n$ . By transitivity
for any $i\leq l$ . Partition the set
have
into two sets and as follows: $A=\{i\leq l : k<n_{i}\},$ $B=\{i\leq l : n_{i}<k\}$ ( is irreflexive.) By (1) wefor each $i\in A$ , and hence $\#\sum\{h(n_{i}) : i\in A\}<_{\epsilon_{0}}h(k)$ since $h(k)$ is additive principal.
have)denotes(,, using the transitivity
On the other hand we

Proof of Claim 1.1.

$\blacksquare$$n_{0},$$\ldots,$$n_{0}\prec$$n_{l}$$n_{i}\prec k$$\mathrm{o}\mathrm{f}\prec \mathrm{w}\mathrm{e}$$\{0, \ldots, l\}$$\ldots,$

$A$

$B$

$\prec$$h(n_{i})<_{\epsilon_{0}}h(k)$$\#\sum\{\alpha_{0},$$\alpha_{n}\}$$\alpha 0\#\cdots\#\alpha_{n}.$$\ldots,$$\mathrm{o}\mathrm{f}\prec$$.\mathrm{h}\mathrm{a}\mathrm{v}\mathrm{e}$$\#\sum\{h(n_{i}):i\in B\}\leq_{\epsilon_{0}}$$\max_{0}\{<_{C}h(k_{0})\#\cdots\# h(k_{m}-1) :k_{0}\prec\cdots\prec k_{m-1}\prec k\ k_{0}, \ldots, k_{m-1}<k\}$

Therefore we get $f(n)<_{\epsilon_{0}}f(k)$ .

$\square$Sketch of a definition of the function .
We follow notations and terminology in [24].
$h$1) Define a $TJ$ proof exactly as in [24], p.149. That is, a TJ proof may have TJ initial sequents as extra initial

sequentes:
TJ initial sequent $\forall x\prec tX(x)arrow X(t)$ ( $X(t)$ is called the principal formula of the TJ initial sequent.).
$x(mn)$ . We identify thenumeral
Also a TJ proof ends with a sequent of thewith the number $m$ .
$\mathrm{f}\mathrm{o}\mathrm{r}\mathrm{m}arrow X(m_{0}),$$m\mathrm{t}\mathrm{h}$$\ldots,$

2) The ordinal assignment $o(P)$ for a TJ proof $P$ is defined as in [24].
3) A TJ proof is called noncritical if one of the reduction steps for $PA$ which lowers the ordinal applies to it.
Otherwise it is called critical.
4) We say that a TJ proof $P’$ is the noncritical reduct of a noncritical TJ proof $P$ if $P’$ is obtained from $P$ by

applying a reduction step for $PA$ which lowers theordina.l.

5) We call a formula in the end-piece of a TJ proof, a principal $TJ$ descendent if it is a descendent of a principal
formula of a TJ initial sequent. If is a critical TJ proof, then the endsequent of contains a principal
TJ descendent (cf. [24], pp.151-152.).
$P$

$P$

$x(mn)$ , and be a number such thatfor every $i\leq n$ .
6) Let $P$ be a critical TJ proof$x(mn)$ is a principal TJ descendent
For some $i\leq n$ the fomula $X(m_{i})$ in theof a TJ initial sequent $\forall x\prec m_{i}X(x)arrow X(m_{i})$ . Then add the formula $X(k)$ to the endsequent andreplace the TJ initial sequent $\forall x\prec m_{i}X(x)arrow X(m_{i})$ by the following proof:$\mathrm{o}\mathrm{f}arrow X(m_{0}),$$k\prec m_{i}$$k$$\ldots,$$\mathrm{e}\mathrm{n}\mathrm{d}_{\mathrm{S}\mathrm{e}\mathrm{q}\mathrm{u}\mathrm{e}\mathrm{n}}\mathrm{t}arrow X(m_{0}),$$\ldots,$$\frac{\frac{arrow k\prec m_{i}X(k)arrow x(k)}{\frac{k\prec m_{i}\supset x(k)arrow x(k)}{\forall x\prec miX(x)arrow x(k)}}}{\forall x\prec m_{i}X(x)arrow X(k),x(mi)}$If $P’$ is obtained from a critical

$P$

and

$k$

in this way, then we say that $P’$ is the critical reduct of

$P$

at .
$k$

7) Since
is provably well founded, we have in the system formed from $PA(X)$ by adjoining TJ initial$P(k)$ denotes a TJ
for a free variable . Then, for eachsequents, a proof $P(a)$ of the$P(a)$
by substituting the numeral for the variable .
obtained fromproof$\prec$$k$8) Now let us define, for each number , a TJ proof(in the endsequent of , then$k$$k\preceq n$$P_{k}$

by induction onor $k=n$ ).

$P_{k}$$\Leftrightarrow dfk\prec n$8.1) The case $\neg\exists n<k(k\prec n)$ : Then $P_{k}=P(k)$ . The endsequent of
8.2) The case $\exists n<k(k\prec n)$ : Pick an $n_{0}<k$ so that
8.21) If

$P_{n_{0}}$

$k,$

$a$

$\mathrm{s}\mathrm{e}\mathrm{q}\mathrm{u}\mathrm{e}\mathrm{n}\mathrm{t}arrow X(a)$$\mathrm{o}\mathrm{f}arrow X(k)$is noncritical, then$P_{k}$$k\prec n_{0}$

and

$k$

$a$

so that for every , if $X(n)$ occurs$n$$P_{k}\mathrm{i}\mathrm{s}arrow X(k)$.

$\forall n<k(k\prec n\Rightarrow o(P_{n_{0}})\leq_{\epsilon_{0}}o(P_{n}))$is defined to be the noncritical reduct of$P_{n_{0}}$.

.

at . In 8.21 the endsequent is
is defined to be the critical reduct ofis critical, then.
unchanged, while in 8.22 it is augmented with the formula $X(k)$ . In any cases we have8.22) If

$P_{n_{0}}$$P_{k}$$P_{n_{0}}$$k$$o(P_{k})<_{\epsilon_{0}}o(P_{n_{0}})$9) Finally we set: $h(k)=_{df}\omega^{O}(P_{k})$ . Then the required condition (1) is clearly enjoyed.
$\square$99
2

Elementary bound for cut elimination in propositional calculus

It is well known that the length of the shortest cut free proof is bouded by an elementary function of thelength of the original proof in propositional calculus, e.g.,. In this section we give a simple proof of thisfact.This yields $S_{2}^{0}(X)\neq T_{2}^{0}(X)$ as a corollary.
Letdenote a classical propositional calculus in a Tait calculus. To be definite
denotes the calculus
for the propositional part in [20].
denotes sequents, i.e., finite sets of formulae. $(Ax)\Gamma,$(for anatomic ) is the only initial sequent in. Inference rules areand (cut). A precise fomulation ofthese rules is irrelevant to our proof. Each proof in
is a tree of sequents.
, the depth of , denoted by $dp(P)$ , is defined to be the depth of the tree , i.e., the length
For a proof inof the longest branch in the tree . The length of , denoted by $lh(P)$ , is defined to be the total number ofoccurrences of inference rules in . Clearly we have $lh(P)<2^{dp(P)}$ since each inference rule is at most binary.
$\mathrm{c}\mathrm{f}.[15]$$LK_{0}$$LK_{0}$$\Gamma,$$\neg A,$ $A$$\Delta$$A$$LK_{0}$$(\wedge),$$(\vee)$$LK_{0}$$P$$P$$LK_{0}$

$P$

$P$

$P$

$P$

Theorem 2.1 If

is a proof of a sequent$dp(P)\leq lh(P_{0})$ .
Therefore $lh(P)<2^{lh(P_{0}})$ .
$P_{0}$$\Gamma_{0}$in$LK_{0}$, then there exists a cut free proof $P$ of

so that$\Gamma_{0}$Proof. First eliminate cuts in the given proof
by a usual cut elimination procedure, e.g., in [20]. The
resulting cut free proof is denoted by. We say that two infernce rules
andare similar if 1) these are
the same type of rules, e.g., both rules are
and 2) their auxiliary formulae and principal formulae are thesame. We denote this equivalence relation by. For example,$P_{0}$$P^{cf}$$J_{0}$$J_{1}$$(\wedge)$$J_{0}\simeq J_{1}$$\frac{\Gamma,A_{0}\Gamma,A_{1}}{\Gamma,A_{0}\wedge A_{1}}J_{0}$$\frac{\Delta,B_{0}\Delta,B_{1}}{\Delta,B_{0}\wedge B_{1}}J_{1}$.
Then it is obvious that for each inference ruleinthere exists a $J’$ insuch that $J\simeq J’$ . Hence$k\leq lh(P_{0})$ with the maximum numberof equivalence classes of inference rules in a branch in. Thus it
suuffices to show that we can collapse two similar inference rules in a branch into a single one. For example if
a rule$J_{0}\simeq J_{1}\Leftrightarrow(A_{0}, A_{1})=(B_{01}, B)$$P^{cj}$$J$$P_{0}$$P^{cf}$$k$$\frac{\Gamma,A_{0}\Gamma,A_{1}}{\Gamma,A_{0^{\wedge}}A_{1}}J_{0}$is above the left uppersequent$\Delta,$$A_{0}$of another rule$\frac{\Delta,A_{0}\triangle,A_{1}}{\Delta_{)}A_{0\wedge}A_{1}}J_{0}$then eliminate
to get the sequent
and absorb the formula
into the principal fomulaA
at . In this way we get another cut free proof $P$ such that no branch in $P$ contains a pair of similar inference
rules. Therefore $dp(P)\leq lh(P_{0)}$ as desired.
$J_{0}$$\Gamma,$$A_{0}\wedge A_{1},$ $A_{0}$$A_{0}$$A_{1}$$J_{1}$$\square$Let
denote a bounded arithmetic obtained from Buss’in [5] by adding a unary predicate $X$
together with the equality axiom for the extra $X$ and replacing–PIND by
–PIND.
denotes the set of sharply bounded formulae in the language augmented by $X$ . Also
obtained fromby replacing–PIND by $\Sigma_{0}^{b}(X)-IND$ . We show:$S_{2}^{0}(X)$$S_{2}^{1}$$\Sigma_{0}^{b}(x)$$\Sigma_{1}^{b}$$\Sigma_{0}^{b}(X)$$T_{2}^{0}(X)\mathrm{i}\mathrm{s}$$S_{2}^{0}(X)$$\Sigma_{0}^{b}(x)$Corollary 2.1$S_{2}^{0}(X)\forall X(\mathrm{o})$A $\forall x(X(X)\supset X(x+1))\supset\forall xX(x)\prime i.e.,$ $S_{2}^{0}(X)\neq T_{2}^{0}(x)$ .

Assume that $S_{2}^{0}(X)\vdash X(\mathrm{O})\wedge\forall x(X(X)\supset X(x+1))\supset\forall xX(x)$ . Let denote a system arising fromsuch that 1) the language of is the same as one of
we add initial sequents $X(0)$ in and 3) we
add an inference rule
$S$

$S$

$S_{2}^{0}(X),$$S_{2}^{0}(x)$$2)$$\Gamma,$$S$$\frac{\Gamma,X(t)}{\Gamma,X(t+1)}(prg)$

Then we have $S\vdash X(a)$ for a variable .
Let denote a propositional calculus arising fromsuch that 1) the atoms ininitial sequentsin and 3) we add an inference rule $(prg_{n})$ for each
$a$

$T$

$LK_{0}$$\Gamma,$$X_{0}$$T$$T$

are $X_{n}(n\in\omega),$$2)$

we add$n\in\omega$$\frac{\Gamma,X_{n}}{\Gamma,X_{n+1}}(prg_{n})$sentence a propositional formula
is associated as follows: 1) for an atomic without
if is true, $A^{*}=\neg X_{0}$ otherwise. 2) $X(t)^{*}=X_{n}$ with the value of the closed term t. 3)
commutes with any propositional connectives. 4) $(\exists x\leq tA(x))^{*}=\{A(i)*:i\leq n\}$ with the value of the
For each$A$$\Sigma_{0}^{b}(x)$$X,$ $A^{*}=X_{0}$

$A$

$A$

$A^{*}$

$n$

$*$

$n$

100
sentences,. For a sequent $\Gamma=\{A_{0}, \ldots , A_{m}\}$ consisting solely ofclosed term and similarly for.
we setof variables.
sequent whose free variables are among the sequenceLetdenote aof natural numbers
denotes the result of simultaneous substitution
For a sequencefor . Then it is easy to show:$\Sigma_{0}^{b}(X)$$\forall x\leq t$$t$$\Gamma^{*}=\{A_{0}^{*}, \ldots, A^{*}\}m$$\overline{a}=(a_{0}, \ldots, a_{m})$$\Sigma_{0}^{b}(X)$$\Gamma(\overline{a})$$\overline{n}=(no, \ldots, n_{m})$$\Gamma(\overline{n})$$n_{i}$$a_{i}$

Lemma 2.1 If
in such that

$S\vdash\Gamma(\overline{a})$, then there exists a polynomial$f(\overline{a})$such that for any$\overline{n}$there exists a proofof$P_{\overline{n}}$$T$$\Gamma(\overline{n})$$lh(P_{\overline{n}})\leq f(|\overline{n}|)=f(|n_{0}|, \ldots, |n_{m}|)$( $|n|$ is the length of the binary expansion of the number

$n.$

.

)

there exists a polynomial such that.
This follows from the fact that for each termsuch that for eachofinthere exists a proof
with
Therefore we would have a polynomial$lh(P_{n})\leq f(|n|)$ . It is fairly easy to extend Theorem 2.1 to the caluculus. Thus we would have for apolynomial such that$t(\overline{a})$$\forall\overline{n}(|t(\overline{n})|\leq g(|\overline{n}|))$

$g$

$f$

$T$

$X_{n}$$P_{n}$

$n$

$T$

$f$

for any$n$there exists a cut free proof$P_{n}$

of$X_{n}$

in $T(dp(P_{n})<f(|n|))$ .

(2)

occurrs only positively in it for any . Put
iff there
We say that a sequent is positive if the atom
if is true under the truth
exists a cut free proof of in such that $dp(P)\leq k$ . Also we denoteassignment$X_{n}=$ if $n\leq k$ then true else
false.
$X_{n}$$P$

Then for any positivea contradiction.

$\Gamma$$k\models\Gamma$. Now (2)we$\vdash^{k}\Gamma$

$n$

$T$

$\Gamma$$\mathrm{h}\mathrm{a}\mathrm{v}\mathrm{e}\vdash^{k}\Gamma\Rightarrow k\models\Gamma$$\mathrm{r}\mathrm{u}\mathrm{n}\mathrm{s}\vdash^{j(|n|})x_{n}$$\Gamma$and hence $\forall n(n\leq f(|n|))$ . This isRemark. Add all polynomial growth rate functions to the language. Denote the set of true
sentences in. Let
denote the theory obtained fromby addingthis extended language by.
Then we see$\Sigma_{2}^{0}$$S_{2}^{0}(x)+Tr_{\Sigma_{2}}$$Tr_{\Sigma_{2}}$$S_{2}^{0}(X)$$Tr_{\Sigma_{2}}$$S_{2}^{0}(x)+Tr\Sigma_{2}\forall X(\mathrm{O})\wedge\forall x(X(X)\supset X(x+1))\supset\forall xX(x)$from the above proof. Observe thatfor a bounded formula
without $X$ .

$S_{2}^{0}(X)+Tr_{\Sigma_{2}}\vdash\Sigma_{\infty}^{b}-IND$

since each instance of$\Sigma_{\infty}^{b}-IND$

is in$Tr_{\Sigma_{2}}$$A\in\Sigma_{\infty}^{b}$

Equivalents for Bar Induction

3

In this section we give some equivalents for Bar Induction.
denotes a second order language containg 1) the language of the first order arithmetic, 2) set variables$X,$and 3) unary function variables $f,$
denotes the set of bounded formulae inandthe setof arithmetical (order) formulae possibly with second order parameters. We take the theory
as our base theory. The theory
has the following axiom schemata besides the axioms for first orderconstants:$L_{f}$$g,$$\mathrm{Y},$$\ldots$$\ldots.\Sigma_{0}^{0}$$L_{f}$$\Pi_{0}^{1}$$\Sigma_{0}^{0}-CA$$=\mathrm{f}\mathrm{i}\mathrm{r}\mathrm{S}\mathrm{t}$$\Sigma_{0^{-}}^{0}CA$

1. Graph Principle:(
pairing function),$\forall x\exists!yx(j(x, y))\supset\exists f\forall xx(j(x, f_{X}))$$j:\mathrm{a}$2. Comprehension Axiom for$\Sigma_{0}^{0}$-formulae and3. $IA:\forall X[X(\mathrm{O})\ \forall n\{X(n)\supset X(n+1)\}\supset\forall nX(n)]$In this section we use$\mathrm{s}\mathrm{i}\mathrm{g}\mathrm{n}\mathrm{s}\supset \mathrm{a}\mathrm{n}\mathrm{d}arrow \mathrm{i}\mathrm{n}\mathrm{t}\mathrm{e}\mathrm{r}\mathrm{c}\mathrm{h}\mathrm{a}\mathrm{n}\mathrm{g}\mathrm{e}\mathrm{a}\mathrm{b}\mathrm{l}\mathrm{y}$to denote the propositional connective ’implication’.

Definition 3.1
1. $BI$ denotes the axiom schema:
Hypl&Hyp2&Hyp3 $\supset Q<>$ for a
and an arbitrary formula
where$P\in\Sigma_{0}^{0}$$Q$( $<>$ is the empty sequence),

Hypl : $\forall f\exists xP(\overline{f}x)(\overline{f}x=<f0, \ldots, f(x-1)>)$

Hyp2 : $\forall c\in Seq(Pc\supset QC)$
(Seq denotes the set of g\"odel numbers of finite sequences of natural numbers).

Hyp3 : $\forall c\in Seq[\forall XQ(C*<x>)\supset Qc]$

2. For a binary relation$\prec,$$Wf(\prec)\Leftrightarrow_{d}f\forall f\exists x(f(X+1)\neq fx)$

101
3.

$Prg[\prec, Q]\Leftrightarrow dJ\forall x(\forall y\prec xQy\supset QX)$

4.

$I(\prec, Q)\Leftrightarrow_{d}JPrg[\prec, Q]\supset\forall xQx$

5. $TI$ denotes the axiom schema $Wf(\prec)\supset I(\prec, Q)$
and an arbitrary .
$Q$$\mathrm{f}\mathrm{o}\mathrm{r}\prec\in\Sigma_{0}^{0}$

6. $TI’$ denotes the axiom schemaand an arbitrary .
for
7.

$\forall XI(\prec, x)\supset I(\prec, Q)$$Q$$\prec\in\Sigma_{0}^{0}$$Ng\Leftrightarrow_{df}\forall f\forall X\exists c\in Seq(lh(C)=x\ f\in c)\Leftrightarrow dj\forall f\forall X\overline{\lrcorner}c\in Seq(c=\overline{f}x)$

8. For a formula$c=\overline{F}x\Leftrightarrow df$$F(x, y)_{\rangle}Fnc(F)\Leftrightarrow df\forall x\exists!yF(x, y)$lh(c)=x&\forall i $<xF(i.C(i))$ with the

9. $NG$ denotes the axiom schema
for an arbitrary .

and$i\mathrm{t}\mathrm{h}$component $c(i)$ of the sequence .
$c$$Fnc(F)\supset\forall x\exists c(c=\overline{F}x)$

$F$

10.

$\forall E(\Pi_{0}^{1})$for andenotes the axiom schema $\forall XA(X)\supset A(\{x\}F(x))$
and an arbitrary .
$F$$A\in\Pi_{0}^{1}$

Theorem 3.1 (cf. [14]) Over$\Sigma_{0^{-}}^{0}C\mathrm{A}$, the following axiom schemata are mutually equivalent:$Ng+BI,$ $Ng+TI,$ $TI’$ and$\forall E(\Pi^{1})0$

The theorem is seen from a series of the following propositions. Except the direction $Ng+BIarrow\forall E(\Pi_{0}^{1})$these are due to Howard and Kreisel [14]. Also we learned a weaker result $\Pi_{1}^{0}-cA+BIarrow\forall E(\Pi_{0}^{1})$ from [4],p.52.
Remark. We have also a second order parameter-free version of the theorem.

Proposition 3.1

1. $Ng+BI\vdash TI$ (cf. [14], Theorem

2. $TI\vdash BI$ (cf. [14], Theorem
3.

$TI’\vdash\tau x$

4.

$\forall E(\Pi_{0}^{1})\vdash BI$

5. $TI’\vdash Ng$ and$\mathit{5}A$))$\mathit{5}C$$\forall E(\Pi_{0}^{1})\vdash Ng$

6. $Ng+BI\vdash\Pi_{\infty}^{\perp}-IA$
7. $Ng+BI\vdash NG$
Proof. 3. It suffices to show, in$\Sigma_{0}^{0}-CA,$$Wf(\prec)\vdash\forall XI(\prec, x)$$\forall m(m\not\in X\supset\exists n\prec m(n\not\in X))\supset\exists$for$\mathrm{a}\prec\in\Sigma_{0}^{0}$. This follows fromf\forall m(m\not\in X\supset fm\prec m&m\not\in X)

4. As in 3, we have
Hypl&Hyp2&Hyp3\supset X $<>$
for a

$P\in\Sigma_{0}^{0}$in$\Sigma_{0}^{0}-CA$. Taking this formula as $A(X)$ in$\forall E(\Pi_{0}^{1})$we get any instanceHypl&Hyp2&Hyp3\supset Q $<>$of BI.
.
5. This follows from $TI’,$
6. A(O)&\forall n(A(n) $\supset A(n+1)$ ) we have to show $A(a)$ . Put $Pc\equiv a\leq lh(c)$ and $Qc\equiv A(a-lh(C))$ . By $Ng$ wehave Hypl. By $BI$ we conclude $Q<>$ , i.e., $A(a)$ .
7. This follows from 6.
$\forall E(\Pi_{0}^{1})\vdash\Pi_{\infty}^{1}-IA$$\square$$i\leq n$ occurs
is said to be in $\vec{f}normal$ form if each function variable
A formula.
in the formula
only of the form $f_{i}(y)=z$ for some variables
withis transformed into its $f^{-}normal$ form
In a canonical way, each quantifier free formula.
new variables and a quantifier free
Let $R(f)$ be a quantifier free formula and $F\equiv\{x, y\}F(x, y)$ be a binary formula (abstract). Also letbydenote the normal form of $R(f)$ . Then $R(F)$ denotes the result of replacing each $f(x)=y$ in$F(x, y)$ .
$A(f\vec{)}(\tilde{f}=f_{0}, \ldots , f_{n})$$f_{i},$

$y,$

$z$

$R(f\vec{)}$$\vec{x}$$A(f\vec{)}$$\exists\vec{x}R_{0}(\vec{x},$$f\vec{)}$$R_{0}$$\exists\vec{x}R_{0}(\tilde{x}, f)$$f$$\exists\tilde{x}R_{0}(\vec{x}, f)$

102
1. For each quantifier free andProposition 3.2$(a)$every free variable occurring in.
except$P$

normal form $R(x, f)$ there exists a$f$is either a new number variable$c$$P\in\Sigma_{0}^{0}$such that:or a variable occurring in $R(x, f)$$x,$ $f$$(b)$

for any binary formula$F$,$NG\vdash Fnc(F)arrow$with$F\in C\Leftrightarrow djc=\overline{F}(lh(c))$

2. For a quantifier free and$f$[$\exists xR(x$, F)\leftrightarrow \exists c(F\in c&Pc)].

normal form $R(x, f)$ , and a binary formula$F$,$Ng+BI\vdash Fnc(F)\ \forall f\exists xR(X, f)arrow\exists xR(x, F)$

3. For a quantifier free $R(x, f)$ and a binary formula$F_{f}$$Ng+BI\vdash Fnc(F)\ \forall f\exists xR(X, f)arrow\exists xR(x, F)$

4. For a fomula $A(x, y, X)$ let

denote the binary formula:$F$$F\equiv F(X)=_{df}\{x, y\}(y\simeq\mu y.\neg A(x, y, x))$[\exists y\neg A&y $= \min\{y:\neg A\}$ ]with
Then for any formula ,$y\simeq\mu y.\neg A\Leftrightarrow_{dj}$${ }$[\forall yA&y $=0$]$V$$Ng+BI$$Ng+BI$$\vdash$$Fnc(F(V))$ and$\vdash$$\forall x\exists y\neg A(x, y, V)arrow\forall x\forall y[F(V)(X, y)arrow\neg A(x, y, V)]$

that is,$Ng+BI$$\exists xA(x, F(V)(x),$ $V)arrow\exists x\forall yA(x, y, V)$$\vdash$Proof.

1. Letdenote a formula obtained from by replacing each $f(y)=z[f(y)\neq z]$ by c(y)=z&y $<lh(c)$[c(y)\neq z&y $<lh(c)$ ], resp. Then put $Pc\Leftrightarrow dj\exists x<lh(c)P0c$ . We need $NG$ to show that
Fnc(F)&\exists xR(x, F)-\succ \exists c(F\in c&Pc).
$R$$P_{0}c$

2. Assume Fnc(F)&\forall f\exists xR(x, ). Let
Put
$f$

$P$

$Qc\Leftrightarrow dj$

denote the formula formed in 1. Then we have Hypl for this$P$.

F\in c->\exists d(F\in c*d&P(c*d))

By $F$ ( $lh(c)$ , x)&Q(c* $<x>$ ) $arrow Qc$ , we have Hyp2&Hyp3. Thus by $BIQ<>$ and henced&Pd). The assertion follows from 1.

$\exists d(F\in$3. This follows from Proposition 3.2.2 and the definition of $\exists xR(x, F)$ .
4. This follows from Proposition 3.1.6.
$\square$Lemma 3.1 $Ng+BI\vdash\forall E(\Pi_{0}^{1})$Proof For an$A\in\Pi_{0}^{1}$and an arbitrary

Stepl First transform

$A$

$V$

we have to show $\forall XA(X)arrow A(V)$ .

into a prenex normal form whose leading quantifier is . For example assume
with a quantifier free
. We need only logical axioms to obtain this$\exists$$A(X)rightarrow\exists x0\forall y0\exists x1\forall y1A0(X)$$A_{0}$

equivalence. Hence for any formula we haveis in prenex normal form, e.g., of the form
$V$

$A$

Step2 Second transform$A_{0}(x0, f_{0}(x\mathrm{o}),$$A(V)rightarrow\exists x_{0}\forall y\mathrm{o}\exists x_{1}\forall y1A0(V)$$\exists x_{0}\forall y0\exists x_{1}\forall y1A_{0(}X$$x_{1},$$A$. Thus we can assume that).

into its Herbrand normal form. Pick new function variables. We have logically$f_{1}(X_{0}, X_{1}))$$F_{0}$$F_{1}$$=_{df}$$=_{dj}$$\{x_{0}, y0\}(y0\simeq\mu y_{0^{\neg\exists}}.x_{1}\forall y_{1}A0)$$\{x0, x_{1}, y1\}(y_{1}\simeq\mu y_{1}.\exists y0(F\mathrm{o}(x_{0}, y0)\ \neg A_{0}))$and putPut$f_{0},$ $f_{1}$$\exists x_{0}\forall y0\exists x_{1}\forall y_{1}A_{0}arrow\forall f_{0}\forall f_{1}\exists x0\exists X_{1}A_{H}$.

$A_{H}\equiv$

103
By Proposition 3.2.4, $Ng+BI$ proves that
$Fnc(F0(V))\ FnC(F_{1}(V))$

and$\exists x_{01}\exists xA0(X0, F_{0}(V)(x\mathrm{o}),$Hence, in $Ng+BI,$$X_{1},$$F_{1}(V)(X0, X_{1}),$ $V)arrow\exists x0\forall y0\exists X1\forall y1A0(V)$and$\forall XA(x)arrow\forall X\forall f_{0}\forall f1\exists X0\exists x1AH$$\forall X\forall f_{0}\forall f1\exists x0\exists X_{1}A_{H}arrow\exists x0\exists x_{1}A0(x_{0}, F0(V)(X0),$$\exists x_{0}\forall y_{0}\exists x1\forall y_{1}A0(V)\equiv A(V)$$X_{1},$$F_{1}(V)(x0, X_{1}),$ $V)$

. Thus Proposition 3.2.3 yields.
$\square$Now Theorem 3.1 has been proved from these propotions and lemma.
Next we show that Bar Induction is equivalent to the reflection schema for logic.
We change our languageto:From1) remove the function variables, 2) add the -ary predicate
variablesand 3) restrict function constants to. The resulting language is denoted. Thus closed terms inare numerals. We understand that predicate constants corresponding to primitive
recursive relations are included in .
Let
denote a Tait’s calculus for this second order language. A second order terms is just a predicate
variableand hence in
the inference rule
for the second order existential quantifier runs:$\omega$$L_{2}$$L_{f}$$L_{f}$$n$$X_{i}^{n}(i\in\omega)$$0,$$L_{2}$$S(s:\mathrm{s}\mathrm{u}\mathrm{C}\mathrm{c}\mathrm{e}\mathrm{S}\mathrm{s}\mathrm{o}\mathrm{r})$$L_{2}$$L_{2}$$LK_{2}$$L_{2}$$X^{n}$$LK_{2}$$(\exists_{2})$$\frac{\Gamma,F(X)}{\Gamma,\exists \mathrm{Y}F(\mathrm{Y})}$

Also let $RFN$ denote the reflection schema for the calculus$LK_{2}$.

Proposition 3.3$\Sigma_{0}^{0}-CA\vdash RFNrightarrow\Pi_{\infty}^{1}-IA$

Proof.
For each we have $LK_{2}\vdash A(O)\wedge\forall x(A(x)\supset A(SX))\supset A(n)$ .
By cut elimination and the partial truth definition.
$(arrow)$$n$$(arrow)$$\square$

Let $ACA_{0}$ denote the second order arithmetic Arithmetical Comprehension Axiom with Restricted
tion. Since $ACA_{0}$ is finitely axiomatizable, we get the

Corollary 3.1 (cf.

$[\mathit{2}\mathit{2}f$$\mathrm{i}\mathrm{n}\mathrm{d}\mathrm{u}\mathrm{c}^{2}-$, Lemma 2.7)
$ACA_{0}\vdash RFN_{ACA_{0}}rightarrow \mathrm{I}\mathrm{I}_{\infty}^{1}-IA$

Let$X_{0}\subseteq\omega\cross\omega$

be a binary relation.

1. The language of$LK_{\omega}(x_{0})$denotes the$\omega$logic with the relation$X_{0}$:

is obtained fromby adding the binary predicate constantand removing
the first order free variables. Any sequents inhave no first order free variable.
$LK_{\omega}(X_{0})$$L_{2}$$X_{0}$$LK_{\omega}(X\mathrm{o})$2. Axioms (sequent) inconstants and logical ones.
$=\mathrm{i}\mathrm{n}\mathrm{i}\mathrm{t}\mathrm{i}\mathrm{a}\mathrm{l}$$\Gamma,$

3. Inference rules in$LK_{\omega}(x_{0)}$$X_{0}(n, m)$

are diagrams for the relation

if $X_{0}(n, m)$ , andare those offor first order universal quantifier by the$LK_{\omega}(X_{0})$$\Gamma,$$\neg X\mathrm{o}(n, m)$$X_{0}$

if $\neg X_{0}(n, m)$

except the following changes. First replacing the usual rule
rule:

$LK_{2}$$\omega$$\frac{\{\Gamma,A(n).n\in\omega\}}{\Gamma,\forall xA(x)}.(\omega)$

Second restrict the rule$(\exists)$

besides the usual axioms for thefor the first order existential quantifier to:$\frac{\Gamma,A(n)}{\mathrm{r},\exists xA(X)}$104
By a preproof we mean an -branching labelled tree of sequents and some data. Data should include namesof axioms or inference rules and finite cut degrees. A preproof have to be locally correct with respect to thedata. An -proof is a well founded preproof.
$\omega-RFN$ denotes the schema saying that if a sequent, then the sequent is
has an -proof in$\omega$$\omega$$\Gamma$$LK_{\omega}(X_{0})$$\omega$$\Gamma$true.
Theorem 3.2$\Sigma_{0}^{0}-cA_{0}\vdash\omega-RFNrightarrow Ng+TI$

and hence $Ng$ . Assume $Wf(\prec)$ . We have to show $Prg[\prec, A]arrow\forall xA(x)$ . It
Proof.
We have. Wlog we can assume that no
suffices to show that there exists an -proof of the sequent $\neg Prg[\prec, A],$. Thus $n\prec m$ has an -proof when
) occurrs insecond order free variable (except the ’constant’$n\prec m$ is true and similarly for the case $n\neq m$ . Using this fact we can construct a preproof of the sequent$\neg Prg[\prec)A],\forall xA(x)$ which must be well founded bt our assumption $Wf(\prec)$ .
Again by cut elimination and the partial truth definition. Here cuts are eliminated through Mints’ continuous cut elimination procedure in Mints [18]. To ensure that the resulting cut free preproof is well founded
we need $\Pi_{1}^{0}-CA$ , i.e., Arithmetical Comprehension Axiom (cf. [18] or [11]). But $\Pi_{1}^{0}-CA$ follows.
$\Pi_{\infty}^{1}-IA$$(arrow)$$\forall xA(x)$$\omega$$X_{0}$$\prec\in\Sigma_{0}^{0}$$\omega$$(arrow)$$\mathrm{f}\mathrm{r}\mathrm{o}\mathrm{m}\square$$Ng+^{\tau}Irightarrow\forall E(\Pi_{0}^{1})$$\omega-RFN$ is also equivalent to the so calledLet

be a theory in$T$$L_{2}$$A(X)arrow\exists$

When

$T$

$\omega$-model reflection schema over $ACA_{0}$ .

. By $\omega-model-R\tau N\tau$ we mean the following schema for an arbitrary formula $A(X)$ :countable $M=(M_{n} :consists solely of axioms for constants in$L_{s}$

n\in\omega)(M_{0}=X\ M|=T\ M\models A[X])$, we denote simply$\omega-model-RFN$ .

Proposition 3.4 (Henkin-Orey’s -completeness theorem) In $ACA_{0}$ ,in
there exists an -proof of$\omega$$A(X\mathrm{o})$$\omega$

iff
for any countable$\omega$$LK_{\omega}(X\mathrm{o})$model $M\ni X_{0}M\models A[X\mathrm{o}]$Corollary 3.2 $ACA_{0}\vdash\omega-RFNrightarrow\omega-model-RFN$ and hence(cf. [22].)$ACA_{0}\vdash\omega-model-RFN_{ACA0}rightarrow TI’$

4

Direct computations in an equatinal calculus PRE

Let PRE denote the theory $PRA$ minus induction axiom. The axioms of PRE are defining equations forprimitive recursive functions: (zero) denotes an invividual constant ans the successor function. Function
constants and their defining equations are generated as follows.
$S$

$0$

1. (projection) $I_{i}^{n}(x_{1\cdot\cdot n},., x)=x_{i}(1\leq i\leq n, n>\mathit{0})$2. (composition)
where denotes a sequence,of variables.

$f(\overline{x})=h(g_{1}(\overline{x}), \ldots, g_{m}(\overline{X}))$$\overline{x}$$x_{1},$$\ldots,$

3. (primitive recursion 1)( is a natural number).

$f(\mathrm{O})=k,$$x_{n}$$f(Sy)=h(y, f(y))$$k$

4. (primitive recursion 2)$f(\overline{x}, O)=g(\overline{x}),$$f(\overline{X}, s_{y})=h(\overline{x}, y, f(\overline{x}, y))$In what follows our concern is restricted to Horn clauses $E\supset e$ with an equation and a finite set $E$ ofequations. Therefore it is better to consider PRE as an equational theory with an extra axiom $E$ . By
we mean the equation is derivable from the set $E$ in PRE.
For a function constant $f,$ $Cl(f)$ denotes the finite set of function constants which are used to define theconstant (and the successor ). Specifically,$e$$E\vdash e$

$e$

$f$

$S$

1. (projection) $Cl(I_{i}^{n})=\{I_{i}^{n}\}\cup\{S\}$2. (composition) $Cl(f)=Cl(h)\cup\cup\{Cl(gi). 1\leq i\leq m\}\cup\{f\}$3. (primitive recursion 1) $Cl(f)=Cl(h)\cup\{f\}$4. (primitive recursion 2) $Cl(f)=Cl(g)\cup Cl(h)\cup\{f\}$105
For a term
{ $Cl(f)$ : occurs in }.
$C/(t=s)=Cl(t)\cup
cl(S)$ .
For an equation $i=s,$of equabions, $cl(E)=\cup \mathrm{f}^{cl}(e):e\in E\}$ .
For a set
$t,$

$f$

$Cl(t_{)}^{\backslash }=1\lrcorner$

$t$

$E$

Let denote therules $larrow r$ which are obtained from one of the defining equations $l=r$ by replacing. Viewing the set
by thethe equality sign
as a term-rewriting system, $sarrow_{R}t$ or simply $sarrow t$$R$bydenotes the reiation the term rewrites to the termin the sense of [7].
denotes the reflexivethe smallest congruent relation containg the relation .
transitive closure
The following is a folklore.
$R$$\mathrm{s}\mathrm{e}\star_{\mathrm{o}^{\mathrm{f}}}$

$=$

$R$

$\mathrm{a}\mathrm{r}\mathrm{r}\mathrm{o}\mathrm{W}arrow$

$i$

’

”

$t$

$s$

$\mathrm{A}\mathrm{l}\mathrm{s}\mathrm{o}arrow*$$\mathrm{o}\mathrm{f}arrow \mathrm{a}\mathrm{n}\mathrm{d}rightarrow*$

Proposition 4.1$\mathit{2}$

$i$

$R$

. $arrow is$ Church-Rosser, $i.e.,$$rightarrow\subseteqarrow 0arrow***$. $arrow is$ terminating.

3. $sarrow t\Rightarrow Cl(s)\subseteq Cl(t)$Therefore we have

Proposition 4.2 For an equation$e,$$\vdash e$

is decidable by $com$ puting the normal forms of the both sides of .
$e$

, then there
Proposition 4.3 For an equation$e_{i}ever\tau/\ldots hnction$ constant occurring in
is in $Cl(e)$ .
of$e,$$if\vdash e$$exi_{S}t\mathit{8}$a direct (in the sense of [21], p.343) computation$D$$\mathcal{D}$This directness
not hold lf weCounterexamples (H. Friedrnan [9])$\Gamma\{0\mathrm{a}\mathrm{e}$$\mathrm{r}\mathrm{e}\mathrm{p}\mathrm{l}\mathrm{a}\mathrm{C}\mathrm{e}\vdash e$by$E\vdash e$.

1. $Sx=Sy\vdash x=y$ : Apply the predecessor function $pd$ .
2. $\mathit{0}=Sx\vdash y=z$ : Apply the descriminator

Our theorem below$\mathrm{s}_{u}^{\neg}.\mathrm{y}\mathrm{s}$$\delta,$$\delta(y, z, \mathrm{O})=y,$$\delta(y, z, S_{X})=z$.

that these are only exceptions.

Definition 4.1 PRE’ is obtained from PRE by adding the following two rules for an arbitrary equation :$e$$\frac{St_{1}=St_{2}}{t_{1}=t_{2}}(S)$$\frac{\mathit{0}=St}{e}(\delta)\backslash$, then there exists a direct computation
Theorem 4.1 For a finite set $E$ of equations and an equation , if
$Pf?E’,\cdot\rho very$$Cl(E)\cup
Cl(e)$ .
occurringinconstantinisinfunctionof from
$e$

$D$

$E$

$e$

$E\vdash e$$D$

Corollary 4.1 For an open formula $A_{f}if\vdash A$ , then there exists a direct derivationof in PRE’ andhen ce a weakly direct derevalion $D$ of in PRE; every function constant occurring in $D’$ [inin $Cl(A)$$I^{cl}(A)\cup Cl(pd)\cup Cl(\delta)f$, resp.
$A$$\mathcal{D}’$$A$$Dfi\mathit{8}$and consider each conjunct separately.
Proof of Corollary. Write inis equivalent
to $E’arrow E$ for some finite sets $E’$ andof equations ( $E’arrow E$ denotes a sequent in Gentzen’s sense). Then
use the theorem and the fact: $E’\vdash E\Rightarrow E’\vdash e$ for sorne $e\in E$ .
$A$

$C$

$\mathrm{C}\mathrm{N}\mathrm{F}\wedge\{C:C\in\Gamma\}$

$C$

$E$

$\square$

We don’t know an answer to the problem raised by H. Friedman [9]Problem.

1.

$\mathrm{I}\mathrm{s}\vdash A$

2. Is

decidable for an open

$e\vdash \mathrm{d}\mathrm{e}\mathrm{c}\mathrm{i}\mathrm{d}\mathrm{a}\mathrm{b}\mathrm{l}\mathrm{e}$$A$?

for an equation ?
$e$

But we conjecture the following.
Conjecture. Let and be normal terms with respect. Thenfor some term andwith $m>n$ or vice versa.
$t_{1}$$t_{1}=t_{2}\vdash\Leftrightarrow t_{1}\equiv S^{m}t_{0}$$t_{2}$$\mathrm{t}\mathrm{o}arrow R$$t_{0}$$t_{2}\equiv S^{n}0$This means that the theory PRE can discriminate between ternts only when one is and the other is of theform St. Unless the equation $t_{1}=t_{2}$ is of the form $St=u$ where the term occurs in and contains avariable, the conjecture is easily seen to hold. Also if is a variable , then, by H. Friedman [9], we have$St(x)=x\dagger f$ . That’s all what we know about the conjecture.
The rest of the section is devoted to a proof of the Theorem 4.1. Fix a finite setof equations.
denotes ambiguously the equation $t_{1}=t_{2}$ or $t_{2}=t_{1}$ .
$0$

$t$

$u$

$u$

$u$

$x$

$E$

$t_{1}=t_{2}$106
1. $d(E)$ denotes the smallest set of equations such that
1) $E\subseteq d(E)$ and 2) $d(E)$ is closed under the rules $(S)$ , (sub) and (red):Definition 4.2$\frac{e[t_{1}/x]t1=t_{2}}{e[t_{2}/x]}$

2.

,.

(sub)

$\frac{t=u}{t=u}$

(red)

where

$tarrow_{R}t’$and a finite set $\{u_{i}=v_{i} : i<n\}\subseteq d(E)(n\geq \mathit{0})$ of equations such that(simultaneous substitution) and $t_{0}[v_{0}, \ldots , v_{n-1}/x_{0}, \ldots, X_{n-1}]arrow Rt’=$)denotes the reflexive closure$tarrow_{E}t’\Leftrightarrow_{df}$there exists a term$t_{0}$$t\equiv t_{0}[u_{0,\ldots n-1}, u/x_{0}, \ldots , x_{n-1}]$($arrow R=$$\mathrm{o}\mathrm{f}arrow_{R}.$3. $arrow E*[^{*}-E]$ denotes the reflexive-transitive [-symmetric] closure$\mathrm{o}\mathrm{f}arrow E$, resp.

Clearly $e\in d(E)\Rightarrow Cl(e)\subseteq Cl(E)$ and hence we have the

1. $tarrow_{E}t’\Rightarrow Cl(t’)\subseteq Cl(t)\cup Cl(E)$Proposition 4.4

2.

$E\vdash t_{1}=t_{2}\Rightarrow t_{1}rightarrow_{E}t_{2}*$Lemma 4.1 Assume that $\mathit{0}=St\not\in d(E)$ for any term .
$t$$Thenarrow_{E}$is Curch-Rosser, $i.e.,$$rightarrow E\subseteqarrow E**0arrow E*$.

Proof of Theorem 4.1. If $0=St\not\in d(E)$ for any , then we get the theorem by the Lemma 4.1 and the
Proposition 4.4. Assume $0=St\in d(E)$ for some term . Then there exists a direct computation of
from .
we get a desired computation of
from in PRE’. By adjoining the rule
$t$

$D$

$t$

$\mathit{0}=St\square$$E$

In what follows we assume that $\mathit{0}=St\not\in d(E)$ for any term

1.

Definition 4.3$tarrow I^{S}$$E$$t_{1}=t_{2}$$(\delta)$$t$.

is defined inductively as follws:$(a)tarrow_{I}t$where, for sequences$(b)\overline{t}arrow I\overline{s}\Rightarrow f(\overline{t})arrow If(\overline{s})$$\overline{t}\equiv t_{1},$$\ldots,$$t_{n},\overline{s}\equiv s_{1}\ldots$,$s_{n}$of terms,$\overline{t}arrow I\overline{s}\Leftrightarrow dj$

for any .
$i$$t_{i}arrow Is_{i}$$(c)$(projection)$(d)$(composition)$t_{i}arrow_{i^{S}}\Rightarrow I_{i}^{n}(t_{1}, \ldots , t_{n})arrow I^{S}$$\overline{t}arrow I^{\overline{S}}\Rightarrow f(t\gammaarrow_{I}h(g1(\overline{S}), \ldots, g_{m}(\overline{S}))$(primitive recursion 1) $f(O)arrow Ik;tarrow Iu\Rightarrow f(St)arrow_{I}h(u, f(u))$ if $f(O)=k$ .
$(f)$ (primitive recursition 2)
;

$(e)$

$\overline{t}arrow I^{\overline{S}}\Rightarrow f(\overline{t}, O)arrow_{Ig}(\overline{\mathit{8}})$$\overline{t}arrow I\overline{s}\ uarrow_{I}v\Rightarrow f(\overline{t}, Su)arrow Ih(\overline{s}, v, f(\overline{s})v))$

2.

$tarrow_{EI}s\Leftrightarrow dj$$s$there exist a term$t_{0}$

and a sequence $\{u_{i}=v_{i} : i<n\}\subseteq d(E)$ such that $t\equiv t_{0}[u0, \ldots , u_{n-1}/x_{0}, \ldots, x_{n-}1]-$.

As usual we have$1$.

$arrow R^{=arrow}I**$$2$.

$arrow E^{=arrow}**EI$

3. $-I$ is strongly confluent, i.e., satisfies the diamond property:$\forall t,$$s,$$u\exists v(tarrow_{I}s\ tarrow_{I}u\Rightarrow sarrow_{I}v\ uarrow_{I}v)$

Thus it suffices to show the following lemma.
Lemma $4.2arrow EI$ is strongly confiuent.

Define$t_{1}rightarrow_{CE}t_{2}\Leftrightarrow$

there exist a ter.m$t0$

and a sequence $\{u_{i}=v_{i} : i<n\}\subseteq d(E)$ such thatand $t_{2}\equiv t_{0}[v0, \ldots, v_{n-1}/x_{0)}\ldots, x_{n-1}]$ .

$t_{1}\equiv t_{0}[u_{0}, \ldots , u_{n-1}/x_{0}, \ldots, x_{n-1}]$

Since $d(E)$ is closed under the rule, $(sub)rightarrow CE$ is transitive. Therefore it suffices to show:
Claim 4.1 If we have $M_{1}arrow_{I}Mrightarrow_{CE}Narrow IN_{1}$ , then there exist terms$Larrow_{I}M_{2}rightarrow_{CE}N_{1}$.

$N_{2},$ $M_{2},$ $L$

such that $M_{1}rightarrow CEN_{2}arrow I$

107
Proof of Claim 4.1. We prove this by induction on $m+n$ , where $m[n]$ denotes the depth of a derivation of$M-IM_{1}[Narrow IN_{1}]$ , resp.

Case $0M=N\in d(E)$ : Then $M_{1}=N_{1}\in d(E)$ . Take

$N_{2}\equiv L\equiv M_{2}\equiv N_{1}$.

Case 1 $M_{1}\equiv M$ : Take $N_{2}\equiv N,$ $L\equiv M_{2}\equiv N_{1}$ .

Case 2
2.1$M\equiv f(t\gammaarrow_{I}f(\overline{u})\equiv M_{1}$$N\equiv f(\overline{v})arrow If(\overline{w})\equiv N_{1}$with. By IH

with$N\equiv I_{i}^{n}(\overline{v})arrow Iw_{i}\equiv N_{1}$$\overline{t}arrow I\overline{u}$$\overline{v}arrow I\overline{w}$$u_{i}arrow_{I}t_{i}rightarrow_{CE}v_{i}arrow Iw_{i}$

2.2

with

:

: For each$i$

we have$u_{i}rightarrow CEv_{i}’arrow I^{S}iarrow_{I}t_{i}’rightarrow_{CE}w_{i}$$v_{i}arrow Iw_{i}$for some$N\equiv f(\tilde{v}, O)arrow Ig(\tilde{w})\equiv N_{1}$with$s_{i},$$t’i$.

: As in 2.1,

$M_{1}\equiv I_{i}^{n}(\overline{v})rightarrow cEI_{i}^{n}(u1, \ldots, u_{i}-1, v_{i}, ui+1, \ldots, un)Jarrow IS_{i}arrow_{I}t_{i}’rightarrow CEw_{i}$2.3$v_{i}’,$$\tilde{v}arrow\tilde{w}(\tilde{v}\equiv v_{1}, \ldots, v_{r\iota-}1)$: By IH pickby$M_{1}\equiv f(\tilde{u}, u_{n})rightarrow CEf(\tilde{v}’, 0)arrow Ig(\tilde{s})arrow Ig(t’)\simrightarrow CEg(\tilde{w})\equiv N_{1}$$v_{i}’,$

for some$s_{i},$$t_{i}’$$v_{i}’,$$S_{i},$$t_{i}’$.

for $i\neq n$ as in 2.1. Then$\mathit{0}=t_{n}\in d(E)\ t_{n}arrow Iu_{n}\Rightarrow \mathit{0}=u_{n}\in$$d(E)$

2.4$N\equiv f(\tilde{v},$ $s_{v_{n})arrow_{I}}h(\tilde{w}, w_{n}, f(\tilde{w}, w_{n}))\equiv N_{1}$$v_{n}arrow_{I}w_{n}$2.41: Pick$t_{r\iota}=^{s_{v_{n}}}\in d(E)$$\tilde{v}’.t^{\sim_{J}},\tilde{s}$so thatwith$\tilde{v}arrow I\tilde{w}$and$\tilde{u}rightarrow CE\tilde{v}arrow I\tilde{s}arrow It’\simrightarrow CE\tilde{w}$.

: Then $u_{n}=Sw_{n}\in d(E)$ .

$M_{1}\equiv f(\tilde{u}, u_{n})rightarrow cEf(\tilde{v}’, s_{w_{n}})arrow Ih(\tilde{S}, w_{n}, f(\tilde{S}, w_{n}))arrow I$$h(t’, w, fn(t^{J}, w\sim\sim n))rightarrow CEh(\tilde{w},$ $w_{n},$ $f(\tilde{w}, w, fn(\tilde{w}, w_{n}))\equiv N_{1}$$tarrow Iu$ by a shoter or equal lengthwith $trightarrow CEv_{n}$ for some . Also, for some
2.42 Otherwise:$t_{n}\equiv
Starrow ISu\equiv u_{n}$ . By IH pick $v’,$so that $urightarrow CEv’arrow Isarrow It’rightarrow CEw_{n}$ . Thenderivation that$t_{n}\equiv St$

$t$

$u,$

$S,$

$t^{J}$$M_{1}\equiv f(\tilde{u}, u_{n})rightarrow cEf(\tilde{v}^{\prime,s)}v’arrow Ih(\tilde{s}, s, f(\tilde{S}, S))arrow_{I}h(t’’\sim,\sim_{J}t, f(\mathrm{f}, t’))rightarrow CEh(\tilde{w}, w_{n}, f(\tilde{w}, w_{n}))\equiv N_{1}$2.5 $N\equiv f(0)arrow Ik\equiv N_{1}$ : Similar to 2.3.
2.6 $N\equiv f(Sv)arrow Ih(w, f(w))$ with $varrow_{I}w$ : Similar to 2.4.
Case3

$M\equiv I_{i}^{n}(\overline{t})arrow_{I}u_{i}\equiv M_{1}$Case 4assumption,
. Use

with

with
for any$M\equiv f(\overline{t}, 0)arrow Ig(\overline{u})$$\overline{v}arrow_{I}\overline{w}$Case 5$v\not\equiv Sv’$$\mathrm{I}\mathrm{H}$$t_{i}arrow Iu_{i}$$N\equiv I_{i}^{n}(\overline{v})arrow_{I}w_{i}\equiv N_{1}$with$v_{i}arrow Iw_{i}$with $0rightarrow CEv$ , i.e., $\mathit{0}=v\in d(E)$ or. Therefore it must be the caseand$\overline{t}arrow I\overline{u}:N\equiv f(\overline{v}, v)$$v’$$v\equiv 0$$v\equiv 0$. By ourwith$N\equiv f(\overline{v}, O)arrow Ig(\overline{w})$.

and $tarrow Iu$ : As in the Case 4 we have
and $varrow_{I}w$ . Note that if $Strightarrow CESv$ , then $trightarrow CEv$ by the rule $(S)$ .

$M\equiv f(\overline{t}, St)arrow Ih(\overline{u})u,$ $f(\overline{u}, u))$$h(\overline{w}, w, f(\overline{w}, w))$

and

with

$\overline{w}arrow I\overline{w}$with$N\equiv f(\overline{v}, Sv)arrow I$$\overline{t}arrow I\overline{u}$Case 6 $M\equiv f(0)arrow ik$ : Similar to the Case 4.
Case 7 $M\equiv f(St)arrow Ih(u, f(u))$ with $tarrow Iu$ : Similar to the Case 5.
This completes a proof of the Claim 4.1.

5Intuitionistic fixed point theories

is conservative over Heyting Arithmetic $HA$
In [3] Buchholz shows that an intuitionistic fixed point theory
[3]
is
based
on a recursive realizability interpretation
with respect to almost negative formulae. The proof in. Having seen a preliminary version of [3] we can extend and strengthen this result.
of the theory
is interpreted
Our proof runs as follows. First an extension of an intuitionistic iterated fixed point theory
in the intuitionistic analysis $EL+AC-NF$ . This is done by imitating Aczel’s proof in [8] which shows. Then by N.
is interpretable in a second order arithmetic
that the classical fixed point theory
Goodman’s theorem [12] one can conclude our theorem. A proof of N. Goodman’s theorem is based on either
a combination of a realizability interpretation and a forcing or proof theoretic analysis in G. Mints [18]. It
based on one of thses methods is desirable.
seems that a direct analysis of$I\hat{D}_{1}^{i}$$I\hat{D}_{1}^{i}$$I\hat{D}_{n}^{i}$$\Sigma_{1}^{1}-AC$$I\hat{D}_{1}$$a$$I\hat{D}_{n}^{i}$

1. $EL$ denotes the intuitionistic elementary analysis defined in [Definition 5.1$EL$
are denoted byables in$\mathit{2}\mathit{5}f$$\alpha,$$\beta,$$\gamma,$$\ldots$

p.144. Function vari-108
2. The axiom schema AC–NF:$\forall n\exists\alpha A(n, \alpha)\supset\exists\beta\forall nA(n, (\beta)_{n})$with $(\beta)_{n}=\lambda m\beta(j(n, m))$ and a pairing function .
$j$3.

denotes the language of $EL$ . For a list of set parameters
language obtained from by adding .
$L$

$L$

4.

$\overline{X}=X_{0},$ $X_{1},$$L(\overline{X})$$\ldots,$

denotes the expanded$\overline{X}$denotes the extension of $EL[EL+AC-NF\mathit{1}$ by expanding the language, resp.
to
Each axiom schema in $EL[EL+Ac_{-}NFf$ is available forformulae in $EL(\overline{X})l^{EL+A}c-NF(\overline{X})f$ ,resp.
$EL(\overline{X})[EL+AC-NF(\overline{x})\mathit{1}$$L(\overline{X})$$L(\overline{X})$

Lemma 5.1 For eachand each listof set parameters there exists a formulasuch that for every formula inthere is an integerinsuch that$S_{n}(X_{0}, X1, \ldots, xn;\overline{x}, \alpha)$$\overline{X}$$n$$\Sigma_{1}^{0}(x0, x1, \ldots, xn;\overline{x}, \alpha)$$A$$\Sigma_{1}^{0}(x0, x1, \ldots, xn;\overline{x}, \alpha)$$e$$EL(\overline{X})\vdash Arightarrow\Sigma_{1}^{0}(e, x1, \ldots, x;n\overline{X}, \alpha)$

Proof. By formalizing the enumeration theorem. This is done in

Definition 5.2 Let
1.

3.

4.

set of all
by means$Pos(\mathcal{F};\overline{\mathrm{Y}})=_{dj}\mathrm{t}\mathrm{h}\mathrm{e}$formulae in

2.

be a list of set parameters and$\overline{\mathrm{Y}}$$F$$\mathrm{o}\mathrm{f}\wedge,$$L(\overline{\mathrm{Y}}, X)$$\forall m,$$\vee,$$POS(\overline{\mathrm{Y}})=POS(F_{\overline{\mathrm{Y}}} ; \overline{\mathrm{Y}})$and$Pos(\overline{\mathrm{Y}};\overline{\mathrm{Y}})=POS(A_{\overline{\mathrm{Y}}} ; \overline{\mathrm{Y}})$for$\mathrm{Y}_{i}\in\overline{\mathrm{Y}}$$\Phi$

a set of formulae in$L(\overline{\mathrm{Y}})$. Pick an$X\not\in L(\overline{\mathrm{Y}})$$\square$.

formulae which are built up from formulae $X(t)$ ( : a term) and(first order quantifications).
$t$

for a fixed number variable . $FV(\Phi)$ denotes the. Thus no function free variable occurs in.
FV(\Phi)\subseteq\{x\}\}$$x$$\Phi,$$PoS^{*}(\overline{\mathrm{Y}})=POS^{*}(\mathcal{F}\overline{\mathrm{Y}};\overline{\mathrm{Y}})$and. cf. Ch. 3, Sect. 6 and 7 in [25].

$\exists m$$POS^{*}(\mathcal{F};\overline{\mathrm{Y}})=_{dj}\{\Phi\in Pos(\mathcal{F};\overline{\mathrm{Y}}) :set of free variables occurring in$\mathcal{F}$$EL(\overline{X})$with the set$POS^{*}(\overline{\mathrm{Y}};\overline{\mathrm{Y}})=POS^{*}(A_{\overline{Y}} ; \overline{\mathrm{Y}})$$\mathcal{F}_{\overline{\mathrm{Y}}}$$\in POS^{*}(\mathcal{F};\overline{\mathrm{Y}})$of all formulae inwith the set$A_{\overline{\mathrm{Y}}}$$L(\overline{\mathrm{Y}})$.

of atomic formulae$\mathrm{Y}_{i}(t)$.

5. $POS=POS(\mathrm{o})$ .
is narrower than strictly positive formulae (with respect to $X$ ) because $A\supset X(t)\not\in$
but is wider than $POS$ in [3]. If we set $A\supset X(t)\in POS(\tau;\overline{\mathrm{Y}})$ , then one would need $IP$
(Independence of Premise) for proof of Lemma 5.3 below.
Remark.

$Pos(\mathcal{F};\overline{\mathrm{Y}})$$Pos(\mathcal{F};\overline{\mathrm{Y}})$$a$

Lemma 5.2 For each $\Phi\in POS$ there exist a list
frmulae in such that$\overline{\mathrm{Y}}$of set parameters, a$\Phi’\in Pos(\overline{\mathrm{Y}};\overline{\mathrm{Y}})$and a list$\overline{A}$

of

$L$

$EL(X)\vdash\Phirightarrow\Phi’[\overline{A}/\overline{\mathrm{Y}}]$

where [$\overline{A}/\overline{\mathrm{Y}}f$denotes the $simultaneou\mathit{8}$ substitution.

A formula in
if it is of the form
occurs.

$L(\overline{\mathrm{Y}})$is said to be an
fomula (with an open formula$n-\Sigma_{1}^{1}(\overline{\mathrm{Y}})$$\exists\alpha\forall nR(\alpha, n,\overline{\mathrm{Y}})$

Lemma 5.3 For eachand each $A(x)$ in$\Phi\in Pos(\overline{\mathrm{Y}};\overline{\mathrm{Y}})$

formula in normal form with set parameters )inin which no function variable except$\overline{\mathrm{Y}}$$\Sigma_{1}^{1}$$R$$L(\overline{\mathrm{Y}})$$n-\Sigma_{1}^{1}(\overline{\mathrm{Y}})$$\alpha$there exists a $C$ in$n-\Sigma_{1}^{1}(\overline{\mathrm{Y}})$such that$EL+AC-NF(\overline{\mathrm{Y}})\vdash\Phi[A/X]rightarrow C$

Proof by induction on the length of$\Phi$

using the facts:$EL(\overline{\mathrm{Y}})\vdash A\vee\exists\alpha Brightarrow\exists\alpha(AB)$$EL(\overline{\mathrm{Y}})\vdash\forall zA\vee\forall yBrightarrow\exists x\forall z\forall y[(X=0\wedge A)(x\neq 0\wedge B)]$$\square$Lemma 5.4 For eachinsuch that$\Phi\in Pos^{*}(\overline{\mathrm{Y}};\overline{\mathrm{Y}})$

there exists a formula$P^{\Phi}(\overline{\mathrm{Y}}, x)$$n-\Sigma_{1}^{1}(\overline{\mathrm{Y}})$$EL+AC-NF(\overline{\mathrm{Y}})\vdash\forall x\{P^{\Phi}(\overline{\mathrm{Y}}, x)rightarrow\Phi[\{x\}P^{\Phi}(\overline{\mathrm{Y}}, x)/X]\}$

109
Proof by Lemmata 5.1 and 5.3. Put
such that $\Phi[\{x\}B/x]rightarrow C$ . Pick an so thatThen
is a desired one.

$B(u, x;\overline{\mathrm{Y}})\equiv\exists\alpha\forall yS\mathrm{s}(u, u, y, X;\overline{\mathrm{Y}}\alpha))$. Pick an$n-\Sigma_{1}^{1}(\overline{\mathrm{Y}})$

formula.

$e$$C_{0}(u, y, x;\overline{\mathrm{Y}}, \alpha)rightarrow S_{3}(e, u, y, X;\overline{\mathrm{Y}}, \alpha_{\square })$$C\equiv\exists\alpha\forall yC\mathrm{o}(u, y, x;\overline{\mathrm{Y}}, \alpha)$$P^{\Phi}(\overline{\mathrm{Y}}, x)\equiv B(e, x;\overline{\mathrm{Y}})$

By Lemmata 5.2 and 5.4 we get the
Lemma 5.5 For each $\Phi\in POS$ there exists a formula$P^{\Phi}(x)$

in

$L$

such that$EL+AC-NF\vdash\forall x\{P^{\Phi}(X)rightarrow\Phi[\{X\}P^{\Phi}(x)/X]\}$

Let $EL+AC-NF+I\hat{D}_{n}^{i}$ denote an extension of $EL+AC-NF$ . Its language is obtained from byfor eachadding a unary set constant( : a fixed set parameter) and its axioms are those of:language plus the$EL+AC-NF$ in$L$$I^{\Phi}$$\Phi\in POS^{*}(\mathrm{Y})$$\mathrm{Y}$$<\backslash \mathrm{x}\mathrm{i}_{ J}^{\tau}\mathrm{m}(FP)_{n}^{\Phi}$$\ \mathrm{e}\succ^{-\mathrm{X}}.\mathrm{P}^{\mathrm{a}\mathrm{n}\mathrm{d}\mathrm{e}\mathrm{d}}$$(FP\}_{n}^{\Phi}\forall i<n\forall x[I_{i}\Phi(X)rightarrow\Phi(I_{<i}^{\Phi\Phi}, I_{i}, x)]$where

$I_{i}^{\Phi}(X_{\text{ノ}^{})}\equiv I^{\Phi}(_{r}^{\dot{\eta}(i,x))}\backslash ’ I_{<i}^{\Phi}(k, X)\equiv k<i\wedge I_{k}^{\Phi}(x)$and$\Phi\equiv\Phi(\mathrm{Y}, X, x)$.

Theorem 5.1 $EL+AC-NF+I\hat{D}_{n}^{i}$ is a definitional extension of $EL+AC-NF,$ $i.e.$ , the set constantis definable in $EL+AC-NF$ , and hence,
via N. Goodman’s theorem [1212 $EL+AC-NF+I\hat{D}_{n}^{i}$ is a conservative extension of $HA$ for each .

$I^{\Phi}$$n$

Proof. Construct$P_{0}^{\Phi},$$P_{1’-1}^{\Phi}\ldots,$$P_{n}^{\Phi}$

successively by Lemma 5.5.

$\square$Classical fixed point theories

6

Let
denote the second order language obtained from the language of the first order arithmetic by adding
set variables $X,$
Let $T\supseteq ACA_{0}$ denote a second order arithmetic containg $ACA_{0}$ . Assume thatis–faith , i.e., any -consequence in is true. Then, by [11], we have for a recursive theory ,$L_{2}$$T$$\mathrm{Y},$$\ldots$$\Pi_{1}^{1}$$fu\mathrm{J}$$T$$\mathrm{n}_{1}^{1}$$|F|=_{d}f \sup${$T\vdash I(\prec)$$\alpha$$T$for some recursive well ordering$\prec$of type$\alpha$}$<\omega_{1}^{CK}$

wheredenotes the -sentence $\forall XPrg[\prec, X]arrow\forall xX(x)$ . $Prg[\prec, X]$ denotes that $X$ is progressive withrespect
in Section 3.
The proof theoretic ordinal $|T|$ of is free from pathology, while the following alternative definition of theproof theoretic ordinal make sense relative to a vague natural well:$I(\prec)$$\Pi_{1}^{1}$$\mathrm{t}\mathrm{o}\prec \mathrm{a}s$$T$$\mathrm{o}\mathrm{r}\mathrm{d}\mathrm{e}\mathrm{r}\mathrm{i}\mathrm{n}\mathrm{g}\prec$$|T|0=_{df} \sup${$\alpha$:$T\vdash I(\prec,$$\Pi_{0}^{1-})$for some recursive well ordering$\prec$of type$\alpha$}wheredenotes the set of arithmetical formulae without set parameters andthe schema oftransfinite inductionto
Let $FP-ACA_{0}$; and FP-ACA’ denote second order arithmetic in the ianguage(without set constantsdiffering from [16] which are obtained from $ACA_{0}$ and $ACA$ , resp. by addind the following
axiom:$I(\prec, \Pi^{1}-)0$$\Pi_{0}^{1-}$$a$$\mathrm{o}\mathrm{f}\prec \mathrm{a}\mathrm{p}\mathrm{p}\mathrm{l}\mathrm{i}\mathrm{e}\mathrm{d}$$\mathrm{f}\mathrm{o}\mathrm{r}\mathrm{m}\mathrm{u}\mathrm{l}\mathrm{a}\in\Pi_{0}^{1-}$$L_{2}$$P_{A}$$\Sigma_{1}^{1}$$)$$(FP)\exists X\forall x(A[X, X]rightarrow X(x))$

for each $X$ positive arithmetical formula $A[X, x]$ in
Then G. J\"ager and B. Primo [16] shows that

$L_{2}$( $A[X,$ $X]$ contains no free variable except $X$ and $x.$ )Theorem 6.1 (G. \"ager and B. Primo [16])$\mathrm{J}$

1. $|FP-AcA_{0}’|=\epsilon_{0}$

2.

$|$

FP–ACA’$|=\epsilon_{\epsilon_{0}}$3. $FP-ACA_{0}$’ and$\Sigma_{1}^{1}-AC$

are proof theoretically equivalent each other.

Here note that $|ACA_{0}|=\epsilon_{0},$and. Also $FP-AcA_{0}$’ is proof theoreticallystronger than $ACA_{0)}$ e.g., by a truth definition for arithmetical formulae in $\Pi_{0}^{1-}FP-ACA’0\vdash c_{\mathit{0}}n(ACA\mathrm{o})$ .
We observe that the above theorem follows from a result due to G.
or [24], pp.176-177:$|ACA|=\epsilon_{\epsilon_{0}}$$|\Sigma_{1}^{1}-AC|=\varphi\epsilon_{0}0$$\mathrm{K}\mathrm{r}\mathrm{e}\mathrm{i}_{\mathrm{S}\mathrm{e}}1[17]$Theorem 6.2 Let$T$

be a recursive;$\Pi_{1}^{1}$-faithful second order arithmetic contamg$ACA_{0}$.

110
1. (G.

$\mathrm{K}\mathrm{r}\mathrm{e}\mathrm{i}_{\mathrm{S}}\mathrm{e}1[17]$)$|T|= \sup$2. Let$Tr_{\Sigma_{1}^{1}}${ :$\alpha$denote the set of true

$T\vdash I(\prec)$for somesentences in$\Sigma_{1}^{1}$$L_{2}$$\Sigma_{1}^{1}$

well ordering$\prec$of type$\alpha$}. Then$|T|=|\tau+Tr_{\Sigma^{1}1}|$

Proof. Assume $T+A\vdash I(\prec)$ for a primitive recursive well orderingby$\prec$and an$A\in Tr_{\Sigma_{1}^{1}}$. Define a$\Sigma_{1}^{1}$well$\mathrm{o}\mathrm{r}\mathrm{d}\mathrm{e}\mathrm{r}\mathrm{i}\mathrm{n}\mathrm{g}\prec_{A}$$n\prec_{A}m\Leftrightarrow_{dj}$Then we have

$T\vdash I(\prec_{A})$n\prec m&A.

. By the Kreisel’s result, the order type$\mathrm{o}\mathrm{f}\prec \mathrm{i}\mathrm{s}$

equ

$a1$

to the order type$\mathrm{o}\mathrm{f}\prec_{A}\leq|T|$.

$\square$fold iterated fixed point theory $FP_{n}-ACA\prime 0\cdot FP_{n}-ACA’0$ is obtained
The theorem is applied to theaxiom $(FP_{n})$ :from $ACA_{0}$ by adding the$n\mathrm{t}\mathrm{h}$$\Sigma_{1}^{1}$$(FP_{n}) \exists XX\forall Xn’\cdots,1\bigwedge_{1\leq i\leq n}(x\in X_{i}rightarrow A_{t}(X_{i}+, X_{1}, \ldots, X_{i1}-, x))$in the language $L_{2}+\{X_{1}, \ldots, X_{i}\}$ .
positive formula’$FP_{n}-ACA$ is obtained from $FP_{n}-AcA_{0}$’ by adding the full induction schemafor each$A_{i}$$X_{i}$

Corollary 6.1 For any$n\in\omega$$\Pi_{\infty}^{1}-IA$.

,

1. $|FP_{n}-AcA_{0}’|=\epsilon_{0}$2. $|FP_{n}-AcA’|=e_{\epsilon_{0}}$Thus the theories $FP_{n}-ACA_{0}’$ is weak with respect to the proof theoretical ordinal $|T|$ . But these are
proof theoretically much
. er than $ACA_{0}$ . In the following we compute the other proof theoretical ordinal$|FP_{n}-AcA_{0}’|_{0}$ , etc.
(the first strongly critical number). Ordinals
a standard well ordering of type
In what follows let
and their codes are identified and denoted by$\mathrm{s}\mathrm{t}_{\Gamma \mathrm{O}}\mathrm{n}\mathrm{g}$$<\mathrm{d}\mathrm{e}\mathrm{n}\mathrm{o}\mathrm{t}\mathrm{e}$$\leq$$\Gamma_{0}$$\Gamma_{0}$$\alpha,$$\beta,$$\ldots$

be a first order theory containg $PA$ . A first order theory(fixed point
1. LetDefinition 6.1
of
is obtained from the language
oftheory over ) is defined as follows: The language$X$$A[X^{+},$$x]\inL_{T}(X),$positive }.
by adding the set constants {:Axioms $I\hat{D}(T)=T+$ induction schema for $L_{Ii)(T}$ ) $+(FP)$$I\hat{D}(T)$

$T$

$T$

$L_{I\hat{D}(T)}$$T$$I\hat{D}(T)$$L_{T}$$P_{A}$$(FP)\forall x(X\in P_{A}rightarrow A[P_{A}, x])$

2. $I\hat{D}_{0}=PA$ and3.

$L^{n}=L_{I\hat{l})(T)}$

4. the norm of$I\hat{D}_{n+1}=I\hat{D}(I\hat{D}_{n})$.

and $L_{2}^{n}=L^{n}+$ second order variables $X,$
$I\hat{D}_{n}(n\neq \mathit{0})$$\mathrm{Y},$$\ldots$

is defined to be the following ordinal with$\inf\{\alpha :$|k|_{A}<\alpha\Leftrightarrow k\in I_{A}^{<\alpha}$:\forall A[X, x]\in L^{0}(X)\forall k\in\omega[I\hat{D}_{n}\vdash k\in P_{A}\Rightarrow|k|_{A}<\alpha\}]$5. $FP_{n}-ACA=ACA$ for the language$L_{2}^{n}+I\hat{D}_{n}$and $FP_{n}-ACA\prime 0$ [ $FP_{n}-ACA$ and $FP_{n}-ACA’$ ] have the same arithmetical provable
we writefor, resp. For a fixedwith $A_{n}=A[X^{+}, \sum i<n]P_{i}, X$ . Thus
extra constants $P_{i}(i<n)$ for each .
Clearly$I\hat{D}_{n}$$\mathrm{f}_{\mathrm{o}\mathrm{r}\mathrm{m}}\mathrm{u}\mathrm{l}\mathrm{a}\mathrm{e}\in$$L^{0}=\Pi_{0}^{1-}$$A[X^{+}, \mathrm{Y}, x]\rangle$$P_{n}$$P_{A_{n}}$$I\hat{D}_{n}$$A$

Definition 6.2 Let$\Phi$

be a set of formulae.

1. $I(<\alpha, \Phi)$ denotes the schema of transfinite induction up to each$\beta<\alpha$applied to a$\mathrm{f}\mathrm{o}\mathrm{r}\mathrm{m}\mathrm{u}\mathrm{l}\mathrm{a}\in\Phi$

.

has

111
2. A first order theory

is defined as follows: its language$H(\Phi)^{<\alpha}$$=L_{0}+\mathrm{t}\mathrm{h}\mathrm{e}$language of $\Phi+\{H_{A}$ : $A\in$$\Pi_{0}^{1-}(\Phi, x)\}$is aformula relative to $X$ formulae
for the language of $H(\Phi)^{<\alpha}+(H)$ :$(A\in\Pi_{0}^{1-}(\Phi, X)\Leftrightarrow df$$H(\Phi)^{<\alpha}=PA$$A$$\in\Phi$$\Pi_{0}^{1}$).

$(H)\forall x(x\in H_{A}^{\beta}rightarrow A[H_{A}^{<\beta}, X])$for each$\beta<\alpha$Thus $(H)$ says that.

$H_{A}^{<\beta}= \sum_{\gamma<\beta A}H^{\gamma}$$\{H_{A}^{\gamma} :\gamma\leq\beta\}$forms the ’jump’ hierarchy relative to$\mathrm{f}_{\mathrm{o}\mathrm{r}\mathrm{m}}\mathrm{u}\mathrm{l}\mathrm{a}\mathrm{e}\in\Phi$.

1. For each $B\in L^{m}(m<n)$ ,Theorem 6.3$I\hat{D}_{n}\vdash B\Leftrightarrow H(L^{m})^{<\alpha_{n-}}m+I\hat{D}_{m}\vdash B\Leftrightarrow I\hat{D}_{m}+I(<\alpha_{n-m+1}, L^{m})\vdash B$

where

2.

$\alpha_{1}=\epsilon_{0},$with the Veblen function$\alpha_{n+1}=\varphi\alpha_{n}O$$\varphi\alpha\beta$.

$|I\hat{D}_{n}|_{0}=\alpha_{n+1}$

3. For each $B\in L^{m}(m<n)$ ,$FP_{n}-ACA\vdash B$$\Leftrightarrow$$\Leftrightarrow$

where$\beta_{1}=\epsilon_{\epsilon_{0}},$$\beta_{n+1}=\varphi\beta_{n}O$$H(L^{m})^{<\beta_{n-}}m+I\hat{D}_{m}\vdash B$$I\hat{D}_{m}+I(<\beta n-m+1, Lm)\vdash B$.

4. $|FP_{n}-AcA|0=\beta n+1$
5. the norm of
6. the norm of $FP_{n}-ACA=\beta_{n}$$I\hat{D}_{n}=\alpha_{n}(n\neq \mathit{0})$This is proved by using usual techniques in [16] and [8].
over the language() is designed as the first order
Proof of 1 and 2. An infinitary system, i.e., fixed points rules inpart of $FP$ –ACA* in [16], in the language
are only for
and$P_{n-}1\in L^{n}$ are treated as set parameters in. Thusis the first order part
constants
for $B\in L^{n+1}$ where
denotes the axiom for the constantof $FP$ -ACA* in [16]. Put$I\hat{D}^{\infty}$$I\hat{D}^{\infty}(L^{\mathrm{n}})$$L^{n}$$I\hat{D}^{\infty}(L^{n})$$L^{n}$$P_{0},$$I\hat{D}^{\infty}(L^{n})$$\ldots,$$FP_{i}$$B_{n} \equiv\bigwedge_{i<n}FP_{i}\supset B$$P_{i}$$P_{n}$$I\hat{D}^{\infty}(L^{0})$.

$\square$Lemma 6.1

2.

1.

$I\hat{D}_{n+1}\vdash B\Rightarrow I\hat{D}^{\infty}(L^{n})\vdash_{1}<\epsilon_{0}B_{n}$$FP_{n+1^{-}}AcA\vdash B\Rightarrow I\hat{D}^{\infty}(L^{n})\vdash_{1}<\epsilon_{e_{0}}B_{n}$For a proof we set the rank $rn(F)=0$ ifwith respect to$F\in \mathcal{P}N_{n}$$P_{n}$. The rest is the same in [16].

Lemma 6.2 For an -number ,$\epsilon$

1.

$\alpha$

with
by
of
resultreplacing each negative
system whose extra rules are, for each$I\hat{D}^{\infty}(L^{n})\vdash_{1}^{\alpha_{0}}B$$B\in \mathcal{P}N_{n}\Rightarrow\forall\beta<\alpha[(I_{n}^{<\alpha})\vdash_{<\alpha}^{<\alpha}\{\beta\}B\{\beta+\omega^{\alpha_{0}}\}]$$P_{n}$and each positive$I_{n}^{<\beta}$$\beta<\alpha$$P_{n}$

by,$\frac{\Gamma,[\neg]A[I^{<\beta},\sum ni<nP_{i},S]}{\Gamma,[\neg]_{S\in}I_{n}\beta}$2.

$(I_{n}^{<}\alpha)\vdash<\alpha<\alpha B\Rightarrow(I_{n}^{<\alpha})\vdash 0<\varphi\alpha 0B$

3.

$I\hat{l})^{\infty}(L^{n})\vdash_{1}<\alpha B_{n}$with $B\in L^{n}$ ($P_{n}$

does not occur in

$B$

where
and

$I_{n}^{<\beta’}$)$\Rightarrow I\hat{D}^{\infty}(L^{n-1})\vdash_{1}<\varphi\alpha 0B_{n-1}$

Lemma 6.3
$H(X)<\omega^{a}\vdash I(<\varphi aO, X)$

We give a sketch of a proof of this lemma below. From this lemma we see the$\{\beta\}B\{\beta’\}$$(I_{n}^{<\alpha})$denotes theis an infinitary

112
Lemma 6.4
$H(L^{m})^{<\alpha_{n}}-m\vdash I(<\alpha_{n-m+1}, L^{m})(m\leq n, \alpha_{0}=\mathit{0})$Thus we have shown the direction$I\hat{l})_{m}+I(<\alpha_{n-m+1}, L^{m})\vdash B\Rightarrow H(L^{m})^{<\alpha_{n}}-m+I\hat{D}_{m}\vdash B$

Next consider the direction$I\hat{D}_{n}\vdash B\Rightarrow I\hat{D}_{m}+I(<\alpha_{n-m+1}, L^{m})\vdash B$

with $B\in L^{m},$ $m<n$ . By Lemma 6.1 we have forAssume6.2 we successively have
$I\hat{l})_{n}\vdash B$$I\hat{D}^{\infty}(L^{m})\vdash_{1}<\alpha_{n-m}B_{m},$and$B_{m}$$(I_{m}^{<\alpha_{n-m}})\vdash_{<\alpha_{n-}}^{<\alpha_{n}}$$\alpha_{1}=\epsilon_{0}I\hat{D}^{\infty}(L^{n-}1)\vdash_{1}<\alpha_{1}B_{n}$$(I_{m}^{<\alpha_{\mathfrak{n}}}-m)\vdash_{0}<\alpha_{\mathfrak{n}}-m+1B_{m}$. By Lemma.

By a patial truth definition we get $I\hat{D}_{m}+I(<\alpha_{n-m+1}, L^{m})\vdash B$ .
Finally consider the direction$H(L^{m})^{<\alpha_{\mathfrak{n}-}}m+I\hat{D}_{m}\vdash B\Rightarrow I\hat{D}_{n}\vdash B$.

This follows from Lemma 6.5 below. We interprete $H(L^{m})^{<\alpha_{n}}-m+I\hat{D}_{m}$ inleave$L_{m}$$I\hat{D}_{n}$as follows:

formulae unchanged.

is interpreted asso that $P_{A}^{+}=H_{A},$the ’jump’ hierarchy $H_{A}(A\in\Pi_{0}^{1-}(L^{m}))$ up). Then for each in the language of $H(Lm)<\alpha n-m+$(simultaneously defined as fixed points over.
byby
and negative
let $B’$ denote the result of replacing the positive$P_{A}^{+},$$\mathrm{t}\mathrm{o}<\alpha_{n-m}$$\bullet$$P_{A}^{-}=$$P_{A}^{-}$$B$$L^{m}$$\neg H_{A}$$I\hat{D}_{m}$$H_{A}$$H_{A}$$P_{A}^{+}$$P_{A}^{-}$

Lemma 6.5 $1)_{m}H(L^{m})^{<\alpha_{n}}-m+I\hat{D}_{m}\vdash B\Rightarrow I\hat{D}_{n}\vdash B’,$ $i.e.$ ,.
for each$I\hat{D}_{n}\vdash\forall x(x\in H_{A}^{\beta}rightarrow\neg(x\not\in H_{A}^{\beta}))$$\beta<\alpha_{n-m}$$\mathit{2})_{m}I\hat{D}_{n}\vdash I(<\alpha_{n-m+1}, L^{m})(m\leq n)$. It remains to show.
andProof by simultaneous induction on $n-m$ . We have.
By Lemma 6.4 and $I(<\alpha_{n-m+1}, L^{m})\in L_{m}$ we get
Thus we have proven Theorem 6.3.1 and 2.
is obtained from Lemmata. The upper boundfor the norm of
Finally consider the norm of
6.1 and 6.2.
To obtain the lower bound, define a fixed point $W=W_{0}$ by$2)_{m+1}\Rightarrow 1)_{m}$$2)_{n}$$1)_{m}\Rightarrow \mathit{2})_{m_{\square }}$$\mathit{2})_{m}$$I\hat{D}_{n}$$I\hat{D}_{n}$$\alpha_{n}$$\forall\beta(\beta\in Wrightarrow\forall\gamma<\beta(\gamma\in W))$

By Lemma$6.5.\mathit{2})_{1}$, we have$I\hat{D}_{n}\vdash I(<\alpha_{n}, L^{1})$$I\hat{D}_{n}\vdash\forall\beta(\forall\gamma<\beta(\gamma\in W)arrow\beta\in W)$$\mathrm{P}\mathrm{r}o$of of Lemma6.3. Put$\lambda=\omega^{a}$, we get. Hence by $W\in L^{1}$ andfor each$I\hat{D}_{n}\vdash\beta\in W$$\beta<\alpha_{n}$.

and$I_{X}^{<\beta}(\gamma)\Leftrightarrow df\forall \mathrm{Y}\in\cup ReC(H_{\delta}\mathrm{x})I(\gamma\delta<\beta’ \mathrm{Y})$

where

1.

$H_{\delta}^{X}$

2.

$Rec(H^{X})\text{\’{o}}$3.

$I(\gamma, \mathrm{Y})$denotes the

Also for each$\delta^{th}$jump of the set $X$

denotes the set of sets recursive in$H_{\delta}^{X}$

denotes the transfinite induction up to$\alpha<\lambda$$\gamma$.
applied to Y.

,$A_{\alpha}^{X}(\gamma)\Leftrightarrow dj\gamma>\mathit{0}arrow\forall\beta\forall\delta>\mathit{0}[I^{\omega^{\gamma}(\delta}X+1)(\beta)\ \omega^{\gamma}(\delta+1)\leq\alphaarrow I_{X}^{<\omega^{\gamma}\delta}(\varphi\gamma\beta)]$

Then we can prove the following lemma as in [8]:113
Lemma 6.6 For each$\alpha<\lambda$,$H(X)^{<\lambda}\vdash Prg[A^{X}\alpha]$

Lemma 6.7
$H(X)^{<\lambda}\vdash I(<\lambda)$

where $I(<\lambda)$ denotes the .\S chema of
the language of.

$l^{\eta \mathfrak{n}}ansfinite$

induction up to each ordinal

and applied to any formula in$<\lambda$$H(X)^{<\lambda}$

Proof. For
1.

$\alpha<\lambda$

let$S\alpha$denote a fini-te set of ordinals$\leq\alpha$inductively generated as follows:$\alpha\in S\alpha$

2. If$\beta=\beta_{1}+\cdots+\beta_{n}\in S\alpha,$

3. If$\varphi\gamma\delta\in S\alpha$

We show
Assume thatis additiveand is, then$\delta\in S\alpha$$\gamma,$that$\beta_{1}>\cdots>\beta_{n}$&\mbox{\boldmath $\gam $}$\beta_{1},$$\beta n$$\ldots,$

are additive principal, then$\beta_{1},$$\ldots,$$\lambda$$\forall,\beta\in S\alpha H(X)^{<\lambda}\vdash I(\beta)$$\gamma>0\ \alpha,’\gamma\delta\in S\alpha,$ $I(\gamma)$$\mathrm{a}\langle^{1}1\mathrm{d}\mathrm{i}\mathrm{t}\mathrm{i}\mathrm{v}\mathrm{e}\mathrm{I}$$U$$I(\delta)$$I(\varphi\gamma\delta, U)$$Prg[A_{\alpha 2}U]$$\mathrm{r}\mathrm{i}\mathrm{n}\mathrm{c}\mathrm{i}\mathrm{p}\mathrm{a}\mathrm{l}$$\forall\beta[X_{U}^{<2}\omega^{\sim}(\beta\grave{j}’arrow I_{U^{\wedge}\backslash }^{<\omega^{\gamma}/}\varphi\gamma\beta)]$7

and$\omega^{\gamma.\underline{?}}<\omega^{\varphi\gamma\delta}\cdot 2=\varphi\gamma\delta\cdot 2\leq\alpha\cdot 2<\lambda$$\mathrm{p}\mathrm{r}_{1}^{;}\mathrm{n}\mathrm{c}\mathrm{i}\mathrm{P}^{\mathrm{a}}1,$.

.

.
. For a given formuia we have to show
. Also $H(U)^{<\lambda}=H(X)^{<\lambda}$ since). Thus by Lemma 6.6 we have
. By
, we have. By
we ave. Thusand.
Now Lemma 6.3 follows from Lemmata 6.6 and 6.7.
$\mathrm{i}\mathrm{n}\mathrm{d}\mathrm{u}\mathrm{C}\mathrm{t}\mathrm{i}_{\mathrm{V}}\mathrm{e}1\mathrm{y}1$$\beta_{n}\in S\alpha$$J(\mathit{0}^{c})$$I_{U}^{<\omega^{\gamma_{\circ}}}\sim(\delta)$$\mathrm{n}$Iterated reflection formulae$I(\gamma)$$I_{U}^{<\omega^{\gamma}}(\varphi\gamma\delta)$$\mathrm{a}\mathrm{r}_{\wedge}\mathrm{d}\mathrm{F}\mathfrak{U}\mathrm{B}\mathrm{e}\mathrm{S}$. Since$\lambda=\omega^{a}$$U \in\bigcup_{\delta<\lambda}Rec(H^{x})\delta$$A_{\alpha 2}^{U}(\gamma)$

and$\mathrm{h}\mathrm{e}\mathrm{n}\mathrm{c}\mathrm{e}\square$$I(\varphi\gamma\delta, U)$of transfinite induction

In this section we give an equivalence between transfinite induction rule and iterated reflection schema overthe fragment
of $PA$ .
In this section
a standard
well ordering.
$j\zeta\Sigma_{\mathrm{J}}n$$<\mathrm{d}\mathrm{e}\mathrm{n}\mathrm{o}\mathrm{t}\mathrm{e}\mathrm{s}$$\epsilon_{0}$Definition
1. For an additive principal number
and a set of formulae,
denotes thetransfinite induction rule up to and applied to a formula $A\in\Phi$ : Put $Prg[A]\Leftrightarrow dj\forall x(\forall y<xA(y)\supset$$A(x))$ . Then for each $A\in\Phi$$7_{0}1$$TIR[\alpha, \Phi]$$\Phi$$\alpha\geq\omega$$\alpha$$\frac{Prg[A]}{\forall x<\alpha A(_{X)}}$

is an instance of the rule

$TIR[\alpha, \Phi]$.

2. For a theory containg the fragment
let $T+TIR[\alpha, \Phi]$ denote the theory obtained fromby
$TIR[\alpha.\Phi]$$T+TIR^{(m)}[\alpha,\Phi](m\in\omega)$ denotes a formal
adding the rule
. Alsoinwhich the ru’-e
can be applied nestedly at mosttimes.
For exalnple
and 1) in $T+TIR^{(1)}[\alpha, \Phi]$ the rulecan be applied only
$T$

$T$

$I\Sigma_{1}$$\mathrm{s}\mathrm{y}\mathrm{s}\mathrm{t}\mathrm{e}\mathrm{m}\subseteq T+TIR[\alpha, \Phi]$$TIR[\alpha, \Phi]$$m$$0\grave{\dot{;}}T\cdot\cdot\vdash TIR^{(0)}[\alpha, \Phi]=T$$TIR[\alpha, \Phi]$

when $T\vdash Pr.0[A](A\in\Phi)$ . etc.

3. For a theory
in
we have$T\supseteq I\Sigma_{1}$let$C_{\eta}^{T}(_{\backslash }\alpha)$denote the iterated reflection formula defined in U. Schmerl [19]. Thus

$I\Sigma_{1}$$(/_{a)}c_{n\backslash ^{0)}}^{T/}rightarrow RFN_{\Pi_{\mathrm{n}+1}}(T)$$\mathrm{i}^{(b)}\sigma_{n}^{\tau_{(_{C\prime}}}+1)$$\sim$R_{-}^{\Gamma}W\mathrm{n}+1(^{\Gamma_{-}}\mathrm{L}r\mathrm{r}C_{n}^{\tau_{(}}\alpha_{\grave{)}\grave{J}}$$(c)C_{n}^{T}(\lambda)rightarrow\forall\alpha<\lambda C_{n}^{T}(\alpha)$

4.

for a limit$=_{dj}\mathrm{F}+\{CT(n\beta):_{l}\theta<\alpha\}$Proposition 7.1 Over$I\Sigma_{1}$as$\lambda$.

$\wedge|.11’\lfloor 19$].

,$TIR[\omega^{2+}, \Sigma_{n}\alpha]=TIR[\omega^{1+\alpha}, \Pi n+1]$

Proof. This is contained in the proof of Theorem 4.1. e) in$\mathrm{L}\lceil‘ A3$]$\square$

A formula $A(x)$ is called refiexively progressive (in ) with respect to a theory
$x$

$T$

if

$T\vdash\forall x[\forall y<xPr\tau()’ A(\dot{y})" )\supset A(x)]$with a canonical provability predicate$Pr_{T}$for$T$

and the g\"odel number

”

$E$ ”

of an expression $E$ .

114
Proposition 7.2 (cf. [19], p.337)$T\vdash A(x)\Leftrightarrow A(x)$Remark. The proof of the direction

is reflexively progressive with respect to$T$in [19] uses L\"ob’s theorem and the facts:$[\Leftarrow]$

1. $T\vdash y<z\supset Pr\tau(" \dot{y}<\dot{z})’$ )2. $T\vdash<$ is transitive
Proposition 7.2 holds if is demonstrably transitive in . In other words,
binary relation
Thus anyreflexive progressiveness is nothing to well foundedness although the name remind us the latter.

Lemma 7.1 For

1.

and

$A\in \mathrm{I}\mathrm{I}_{n+1}$

if$T\supseteq I\Sigma_{1}$,is reflexively progressive with respect to$B(\alpha)\equiv C_{n}^{T}(\alpha)\supset A(\alpha)$$T\vdash C_{n}^{T}(0)\supset Prg[A]$

$T$

$<$

$<$

$\Sigma_{1}$$T$.

2. $T\vdash Prg[A]\Rightarrow T+C_{n}^{T}(O)\vdash Prg[\forall x<\omega(1+\alpha)A(x)]$.
3.

$T\vdash Prg[A]\Rightarrow T\vdash C_{n}^{T}(\alpha)\supset\forall x<\omega(1+\alpha)A(x)$.

Proof.

1. Assume $T\vdash C_{n}^{T}(0)\supset Prg[A]$ . We can assume that$T\vdash C_{n}^{T}(0)\supset A(O)$ . Then we have by $A\in\Pi_{n+1}$ ,$\alpha\neq 0$

since$T\vdash\forall\beta<\alpha Pr_{T}(" C^{\tau}(n\dot{\beta})\supset A(\dot{\beta})" )\ c_{n}^{T}(\alpha)\supset\forall\beta<\alpha A(\beta)$

By our assumption $T\vdash C_{n}^{T}(\alpha)\supset Prg[A]$ .

2. Assume $T\vdash Prg[A]$ . Consider the case $\alpha=0$ . Then we have to show $T+C_{n}^{T}(O)\vdash\forall x<\omega A(x)$ . This). Other cases are similar.
) or better
follows from$T\vdash\forall n<\omega Pr_{T}()’\forall X<\dot{n}A(X)$$T\vdash\forall n<\omega Pr\tau(" A(\dot{n})’)$”$\square$Lemma 7.2 Assume

and$T\supseteq I\Sigma_{n}$

$A$

is a

$\mathrm{I}\mathrm{I}_{n+1}$-sentence. Then

$T\vdash A\Rightarrow T+TIR^{()}1[\omega^{1+}\alpha, \Pi_{n}+1]\vdash C_{n}^{I\Sigma_{n}+A}(\underline{\omega^{\alpha}})$with$\omega^{\alpha}$$\alpha\neq \mathit{0}$$0$$otherwi_{\mathit{8}}e$$\underline{\omega^{\alpha}}=_{dj}\{$

Proof. Let $B(\omega\beta+p)$ denote the$\beta<\omega^{\alpha}$$\mathrm{I}\mathrm{I}_{n+1}$-formula:$\ p<\omega\$$\forall\Gamma\subseteq\Pi_{n+1}\{Prov_{I\Sigma n}(p,’\neg A), \neg C_{n}I\Sigma_{n}(\dot{\beta}-1), \Gamma" )\supset Tr_{\Pi_{h}}+1()’\mathrm{r}" )\}$

where

1.

2.

$\Pi_{n+1}=\mathrm{t}\mathrm{h}\mathrm{e}$$\Pi_{n+1}$) is a proof predicate foris formulated in a Tait’s calculus.

$Prov_{I\Sigma_{n}}(p, " \Gamma’)$$I\Sigma_{n}$3.

set of g\"odel numbers of$Tr_{\Pi_{n+1}}$

denotes a parti$a1$-formulae$I\Sigma_{n}$truth definition for

4. $\beta-1=_{df}$ if $\beta=n<\omega$ then $n-1$ else , and$\beta$which says that$\Pi_{n+1}$$p$

is a proof of a sequent$\Gamma$in$I\Sigma_{n}$. Here-fomulae.

$C_{n}^{I\Sigma_{n}}(-1)$

denotes a true formula, e.g., $0=0$ .

, every sequent in the proof is of theandWe assume that when
. This follows from a partial cut elimination which is available
for some
form
.
in
. By
. Hence
We show that $T\vdash Prg[B]$ . Argue in . We have andis analysed by an inference rule
induction on $p<\omega$ we get F. If’
andare true.
then use the fact:$Prov_{I\Sigma_{n}}(p, )’\neg A,$ $\neg C_{n}I\Sigma_{n}(\dot{\beta}-1),$ $\Gamma)’)$$\Gamma\subseteq \mathrm{I}\mathrm{I}_{n+1}$$\neg A,$ $\neg C_{n}^{I\Sigma_{n}}(\beta-1),$$\Delta$$p$$\Delta\subseteq \mathrm{I}\mathrm{I}_{n+1}$$I\Sigma_{1}\subseteq T$

$T$

${ }$

$a$

$A$

$\forall\gamma<\beta\forall p<\omega B(\omega\gamma+p)$$c_{\mathrm{n}}^{I\Sigma_{n}}(\beta-1)$$\Sigma_{n+1^{-}}\mathrm{f}_{\mathrm{o}\mathrm{r}\mathrm{m}\mathrm{u}}1\mathrm{a}\in\{\neg A, \neg c_{n}^{I}\Sigma_{n}(\beta-1)\}$$(\exists)\square$$A$$C_{n}^{I\Sigma_{n}}(\beta-1)$

115
Theorem 7.1 For each

and$\alpha\geq 0$$\mathit{0}<n,$$m<\omega$,.

$I\Sigma_{n}+TIR^{(}m)[\omega 1+\alpha, \Pi_{n}+1]=I\Sigma_{n}+C_{n}^{I}\Sigma_{n}(\omega m)\alpha$with$\underline{\omega^{\alpha}\cdot m}=_{df}\{$

Proof.

$[\subseteq]$

By induction on$m\geq \mathit{0}$$\omega^{\alpha}\cdot m$$\alpha\neq \mathit{0}$$m-1$otherwise, we show, for $A\in\Pi_{n+1}$$I\Sigma_{n}+C_{n}^{I\Sigma_{n}}(\underline{\omega m})\alpha.\vdash Prg[A]\Rightarrow I\Sigma_{n}+C_{n}^{I\Sigma_{n}}(\omega^{\alpha}\cdot(m+1))\vdash\forall x<\omega^{1+\alpha}A(X)$

where
. Put
Also
This follows from Lemma 7.2.
$I\Sigma_{n}+c^{I\Sigma}nn(\underline{\omega 0\alpha.})=I\Sigma_{n}$$T=I\Sigma_{n}+c_{n}^{I}\Sigma n(\underline{\omega^{\alpha}\cdot m})$

$T+C_{n}^{T}(\underline{\omega^{\alpha}})=I\Sigma_{n}+C_{n}^{I\Sigma_{n}}(\omega^{\alpha}\cdot(m+1))$. By Lemma 7.1$T\vdash C_{\mathrm{n}}^{T}(\underline{\omega^{\alpha}})\supset\forall x<\omega^{1+\alpha}A(X)$$[\supseteq]$$\square$In what follows we concentrate on the case $n=1$ . For a limit ordinal
fundamental sequence given in the Definition 3.7 in [23], i.e.,$\lambda<\epsilon_{0},$$\omega^{\alpha+1}[x]=\omega^{\alpha}\cdot(x+1)$

Definition 7.2 Fast growing
1.

$F_{\alpha}$.

.

$function\mathit{8}F_{\alpha}$denotes the$\{\lambda[x]\}_{x\in\omega}$

.

.

.

$(a)F_{0}(x)=\mathit{2}x+\mathit{2}$$(b)F_{\alpha+1}(x)=F^{(x}\alpha()2)$$(c)F_{\lambda}(0)=2$

for a limit$(d)F_{\lambda}(x)=F_{\lambda[x]}(X)$2.
3.

$F_{\alpha}(x)\downarrow \mathrm{d}\mathrm{e}\mathrm{n}\mathrm{o}\mathrm{t}\mathrm{e}\mathrm{S}$a$\Sigma_{1}$2. For a set, resp.

: a$\Pi_{2}$$T\supseteq I\Sigma_{1},$is defined’.

formula$\{(\alpha, x, y) :F_{\alpha}(x)=y\}$is$\triangle 0$

definable.

and ER $(F)$ .

$PR(\mathcal{F})$$Tot(T)$ denotes the set of provably total recursive functions in $T$ .

of functions on$\mathcal{F}$$x\neq \mathit{0}$$F_{\alpha}(x)$R. Sommer [23] shows that the graph

1. For a theory

andformula saying ’$F_{\alpha}\downarrow\Leftrightarrow_{df}\forall x\in\omega(F_{\alpha}(x)1)$

Definition 7.3 Tot $(T),$$\lambda$$PR(\mathcal{F})[ER(\tau)]$$\omega,$denotes the primitive [elementary] recursive closure of$\mathcal{F}$

Lemma 7.3

1. Each$)\subseteq PR(F_{\alpha})$$f\in Tot(I\Sigma_{1}+F_{\alpha}\downarrow)$

is majorized by an$F_{\alpha+n}$.

2.

$I\Sigma_{1}\vdash F_{\alpha}\downarrowarrow F_{\alpha+1}\downarrow$

3.

$I\Sigma_{1}\vdash F_{\alpha+\omega}\downarrowrightarrow RFN\Pi_{2}(I\Sigma 1+F_{\alpha}\downarrow)=C_{1}^{I\Sigma_{1}+}F\alpha\iota(O)$. Thus Tot$(I\Sigma_{1}+F_{\alpha}\downarrow)=PR(F_{\alpha})$Proof. 2. It suffices to show
by induction on .
by a formalization of a proof of Lemma 7.3.1 in
3.

$n<\omega$. Thus Tot$(I\Sigma_{1}+F_{\alpha}\downarrow$.

$I\Sigma_{1}+F_{\alpha}\downarrow\vdash\forall y\forall x(F_{\alpha}^{(}(x)y)1)$$\forall x(F_{\alpha}^{()}(xy)\downarrow)$for some

. Fix

$y$

as a parameter and use$I\Sigma_{1}$to show$x$$[arrow]$$I\Sigma_{1}$.

$[arrow]$follows from 2.

$\square$Lemma 7.4
I$\Sigma_{1}\vdash C_{1}^{I\Sigma_{1}}(\alpha)rightarrow F_{\omega(1\alpha}+)\downarrow$

Proof.
By the Lemma 7.1.3, it suffices to show $I\Sigma_{1}\vdash Prg[A]$ with. This follows fromthe Lemma 7.3.2.
Put. We show this formula
is reflexively progressive with respect to. Argue inand assume that$[arrow]$$[arrow]$$A(x)\Leftrightarrow_{d}fF_{x}\downarrow\in \mathrm{I}\mathrm{I}_{2}$$B(\alpha)\Leftrightarrow dfF_{\omega(1\alpha}+)\downarrowarrow C_{1}^{I\Sigma_{1}}(\alpha)$$I\Sigma_{1}$$B(\alpha)$$I\Sigma_{1}$$\forall\beta<\alpha Pr_{I\Sigma_{1}}(" B(\dot{\beta}))’$

Case . $\alpha=0$ : By the Lemma 7.3.3,
Case 1.
: Assume$\omega(1+\beta)+\omega\leq\omega(1+\alpha)$
By, we see. Thus$0$)$\ F\omega(1+\alpha)\downarrow$.

$F_{\omega}\downarrowarrow C_{1}^{I\Sigma}.1(0)$$\alpha\neq 0$$\beta<\alpha\ Pr_{I\Sigma_{1}}(" C_{1}^{I\Sigma_{1}}(\beta)arrow A^{)}’)$$RFN_{\Pi_{2}}(I\Sigma_{1}+F_{\omega(\beta)}1+\downarrow)$

Observe thatfor a $A\in\Pi_{2}$ . By a cut,
. Again by the Lemma 7.3.3, we)$F_{\omega()+}1+\beta\omega\downarrow \mathrm{f}\mathrm{r}\mathrm{o}\mathrm{m}F_{\omega(1\alpha}+$$Tr_{\Pi_{2}}(" A’)$$\omega^{1+\alpha}\cdot m=\omega(1+\underline{\omega^{\alpha}\cdot m})$).

”$Pr_{I\Sigma_{1}}(^{)}’ F_{\omega(1+}\beta)\downarrowarrow A$).

$\downarrow$$\mathrm{h}\mathrm{a}\mathrm{v}\mathrm{e}\square$. Therefore from these lemmata and the Theorem 7.1 we see the116
Theorem 7.2 For each$\alpha\geq 0$

and $\mathit{0}<m<\omega$ ,$T_{\alpha}^{(m)}=dfI\Sigma 1+TIR(m)[\omega^{1}, \Pi+\alpha]2=I\Sigma 1+C_{1}^{I\Sigma}1(\underline{\omega m})\alpha.+=I\Sigma_{1}F1+\omega\alpha m\downarrow$andTot $(T_{\alpha}(m))=PR(F_{\omega^{1}m}+\alpha)$
Corollary 7.1 For$\mathit{0}\leq k,$$m<\omega$with$m\neq \mathit{0}$,$T_{k}^{(m)}=_{df}I\Sigma_{1}+TIR^{(m)}[\omega^{1}, \Pi_{2}]+k=I\Sigma_{1}+C_{1}^{I\Sigma_{\}}}(\underline{\omega^{k}\cdot m})=I\Sigma_{1}+F_{\omega^{1+k}m}\downarrow$andTot $(\tau_{k}(m))=PR(F_{\omega^{1+k}m})$

Derivation lengths of finite rewrite rules reducing under lexicographic path orders

8

In this section we discuss a relationship between the derivation lengths of finite rewrite rules reducing under
defined in Corollary 7.1.
lexicographic path orders and the provably total recursive functions in theories
In Weiermann [26] and Buchholz [2] it is shown that$T_{k}^{(m)}$Theorem 8.1 (Weiermann [26] and Buchholz [2])The demvation lengths offinite rewmte rules reducing under a lexicographic path order are bounded by a multiply
recursive function $F_{\omega^{1+k}m}(k, m\in\omega)$ .
First we introduce a variant of a slow growing function
1. $Od,$Deflnition 8.1$(a)P\subset Od$$(b)O\in Od,$

$G_{n}\alpha$in [1].

and $S\alpha\in\{0,1\}$ .

$P$.
$SO=\mathit{0}$.

$[S\alpha=0\Leftrightarrow\alpha<\Omega.]$$(c)\alpha_{1)}\ldots,$ $\alpha_{n}\in P\ \alpha_{1}\geq\cdots\geq\alpha_{n}(n\geq 2)\Rightarrow\alpha_{1}+\cdots+\alpha_{n}\in Od$[Here$\alpha\leq\beta\Leftrightarrow_{df}\alpha<\beta$or$\alpha=\beta.$$S( \alpha_{1}+\cdots+\alpha_{n})=\max\{S\alpha_{i} :1\leq i\leq n\}=S\alpha_{1}$.

$(d)\alpha\in Od|\Omega=_{dj}\{\alpha\in Od:\alpha<\Omega\}\Rightarrow\omega^{\alpha}\in P$.

$(e)\alpha\in Od\Rightarrow d\alpha\in P$$Sd\alpha=\mathit{0}$.

$S\omega^{\alpha}=S\alpha=\mathit{0}$.

$S\Omega^{n}\cdot\xi=1$$K\alpha\subset P|\Omega$$(a)K0=0$$(b)K(\alpha_{1}+\cdots+\alpha_{n})=\cup\{K\alpha i :$(c)K\omega^{\alpha}=K$

1\leq i\leq n\}$a$(d)Kd\alpha=\{d\alpha\}$$(e)K(\Omega^{n}\cdot\xi)=K\xi$3.

$\alpha<\beta$$(a)\beta\neq \mathit{0}\Rightarrow \mathit{0}<\beta$$(b)\alpha_{1}+\cdots+\alpha_{n}<\beta_{1}+\cdots+\beta_{m}$

$i$

$ii$

(

$\alpha_{i},$$\beta_{j}$\in P&n+m. $n<m\forall i<n(\alpha_{i}=\beta_{i})$ or.

$\exists l\leq\min\{n, m\}[\alpha_{1}<\beta_{l} \ \forall i<l(\alpha_{i}=\beta_{i})]$$(c)\alpha\in P|\Omega\Rightarrow\alpha<\Omega^{m}\cdot\zeta$$(d)\alpha<d\beta\Rightarrow\omega^{\alpha}<d\beta$, and$(e)\alpha<\beta(<\Omega)\Rightarrow\omega^{\alpha}<\omega^{\beta}$$(f)d\alpha<d\beta\Leftrightarrow$$i$. \alpha <\beta &K\alpha $<d\beta$ or.

.

$(f)\mathit{0}<n<\omega\ \xi\in P|\Omega=\{\xi\in P : \xi<\Omega\}\Rightarrow\Omega^{n}\cdot\xi\in P$

2.

.

]

$d\alpha\leq\beta\Rightarrow d\alpha<\omega^{\beta}$$>\mathit{2}$)$\Leftrightarrow$

.

117
.

$ii$

$d\alpha\leq K\beta$[X$<\beta\Leftrightarrow_{df}\forall\alpha\in X$(a$<\beta$) and$\alpha\leq \mathrm{Y}\Leftrightarrow_{df}\exists\beta\in \mathrm{Y}(\alpha\leq\beta)$]$(g)\Omega^{n}\cdot\xi<\Omega^{m}\zeta\Leftrightarrow$$\dot{3}$. $n<m$ cr$3i$. n=m&\xi$<\zeta$

4. Conventions$(a)1=\omega^{0},$$n=1+\cdots+1$ for$n<\omega$$\Omega^{0}\cdot\xi=\xi_{f}\Omega^{n}=\Omega^{\alpha}\cdot 1$$(b)\Omega^{n}\cdot \mathit{0}=0,$.

and$\Omega=\Omega^{1}$.

$(c)\Omega^{m}\cdot(\xi_{1}+\cdots+\xi n)=\Omega^{m}\cdot\xi_{\underline{\rceil}}+\cdots+\Omega^{m}\cdot\xi_{n}$for$\Omega>\xi_{1}\geq\cdots\geq\xi_{n},$$(d)\alpha\in P_{\Omega}\Leftrightarrow df$$[$$\xi_{1},$$\ldots,$$\xi_{n}\in P$\alpha <\Omega &\alpha $\in P]$ or [.

$\alpha=\Omega^{n}\cdot\xi\geq\Omega$for some$n,\xi$]denotes the natura sum.

$(e)\alpha\#\beta$$l^{7}$

Deflnition 8.2 Normal Forms
1. We write
if $n\geq 1,$

2. For each$\alpha=_{NF_{0}}\alpha_{1}+\cdots+\alpha_{n}$$\alpha=\alpha_{1}+\cdots+\alpha_{n},$$\alpha\in Od$

with$\alpha_{1}\geq\cdots\geq\alpha_{n}$$\alpha\neq 0,$$\ \forall i\leq n(\alpha_{i}\in P)$$\exists!n<\omega\exists!(\alpha_{0}, \ldots , \alpha_{n})\exists!(\xi_{0}, \ldots , \xi_{n})$such that$\alpha=\Omega^{\alpha_{n}}\cdot\xi_{\mathrm{n}}+\cdots-\vdash\Omega^{\alpha_{0}}\cdot\xi 0\ 0=\alpha 0<\cdots<\alpha n<\omega$$\mathit{0}<\xi_{1}$

..

,

.

, $\xi_{\mathcal{T}i}<\Omega\ \mathit{0}\leq\xi_{0}<\Omega$

In this case we write$\alpha=_{\Omega-NF}\Omega\alpha_{n}.\epsilon_{n}+\cdots+\Omega^{\alpha}0.\xi 0=\Omega-NF\sum i=0n\Omega\alpha.{}^{t}\xi_{i}$3. For each$\alpha\in Od$

with$\alpha\neq 0$,$\exists!n<\omega\exists!m<\omega\exists!(\alpha_{1_{)}}\ldots , \alpha_{n})\exists!(\xi_{1,)}\ldots\xi n)3!(\beta_{1}, .

.

, \beta_{m})$$\alpha=\sum_{1i=}^{n}\Omega^{\alpha}’\cdot\xi i+\sum^{In}i=1\beta i\ 0< \alpha_{n}<,$$\beta_{m}\leq\cdots\leq\beta_{1}$..

such that$<\alpha_{1}$$<w\ O<\xi_{1},$ $\ldots,$ $\xi_{n}<\Omega$<\Omega &\forall i $\leq m(\beta_{i}\in P)\ n+m>0(n,$$m\geq \mathit{0}\grave{)}$In this casc we write$\alpha=_{NF_{1}}\sum_{i=1}^{n}\Omega^{\alpha}\cdot\cdot\xi_{i}+\sum_{i=1}^{m}\beta i=_{NF_{1}}\sum_{i=1}^{n}\gamma i+\sum_{i=1}^{m}\beta i$

Definition 8.3 The norm

$N\alpha$with$\gamma_{i}=\Omega^{\alpha}\cdot\cdot\xi_{i}$of $\alpha\in Od$

1. $N0=0$2.

$N\alpha=\mathrm{n}\mathrm{l}\mathrm{a}\mathrm{x}\{n, N\alpha i :3.

$N\omega^{\alpha}=N\alpha+1$

1\leq i\leq n\}$for.

$\alpha=_{NF_{0}}\alpha_{1}+’\cdot\cdot+\alpha_{n}<\Omega$

4. $Nda=N\alpha+1$
5. $N \alpha=\max(\{k-1\}\cup\{N\xi_{i} : i\leq n\})$ for
Definition 8.4 (cf.

$[\mathit{2}f,$)$[\mathit{2}\mathit{6}\mathit{1}$$\alpha=_{\Omega-NF}\Omega^{\alpha_{n}}\cdot\xi n+\cdots+\Omega^{\alpha_{0}}\cdot\xi_{0}$$\alpha<_{k}\beta$

1.

$\beta\neq 0\Rightarrow 0<_{k}\beta$

2.

$\beta=_{NF_{1}}\beta_{1}+\cdots-\vdash\beta_{m}(\beta i\in P_{\Omega)}m\geq 2)$[zero]:$\exists(\alpha_{1}, \ldots, \alpha_{m})[\alpha=a_{1}\#\cdots\#\alpha m\ \forall i\leq m(\alpha_{i}\leq_{k}\beta_{i})\ \exists i\leq m(\alpha_{i}<_{k}\beta_{i})$$\Rightarrow\alpha<_{k}\beta$[Here$\alpha_{i}$[multiset]

may be3. \beta \in P\Omega &\alpha$0\mathrm{a}\mathrm{n}\mathrm{d}/\mathrm{o}\mathrm{r}\not\in P_{\Omega}$.

$\alpha\leq_{k}\beta\Leftrightarrow df\alpha<_{k}\beta$$=_{NF_{1}}\alpha_{1}+\cdots+\alpha_{n}(\alpha_{i}\in P_{\Omega}, n\geq \mathit{2})$:or$\alpha=\beta.$]with $0<k=\alpha_{n}<\omega$ .

118$(a)S\beta=\mathit{0}:\forall i\leq n(\alpha_{i}<_{k} \beta)\ N\alpha\leq N\beta+k\Rightarrow\alpha<_{k}\beta$$(b)S\beta=1:\forall i\leq n(\alpha_{i}<_{k}\beta)\Rightarrow\alpha<_{k}\beta$

4.
5.

$a$

$\alpha$[inaccessibility][additive principa4, \beta \in P\Omega &O $=S\alpha<S\beta=1\Rightarrow\alpha<_{k}\beta$ [Stufe], \beta \in P\Omega &S\alpha $=S\beta=1\ \alpha$$=_{\Omega-NF}\Omega^{n}\cdot\xi\ \beta=_{\Omega-NF}\Omega^{m}\cdot\zeta$:$(a)n<m$ or$(b)\alpha_{1}=\beta_{1}\ \xi<_{k}\zeta$$\Rightarrow\alpha<_{k}\beta$[lexicographica4[monotonicity]

6.

$\alpha<_{k}\beta<\Omega\Rightarrow\omega^{\alpha}<_{k}\omega^{\beta}$

7.

$da\leq_{k}\beta<\Omega\Rightarrow d\alpha<_{k}\omega^{\beta}$8.

$\alpha<_{k}$9.

d\beta &Nw\alpha[subterm]$\leq Nd\beta+k\Rightarrow\omega^{\alpha}<_{k}d\beta$$(a)\alpha<_{k}$ $\beta\ K\alpha<_{k}$[inaccessibility]d\beta &N\alpha $\leq N\beta+k$ [inaccessibility] or[subterm]$(b)d\alpha\leq_{k}K\beta$$\Rightarrow da<_{k}d\beta$

1.

Lemma 8.1.

$N\alpha i_{\mathit{8}}$a norm, $i.e.$ , the set $\{\beta\in Od : \beta<\alpha\ N\beta \leq n\}$ is finite for each $\alpha\in Od$ and$n\in\omega$

2. The set

is finite for each $a<\Omega$ and$\{\beta\in Od:\beta<_{k}\alpha\}$Definition 8.5$G_{n}\alpha$forFirst we show that the function.

\exists(\alpha_{0}, \ldots, \alpha_{k})[\alpha_{k}<_{n}, .$ $<_{n}\alpha_{0=}\alpha]\}$is provably total in the fragments$G_{n}\alpha$$T_{k}^{(m)}$of$I\Sigma_{2}$.

$(cf.[\mathit{2}f)$1.

$D_{k}=_{dj}\{(a_{0,\ldots,l_{/}^{)}}\alpha\subset Od|\Omega :2.

$W_{k}=_{df}\{\alpha\in Od|\Omega :3.

$A_{k}(x, \alpha)\Leftrightarrow df$

4.

$A_{k}(X)=_{df}\{\alpha\in Od|\Omega :Note that.

$\alpha\in Od|\Omega$$G_{n} \alpha=_{df}\max\{k\in\omega.

Definition 8.6$k\in\omega$\forall j\leq l\forall\alpha<_{k}\alpha_{j}(\alpha\in(\alpha 0, \ldots, \alpha i-1))\}$\exists d\in D_{k}(\alpha\in d)\}$\alpha <\Omega &\forall \beta $<_{k}\alpha(\beta\in X)$ for a unary$X$

A_{k}(X, \alpha)\}$$D_{k},$ $W_{k},$ $M_{k}\in\Sigma_{1}$and $A_{k}(x, \alpha)\in\Sigma_{0(X^{+})}$ . The following lemmata are seen as in [1].

Lemma 8.2 $(W_{k}.1)I\Sigma_{1}\vdash A_{k}(W_{k})=W_{k}$$(W_{k}.2)$ For each,
$F\in\Sigma_{1}\cup\Pi_{1}$$I\Sigma_{1}\vdash A_{k}(F)\subseteq Farrow W_{k}\subseteq F$

and$I\Sigma_{1}\vdash\forall\alpha\in W_{k}(\forall\beta<_{k}\alpha F(\beta)arrow F(\alpha))arrow W_{k}\subseteq F$

Lemma 8.3$(I\Sigma_{1})\alpha,$

Lemma 8.4$(I\Sigma_{1})\beta=_{NF_{0}}\beta_{1}+\cdots+\beta_{n}$Lemma 8.5$(I\Sigma_{1})\alpha\in W_{k}arrow\omega^{\alpha}\in W_{k}$Lemma 8.6 For.

$\beta\in W_{k}rightarrow\alpha\#\theta\in W_{k}$&7$\forall i\leq n(\beta_{i}\in W_{k})arrow\beta\in W_{k}$$\{\alpha_{0}, \ldots, \alpha_{n}, \beta 0, \ldots)\beta_{n}\}\subset Od|\Omega$$\sum_{i=0}^{n}\Omega i$.

.
$\alpha i<_{k}\sum_{i=0}^{n}\Omega|$.

$\beta_{i}$$\Leftrightarrow$$\Leftrightarrow df$,$(\alpha_{n)}$. .,$\alpha_{0})<_{k}^{lex}(\beta_{n)}\ldots, \beta_{0})$[&\forall i(l$\exists l\leq n$$\alpha\iota<_{k}\beta_{l}$$<i\leq narrow\alpha_{i}=\beta_{i})$]119Lemma 8.7 For each$k,$ $m$with$\mathit{0}\leq k$$\tau_{k}^{(m)}\vdash\forall\alpha 0,$$\ldots,$, m<w&m$\neq 0$,$\alpha_{k+}1\in W_{n}\{d(\Omega^{2}+k.

Proof by induction on $m>0$ . Argue in$l_{i}=lh(d_{i})$ . Show theformula

$T_{k}^{(m-1)}$(m-1)+\sum_{i=0}\Omega^{i}\cdot\alpha_{i})1+k\in W_{n}\}$. Assume$d_{0},$$\ldots,$$d_{k}+1\in D_{n},$$d_{i}=(\beta_{0}^{i}, \ldots, \beta_{l1}^{i}-)i$

with$\Sigma_{1}$$B(j \mathrm{o}, \ldots,jk+1)\Leftrightarrow dfd(\Omega 2+k.

(m-1)+\sum_{i=^{0}}^{1}+k\Omega^{i}\cdot\beta_{ji}^{i})\in W_{n}$is progressive with respect to the lexicographic order for $j_{i}<l_{i}(i\leq k+1)$ . Then the rule
implies the assertion.
for
For a proof of the progressiveness use a subsidiary induction on
and the Lemmata 8.4,8.5 and 8.6.

$TIR[\omega^{1+k}, \mathrm{I}\mathrm{I}2]=$$TIR[\omega^{2+}k, \Sigma_{1}]$$\ell\alpha$$\alpha<_{n}d(\Omega^{2+k}\cdot(m-1)+\sum_{i=0j}^{1+k}\Omega i.

\beta i.)\coprod$

Lemma 8.8 For each $l<w_{f}$$T_{k}(m)\vdash\forall\alpha\in Wn(d(\Omega^{2}+k.

m+\Omega l+\alpha)\in W_{n})$Proof by metainduction on $l<\omega$ .

Claim 8.1

$T_{k}^{(m)}\vdash d(\Omega^{2+k}\cdot m)\in W_{n}$.

Proof of the Claim 8.1. By induction on$\ell\alpha$, we show$\alpha<_{n}d(\Omega^{2+k}\cdot m)arrow a\in W_{n}$Cosider the case $\alpha=d\beta<_{n}d(\Omega^{2+k}\cdot m)$ . Then
. This follows from
Lemma 8.7 it suffices to show
Now the lemma follows from the Claim 8.1 and the IH on .

$\beta=\Omega^{2+k}\cdot m’+\sum_{i=0}^{1+}\Omega^{i}\cdot\beta ik$$\{\beta_{0}, \ldots , \beta_{1+k}\}\subset W_{n}$for some $m’<m,$and$\beta_{i}<_{n}d(\Omega^{2+k}\cdot m)$$\beta_{i}<\Omega$$\mathrm{I}\mathrm{H}$. By the.

$\square$$\square$$l$

Now by a metainduction on$\ell\alpha$

we have theLemma 8.9 For each $a<d(\Omega^{2+k}\cdot m+\Omega\omega)$ ,$T_{k}^{(m)}\vdash\alpha\in W_{n}$Next we define the lexicographic path order over a vocabulary having $m$ function symbols of the arity
Let $ar(f)$ denote the arity of the function symbol when the symbol has a fixed arity.

1. A set

.

$f$

$f$

Definition 8.7$\mathit{2}+k$$:F_{k}^{(m)}Q$$\mathcal{F}_{kQ}^{(m)}$of function symbols$\mathcal{F}_{kQ}^{(m)}=_{df}\{list\}\cup\{A_{p} :p<m\}\cup\{fq :q<Q\}$

where list is varyadic, $ar(A_{p})=2+k$ for each $p<m$ and $ar(f_{q})=1$ for
Precedence of these symbols is given by$\mathrm{e}a\mathrm{c}\mathrm{h}q<Q$.

$list<A_{0}<\cdots<A_{m-1}<f0<\cdots<f_{Q-1}$

2.

Applying$\mathrm{t}\mathrm{h}\mathrm{e}\mathrm{s}\mathrm{y}\mathrm{m}\mathrm{b}\mathrm{F}\mathrm{o}\mathrm{r}\mathrm{a}\mathrm{g}\mathrm{i}\mathrm{v}\mathrm{e}_{1}\mathrm{n}_{l}CountableSetVar\mathit{0}fvariableS,Term\mathrm{d}\mathrm{e}\mathrm{n}\mathrm{o}\mathrm{t}\mathrm{e}_{d}\mathrm{s}_{i}\mathrm{t}\mathrm{h}\mathrm{e}se_{C}tofte\Gamma msov_{d}erF^{(}\mathrm{p}\mathrm{o}ist\mathrm{t}\mathrm{o}\mathrm{t}\mathrm{h}\mathrm{e}\mathrm{e}\mathrm{m}\mathrm{t}\mathrm{y}\mathrm{s}\mathrm{e}\mathrm{q}\mathrm{u}\mathrm{e}\mathrm{n}\mathrm{C}\mathrm{e}\mathrm{w}\mathrm{e}\mathrm{P}\mathrm{r}\mathrm{o}\mathrm{d}\mathrm{u}\mathrm{C}\mathrm{e}\mathrm{a}\mathrm{n}invidualonstant0=Jlistk\mathrm{Q}m)_{\cup Vr}().a.$$\mathcal{G}=\mathcal{G}_{kQ}^{(m)}$denotes the set of ground$(=cl_{\mathit{0}Se}d)$terms in Term.

120
Definition 8.8
For sequences
iff

for

$s<_{lp\circ}t$$s,$$t\in Term$ .

$\overline{t}=(t_{0}, \ldots,tn-1),\overline{s}=(s_{0}, \ldots, s_{l1}-)$of terms, let$\ll_{lpo}$

denote the multiset extension$\overline{s}\ll_{lpo}\overline{t}$$\exists\overline{s}0,$$\mathrm{w}\mathrm{h}\mathrm{e}\mathrm{r}\mathrm{e}\approx \mathrm{d}\mathrm{e}\mathrm{n}\mathrm{o}\mathrm{t}\mathrm{e}\mathrm{S}$,$\ldots,\overline{s}_{n}-1[_{\overline{S}}\approx\overline{s}_{0}*\cdots*\overline{s}n-1\ \forall i<n(_{\overline{S}}i\leq_{lpoi}t)\ \exists i<n(\overline{s}_{i}<_{po}tti)]$the permutative congruence, $*concatenati\mathit{0}n$ and$(s_{0}, \ldots, Sl-1)<lpot\Leftrightarrow dj\forall j<l(sj<_{lpo}t)$Put$t\equiv g\overline{t},\overline{t}=(t_{0,\ldots 1},t_{n-})$$s<_{lpo}t$

1.

.

.

if one of the following conditions is fulfilled:$s\leq\iota_{po}t_{i}$for some$t_{i}$.

2.

$s\equiv h\overline{s},\overline{\mathit{8}}=(s_{0}, \ldots, s_{l1}-)$

3.

$s\equiv g\overline{s}$with $h<g:s_{j}<_{lpo}t$ for each$s_{j}$.

:$(a)g=liSt:\overline{s}\ll_{l}po\overline{t}$$(b)g=A_{p}(p<m)$ :$\exists j<l=n=2+k$ [$\forall i<j(s_{i}=t_{i})\ s_{j}<_{lpo}t_{j}$ &\forall i(j $<i<larrow s_{i}<_{lpo}t$ ]$(c)g=f_{q},$ $(q<Q):$$s\mathrm{o}<_{l}tpo0$.

Deflnition 8.9 The norm $|t|$ of a term .
$t$

1. $|v|=0(v\in Var)$

2. $|list(t_{1,\ldots n},t)|= \max(\{n\}\cup\{1+|t_{i}|:1\leq i\leq n\})$3.

$|A_{P}$( $t_{1}+k,$$\ldots,$to) $|= \max(\{1+k,p\}\cup\{|t_{i}|:i<2+k\})+1$

4. $|f_{q}(t)|= \max\{1+k, m, q, |t|\}+1$
Deflnition 8.10 (cf.

) $\pi t\in Od$ for a ground term$[\theta f$

1.

$\pi list(t1, \ldots,tn)=\omega\pi t_{1}\#\ldots\#\omega^{\pi}t_{n}$2.

$\pi A_{p}(t_{1+k}, \ldots, t_{0})=d(\Omega^{2+k}\cdot p+\sum_{i=0}^{1+}\Omega^{i}\cdot\pi kti)$$t\in \mathcal{G}$

3. $\pi f_{q}(t)=d(\Omega^{2}+k. m+\Omega\cdot q+\pi t)$
Deflnition 8.11 (Buchholz [2]) $s<_{k}t$Put$t\equiv g\overline{t},\overline{t}=(t_{0))}\ldots t_{n-1})$$s<_{k}t$.

if one of the following conditions is fulfilled:1.

$s\leq_{k}t_{i}$2.

$s\equiv h\overline{s},\overline{s}=(s_{0}, \ldots, s_{l1}-)$$s_{j}<_{k}t$3.

$s\equiv g\overline{s}$for some
for each$t_{i}$$s_{j}$.

with $h<g$ :and $|s|\leq|t|+k$ .

:$(a)g=list:\overline{s}\ll_{k}\overline{t}$with the multiset$\mathrm{e}\mathrm{x}\mathrm{t}\mathrm{e}\mathrm{n}\mathrm{S}\mathrm{i}\mathrm{o}\mathrm{n}\ll_{k}$of$<_{k}$

and $|s|\leq|t|+k$ .

$(b)g=A_{p}(p<m)$ :$\exists j<l=n=2+k$ [$\forall i<j(s_{i}=t_{i})\ s_{j}<_{k}t_{j}$ &\forall i(j $<i<larrow s_{i}<_{k}t$]and$|s|\leq|t|+k$ .

$(c)g=f_{q},$ $(q<Q):s_{0}<_{k}t_{0}$ and $|s|\leq|t|+k.$ .

Lemma 8.10

1. $s<_{lpo}tarrow|s\sigma|\leq|t\sigma|+|s|$ for any substitution

2. $s<_{lpo}tarrow s\sigma<|s|t\sigma$ for any substitution .
$\sigma$$\sigma$.

$of<\iota_{po}$

121
3.

$Ifa(l,r)\in finit\mathcal{R}\}eerw\mathrm{N}te$rule$\mathcal{R}=\{(l, r)\}$4. $|t|=N\pi t$ for any ground term.
5.
for$s<_{k}tarrow\pi \mathit{8}<_{k}\pi t$

over$t\in \mathcal{G}$$Dh_{\mathcal{R}}$$dh_{\mathcal{R}}(:)$$=_{df}$$Dh_{\mathcal{R}}(n)$with $n= \max\{|r|$ :$t\in \mathcal{G}$$\max\{l\in\omega :.

such that$.’(m)\succ_{kQ}$is reducing under$\mathcal{R}$$<\dagger p\circ\cdot$

The derivation\exists(t_{0}, \ldots , t_{l})[t\equiv t_{l}arrow R\ldotsarrow_{\mathcal{R}}t_{0}]\}$$\mathrm{m}\mathrm{a}\mathrm{x}\mathrm{f}^{dh_{\Gamma\backslash }}(t).|\dot{\tau}|\leq n\}$$=_{d\dot{J}}$Lemma 8.11 The derivation lengih$i.e.$$thenarrow \mathcal{R}\subseteq<_{n}$$s,t\in \mathcal{G}$be a finite rewrite rule overis defined by$\prime \mathcal{R}=\{(l, r)\}$$<_{lp\circ},$.

6. $|t|\leq larrow\pi t<_{l}d(\Omega^{2+k}\cdot m+\Omega\cdot Q)$ forLetlength function

is reducing under$F_{kQ}^{(m)}$$\mathrm{f}_{\dot{u}nC}ntionDh_{\mathcal{R}}(n)$is majorized by the function $G_{n}(d(\Omega^{2+}k. m+\Omega\cdot Q))$ ,,$\exists n_{0}\forall n\geq n_{0}\check{\lfloor}Dh_{\mathcal{R}}(n)\leq G_{n}(d(\Omega 2+k.

m+\Omega\cdot Q))]$and $|t|\leq n$ , then. Ifdepending on 7? so that
Proof. By Lemma 8.10 pick an$\pi t<_{n}d(\Omega^{2+k}\cdot m+\Omega\cdot Q)$ . Thus $dh_{\mathcal{R}}(t)<G_{n}(d(\Omega^{2+}k. m+\Omega\cdot Q))$ by.
again,
Lemma 8.10
$dh_{\mathcal{R}}(t)\leq G_{n_{0}}(\pi t)$$n_{0}$$n\geq n_{0}$$\mathrm{b}\mathrm{y}\square$$<_{n_{\mathrm{O}}}\subseteq<_{n}$Next we show that the computation of a multiply recursive function
can be regarded as a derivation in a finite rewrite rule. We learnt this view from Hofbauer [13].
and list $(t)$ otherwise.
if
For a term let . denote the term list!@ the $m_{v}^{t}hnum$ eral. Observe that $|O^{(m)}|=\pi \mathit{0}^{(m)}=m$ .
ation.
fcliowmg$F_{\omega^{1+k}m}$$(k, m\in\omega)$$\acute{\tau}$$(\mathrm{O}, t1, \ldots, t_{n})$$S+$$l\equiv list(t_{\mathrm{i}}, \ldots, t_{n})$$S\cdots S\mathrm{i}\}=l_{\dot{l}}.\mathrm{q}t(\mathrm{o}, , 0)$$\mathrm{c}\mathrm{o}\mathrm{n}\mathrm{S}\mathrm{i}\mathrm{d}\mathrm{e}\mathrm{r}^{+}‘ J\mathrm{h}\mathrm{e}$$\mathrm{i}\mathrm{n}\mathrm{t}_{8}\mathrm{r}\mathrm{p}\mathrm{r}\mathrm{e}0$$O:=iist(\backslash ,;\perp 1:=S;F_{\alpha}(x\mathrm{o}):=A_{p}(x_{1k}+, \ldots, x_{1}, x\mathrm{o})$with $\alpha=\omega^{1+k}\cdot p+\sum_{i=0}^{k}w^{i}\cdot xi+1\mathit{0}\leq p<m$ and$x^{\Gamma}+\omega’ km+(1+q)=f_{q}(q<Q)$,$\mathscr{L}\}e\mathrm{f}\mathrm{i}\mathrm{n}\mathrm{i}\mathrm{t}\mathrm{i}_{9}\mathfrak{W}8.12G;_{\mathrm{v}}7\beta.\overline{j}\backslash ’$

1.

rczyk-Ackermann Rewri 3 Ruie$e$$\mathcal{R}_{Q}$for$F_{\alpha},$$\alpha\leq\omega^{1+k}\cdot m+Q$

$F_{\alpha}(0_{)}^{\backslash }=2$$(a\dot{\text{ノ}})\lrcorner*(’\overline{x}, 0)arrow 2=S_{\sim}^{\sigma}’;..\backslash |$$(b)f_{\mathit{0}}(0)arrow 2$2.

$F_{\omega p}1+k+\alpha+x_{1}+1(’X0+1)=A_{p}(\overline{X}_{)}s_{X_{1}}, sX_{0})\text{ノ}arrow$$A_{p}(\overline{x}_{i}X_{1,p}A(\overline{X}, SX_{1}, x0))=F_{\omega^{1+k}px_{1}}+\alpha+(F_{\omega^{1+k}p}1(+\alpha+x_{1}+X\mathrm{o}))$

with

.

$a= \sum_{\wedge=}^{k}..1\omega^{:}\cdot Xi+1$

3.

$f_{g}(sX_{\text{ノ}^{}\backslash }\mathrm{t}arrow f_{q-1}(f_{q}(X))\backslash$4.

$F_{\omega^{1+k}m+}1(X_{0}+1)=f0(^{-}‘’ x_{0}1arrow A_{m-1}(Sf\mathrm{o}(x0\grave{)},\overline{\mathrm{C}}, f_{0}(x0))$$=F_{\omega^{1+k}}(mF1\neq k_{\mathrm{n}},*1(\omega\prime d\prime 0))$5.

$F_{\omega^{1+k}p}(x0+1_{\mathit{1}}^{\backslash }=A_{p}(\overline{O}, Sx0\grave{)}arrow A_{p-1}(sSX_{0, )} \text{\={o}} sX_{0})$$=F1+k-1_{\text{ノ}})\omega(p+\omega k(x_{0}+2)(x0+3_{1}\backslash \mathrm{t}n-’\backslash \mathit{3}^{-\neq\{};)$

6.

$F_{\omega^{1+k}p+}\mathrm{o}+\omega(ix_{+}.1+1)(X0+1)=A_{p}(\overline{x}, Sx_{i1}+,\overline{O}, SX0)arrow$$A_{P}(\overline{X}_{)}xi+1, SsX0,\overline{O}, Sx_{0})=F_{\omega^{1+\cdot 1}}k+\alpha+\omega\cdot x.+1+\omega\vee^{-}(x\mathrm{o}+2)(\mathcal{P}-x_{0\vdash}1)$$(i\neq \mathit{0})$

with

7.

.

$\alpha=\sum_{j=i+2}^{1k}+i-1$$x_{j}\omega$$F_{0}(x0+1)=A_{0}(\overline{O}, sx\mathrm{o})arrow SSA\mathrm{o}(\overline{O}, x\mathrm{o})=F_{0}(X_{0})+2$

Definition 8.13
2. For each1.

$t\in N\mathcal{G},$$(a)no(0)=\mathit{0}$$N\mathcal{G}$denotes the set of ground terms over$no(t)\in\omega$is defined by$0,$ $S,$ $A_{p},$$f_{q}$.

$\mathit{0}^{(m)}=$122$(b)no(st)=no(t)+1$$(c)no(A_{p}(t_{1+k}, \ldots,t1,t\mathrm{o}))=no(f_{q}(t\mathrm{o}))=no(t_{0})$1. The Grzegorczyk-Ackermann rewrite ruleLemma 8.12

2. For eachand each substitution$(l.r)\in \mathcal{R}_{Q}$$\sigma$with$l\sigma,$$\mathcal{R}_{Q}$is reducing under$r\sigma\in N\mathcal{G}$$<_{lp\circ}$.

,

no $(r\sigma)\leq no(l\sigma)+2$

3.

is terminating. Let denote the unique normal form of
no denotes the value of the ground term .
$t\sim$$\mathcal{R}_{Q}$4. For$t\in N\mathcal{G}$. Then$t^{\sim}is$a numeral and $val(t)=_{df}$$t$$(t^{\sim})$$t\in N\mathcal{G}$,$val(t)\leq no(t)+2dh_{\mathcal{R}_{\mathrm{Q}}}(t)$

Let

over

$Dh(<_{l}, \mathcal{F}^{()})pokqm$$F_{kq}^{(m)}$denote the set of derivation lengths functions

which is reducing under$<\iota_{p\mathrm{o}}$$Dh_{\mathcal{R}}$such that 71 is a finite rewrite rule.

Lemma 8.13 For each $q<w$

1.

$F_{\omega^{1+k}m}+q$

is elementary recursive in2.

$F_{\omega^{1+k}m+q}$

is majorized by the function $G_{n}(d\eta_{km}q)$ with

$Dh_{\mathcal{R}_{q}},$.

$\Omega^{2+k}\cdot(m-1)+\Omega^{1+k}\cdot\omega$$q=\mathit{0}$$\Omega^{2+k}\cdot m+\Omega\cdot q+\omega$otherwise$\eta_{kmq}=_{df}\{$

Proof. Casel$q=\mathit{0}:\mathrm{W}\mathrm{e}$have, by the Lemma 8.12

$F_{\omega^{1}+k}m(n)$1. For some constant$2Dh_{\mathcal{R}_{0}}(n+c)$

$c$

$=$

$F_{\omega^{1+k}(m}-1)+\omega^{k}(n+1)(n)$$=$$val(A_{m-1}(O^{(}n+1),\overline{0}, 0^{(}n)))\leq n+2dh_{\mathcal{R}_{0}}(A_{m-}1(0(n+1),\overline{0}, 0^{(}n)))$depending on $m,$$k,$$|A_{m-1}(0(n+1),\overline{0}, 0^{(n}))|\leq n+c$

Thus $F_{\omega^{1+k}m}(n)\leq n+$.

.

2. By the Lemma 8.10 there exists an$n_{0}$

such that for any $n\geq n_{0}$ ,$dh_{\mathcal{R}_{0}}(A_{m-1}(O^{(}n+1), \text{\={o}} \mathrm{o}(n))))\leq G_{n}a_{n}$with$\alpha_{n}=\pi(A_{m-1(\mathrm{o},\overline{0}}(n+1), \mathrm{o}^{(}n)))=d(\Omega^{2+k}\cdot(m-1)+\Omega^{1+k}\cdot(n+1)+n)$.

We show the following Claim which yields $\forall n\geq n_{0}[F(\omega^{1+k}mn)\leq G_{n}d\eta_{km}0]$ :Claim 8.2 $n+2G_{n}\alpha_{n}<G_{n}d\eta_{km0}$$\}$

Proof of the Claim 8.2. We have, by $n+1<_{n}\omega$ and $Nd\eta_{km0}\geq 2$$n\#\alpha_{n}\cdot 2<_{n}d(\Omega^{2+k}\cdot(m-1)+\Omega^{1+k}\cdot w)=d\eta_{km0}$ . Also, in general, we have
From these we see the Claim.
Case2$q\neq \mathit{0}$.

$G_{n}\alpha+G_{n}\beta\leq G_{n}(\alpha\neq\beta)\square$: We have$F_{\omega^{1+k}m+(q}1+)(n)=val(f_{q}(0^{(}n)))\leq n+2dh_{\mathcal{R}_{1+q}}(fq(\mathrm{o}(n)))$1. For a constant$c$depending on $m,$

2. As in the Case 1, there exists an$k,$ $q,$$n_{0}$$|f_{q}(O^{(n)})|\leq n+c$

such that for any$dh_{\mathcal{R}_{1+q}}(f_{q}(\mathrm{o}^{()}n))\leq G_{n}\alpha_{n}$We have.

.

$n\geq n_{0}$,with $\alpha_{n}=\pi f_{q}(0^{()}n)=d(\Omega^{2+k}\cdot m+\Omega\cdot q+n)$ .

$n\#\alpha_{n}\cdot 2<_{n}d(\Omega^{2+k}\cdot m+\Omega\cdot q+\omega)=d\eta_{kmq}$. Thus for any $n\geq n_{0}F_{\omega^{1+k}m+(}1+q$ ) $(n)<G_{n}d\eta kmq$ .
口123
Theorem 8.2 For each$k,$ $m$with $0\leq k<\omega,$ $\mathit{0}<m<\omega$ ,$T_{k}^{(m)}=I\Sigma_{1}+TIR^{()}m[w, \mathrm{I}1+k\mathrm{I}2]=I\Sigma_{1}+C_{1}(I\Sigma_{1}\underline{wk.m})=I\Sigma 1+F_{\omega^{1+k}m}\downarrow$andTot $(\tau^{(m}))k=$$PR(F_{\omega^{1}m}+k)=ER(\{F\omega^{1}+km+q :q<\omega\})=$$PR(Dh(<\iota p\circ’ \mathcal{F}_{k}(m)0))=ER(\{Dh(<lpo’ \mathcal{F}_{kq})(m) :$PR(G_{n}(d(\Omega 2+k.

Also these$classe\mathit{8}$q<\omega\})=$(m-1)+\Omega 1+k.\omega)))=ER(\{Gn(d(\Omega 2+k.\Omega m+\cdot q)):q<\omega\})$offunctions are majorized by any one of the functions$F_{\omega^{1+k}}m+\omega$and$G_{n}(d(\Omega^{2+k}\cdot m+\Omega\cdot w))$.

Acknowledgements I would like to thank Wilfried Buchholz and Andreas Weiermann for giving me theirpreprints $[2])[3]$ and [26].

References[1] T. Arai, Variations on a theme by Weiermann, to appear in J. Symb. Logic.
[2] W. Buchholz, Proof-theoretic analysis of termination proofs, Ann. Pure Appl. Logic 75 (1995) 57-65[3] W. Buchholz, An Intuitionistic fixed point theory, submitted[4] W. Buchholz, S. Feferman, W. Pohlers and W. Sieg, Iterated Inductive Definitions and Subsystems of
Proof-Theoretical Studies. Lecture Notes in Mathematics 897 (Springer, Berlin Heidelberg
New York, 1981).
$\mathrm{A}\mathrm{n}\mathrm{a}\mathrm{l}\mathrm{y}_{\mathrm{S}}\mathrm{i}\mathrm{s}:\mathrm{R}\mathrm{e}\mathrm{C}\mathrm{e}\mathrm{n}\mathrm{t}$[5] S. Buss, Bounded Arithmetic (Bibliopolis, Napoli, 1986).
[6] E. A. Chichon, Termination orderings and complexity characterizations, in: P. Aczel et al. eds., Proof
Theory, Cambridge University Press, Cambridge, 1993, 171-193.
[7] N. Dershowitz and J.-P. Jouannaud, Rewite Systems, in: J. van Leeuwen, ed., Handbook of TheoreticalComputer Science, vol. B (North-Holland, Amsterdam, 1990) 243-320[8] S. Feferman, Iterated inductive fixed-point
to Hancock’s conjecture, in:G. Metakides,
ed., Patras Logic Symposion (North-Holland, Amsterdam, 1982) 171-196$\mathrm{t}\mathrm{h}\mathrm{e}\mathrm{o}\Gamma \mathrm{i}\mathrm{e}\mathrm{S}:\mathrm{A}\mathrm{P}\mathrm{p}\mathrm{l}\mathrm{i}\mathrm{c}\mathrm{a}\mathrm{t}\mathrm{i}_{0}\mathrm{n}\mathrm{S}$[9] H. Friedman, Provably equality in primitive recursive arithmetic with and without induction, Pac. J.
Math. 57 (1975) 379-392[10] H. Friedman and M. Sheard, Elementary descent recursion and proof theory, Ann. Pure Appl. Logic 71(1995) 1-45
[11] J.-Y. Girard, Proof Theory and Logical Complexity.vol1 (Bibliopolis, Napoli, 1987)[12] N. Goodman, Relativized realizability in intuitionistic arithmetic of all finite types, J. Symb. Logic 43(1978) 23-44[13] D. Hofbauer, Termination proofs by multiset path orderings imply primitive recursive derivation lengths.
Proc. 2nd. ALP, Lecture Notes in Computer Science, Vol. 463, Springer (1990), 347-358.
[14] W. A. Howard and G. Kreisel, Transfinite induction and bar induction of type zero and one, and the roleof continuity in intuitionistic analysis, J. Symb. Logic 31 (1966) 325-358[15] J. Hudelmaier, Bounds for cut elimination in intuitionistic propositional logic, Arch. Math. Logic 31 (1992)

331-353[16] G. J\"ager and B. Primo, About the proof-theoretic ordinals of weak fixed point theories, J. Symb. Logic
57 (1992) 1108-1119[17] G. Kreisel, The status of the first(abstract)$\epsilon$-number in first order arithmetic, J. Symb. Logic 25 (1960) 390

124[18] G.E. Mints, Finite investigations of transfinite derivations, in: Selected Papers in Proof Theory (Bibliopolis, Napoli, 1992) 17-72.
[19] U. Schmerl, A fine structure generated by reflection formulas over primitive recursive arithmetic, in:M.
Boffa et al., eds., Logic Colloquium 78 (North-Holland , Amsterdam, 1979) 335-350[20] H. Schwichtenberg, Proof theory:Some applications of cut-elimination, in:J. Barwise, ed., Handbook ofMathematical Logic (North-Holland , Amsterdam, 1977) 867-897[21] J. C. Shepherdson, Non-standard models for fragments of number theory, in: J. W. Addison et al., eds.,
The Theory of Models. (North-Holland, Amsterdam, 1965) 342-358

transfinite induction, in:D. van Dalen, et al., eds., Logic Colloquium 80 (Northand[22] S. G. Simpson,
Holland, Amsterdam, 1982) 239-253$\Sigma_{1}^{1}$[23] R. Sommer,$r_{\mathrm{b}\mathrm{n}\mathrm{S}}\mathrm{f}\mathrm{i}\mathrm{n}\mathrm{i}\mathrm{t}\mathrm{e}$$\Pi_{1}^{1}$

inducton within Peano arithmetic, Ann. Pure Appl. Logic 76 (1995) 231-289[24] G. Takeuti, Proof Theory, second edition (North-Holland, Amsterdam, 1987)[25] A.S. Troelstra and D. van Dalen, Constructivism in Mathematics An Introduction vol.1 (North-Holland,
Amsterdam, 1988)[26] A. Weiermann, Termination proofs by lexicographic path orderings imply multiply recursive derivation
lengths, Theor. Comput. Sci. 139 (1995) 355-362