# Proofs that Modify Proofs
Work in Progress

Henry Towsner  Department of Mathematics, University of Pennsylvania, 209
South 33rd Street, Philadelphia, PA 19104-6395, USA<EMAIL_ADDRESS>http://www.math.upenn.edu/~htowsner

###### Abstract.

In this paper we give an ordinal analysis of the theory of second order
arithmetic. We do this by working with proof trees—that is, “deductions” which
may not be well-founded. Working in a suitable theory, we are able to
represent functions on proof trees as yet further proof trees satisfying a
suitable analog of well-foundedness. Iterating this process allows us to
represent higher order functions as well: since functions on proof trees are
just proof trees themselves, these functions can easily be extended to act on
proof trees which are themselves understood as functions. The corresponding
system of ordinals parallels this, using higher order collapsing function.

Partially supported by NSF grant DMS-2054379

##  1\. Introduction

In this paper, we give an ordinal analysis of second-order arithmetic.111The
current draft represents an in-progress version of this work. The ordinal
analysis is currently incomplete: we give a “qualitative” ordinal analysis,
working in a strong theory and proving the existence of certain ordinal bounds
without calculating them explicitly. A future version of this paper will
include an explicit ordinal notation system. In addition, certain proofs are
currently only sketched and a great deal of exposition is missing. We follow
the conventional approach in infinitary ordinal analysis as introduced in [12]
(see, for instance, [9] for a modern exposition): we begin with a finitary
proof in second-order arithmetic, transfer it to a proof in an infinitary
system, and show that we can transform any such proof into a cut-free proof,
and further that there can be no cut-free proof of $0=1$. This allows us to
conclude that second-order arithmetic.

Such a proof can, of course, only be given in a sufficiently strong system.
This strength appears in our proof through the use of ordinal bounds: what we
show is that our infinitary system has a cut-free proof with a certain kind of
ordinal bounds. We then use the well-foundedness of the system of ordinal
bounds to conclude that there is no such proof of $0=1$. The goal of ordinal
analysis is, roughly, to calibrate the strength of the theory by identifying
the ordinal needed to carry out such a proof [10, 11, 3].

An ordinal analysis of second-order arithmetic, using more purely finitary
techniques, was also recently announced by Arai [2]. Our approach here was
developed independently and uses rather different methods.

The main challenge is how to deal with second-order quantifiers. Buchholz’s
$\Omega$ rule [4, 5] gives an approach to eliminating cuts between a
$\Pi^{1}_{1}$ and $\Sigma^{1}_{1}$ statement. In this approach, the way we
prove222As is customary, we use a one-sided sequent calculus, so by a proof of
a finite set of formulas, we mean a proof that at least one of these formulas
holds. $\exists^{2}X\,phi(X),\Sigma$ is to give a function which transforms a
proof of $\neg\phi(X),\Delta$ (with suitable restrictions) into a proof of
$\Delta\Sigma$.

A proof of $\exists^{2}X\,\phi(X),\Sigma$ in a finitary system might derive
this from some $\phi(A),\Sigma$. Suppose we have already, inductively,
translated the proof of $\phi(A),\Sigma$ into our infinitary system. Then we
could hope to produce such a function by taking a proof of
$\neg\phi(X),\Delta$, replacing $X$ with $A$ everywhere, and then using the
Cut rule to combine our proof of $\phi(A),\Sigma$ with our proof of
$\neg\phi(A),\Delta$.

To generalize this to a $\Sigma^{1}_{2}$ formula, however, we face a new
difficulty: we would like a proof of
$\exists^{2}X\forall^{2}Y\,\phi(X,Y),\Sigma$ to be a function which acts on
proofs of $\exists^{2}Y\,\neg\phi(X,Y),\Delta$. When we try to produce such a
function, however, we want to be able to convert a proof of
$\exists^{2}Y\,\neg\phi(X,Y),\Delta$ into a proof of
$\exists^{2}Y\,\neg\phi(A,Y),\Delta$. It is not immediately clear how to do
this: we are given a function whose domain is proofs of
$\phi(X,Y),\Delta^{\prime}$, but we need to produce a function whose domain is
proofs of $\phi(A,Y),\Delta^{\prime}$.

Our solution is to use the fact that the functions we need are not arbitrary
functions. The premises of the Buchholz $\Omega$ are, essentially, the _graph_
of the function we are using. Here, we use a modified $\Omega$ rule, which we
call the $\Omega^{\flat}$ rule, which takes as its premise a certain
description of the algorithm being used. In particular, these algorithms are
always “continuous” [8], in the sense that the bottom part of the output is
determined by the bottom part of the input.

The crucial insight is that these algorithms can be seen as proof-trees (that
is, potentially ill-founded proofs): we have nodes in our tree (that is, we
have a special inference rule) where we can look at a position in the input
deduction, and the branches of our tree (that is, the premises of this
inference rule) are the possible rules that the input deduction could have at
that position.

Such a proof-tree is not well-founded; the right property to ask for is that
it transforms well-founded proofs to well-founded proofs. This is represented
by assigning a kind of higher-order ordinal bound to the tree.333Although we
do not explore this here, we expect that these higher-order ordinal bounds are
essentially dilators[6].

So a proof of $\exists^{2}Y\,\neg\phi(X,Y),\Delta$ in our infinitary proof
system will be an _ill-founded proof-tree_ which describes the process by
which a proof of $\phi(X,Y),\Delta^{\prime}$ is transformed into a proof of
$\Delta^{\prime}\Delta$. We are then able to transform this proof-tree into a
proof of $\exists^{2}Y\,\neg\phi(A,Y),\Delta$, which is precisely what we need
to do.

Because we are representing our functions on proof-trees by new proof-trees,
we can simply iterate this idea. Along the way, we need more and more
complicated ordinal bounds—bounds which guarantee that we transform higher-
order ordinal bounds into higher-order ordinal bounds, and so on.444Again, we
expect a fundamental connection to the Girard’s ptykes [7] which is not
explored here.

##  2\. Second Order Arithmetic

###  2.1. Language

Our ultimate interest is the theory of second order arithmetic, which is in
the language $\mathcal{L}_{2}$. We take this language to be defined as
follows.

######  Definition 2.1.

The symbols of $\mathcal{L}_{2}$ consist of:

  * •

an infinite set $Var=\\{x,y,z,\ldots\\}$ for first-order variables,

  * •

a constant symbol $0$,

  * •

a unary function symbol $\mathrm{S}$,

  * •

for every $n$-ary primitive recursive relation $R$, an $n$-ary predicate
symbol $\dot{R}$,

  * •

an infinite set $Var_{2}=\\{X,Y,Z,\ldots\\}$ for second-order variables,

  * •

the unary connective $\neg$,

  * •

two binary connectives, $\wedge$ and $\vee$,

  * •

two first-order quantifiers, $\forall$ and $\exists$,

  * •

two second-order quantifiers $\forall^{2}$ and $\exists^{2}$,

where all symbols are distinct.

The terms are given by:

  * •

Each first-order variable is a term,

  * •

$0$ is a term,

  * •

if $t$ is a term, $St$ is a term.

The atomic formulas are defined by:

  * •

whenever $\dot{R}$ is a symbol for an $n$-ary primitive recursive relation and
$t_{1},\ldots,t_{n}$ are terms, there is an atomic formula $\dot{R}t_{1}\cdots
t_{n}$,

  * •

whenever $X$ is a second order variable and $t$ is a term, $Xt$ is a atomic
formula.

We define formulas as follows:

  * •

whenever $\eta$ is an atomic formula, $\eta$ and $\neg\eta$ are formulas,
which we call _literals_ ,

  * •

whenever $\phi$ and $\psi$ are formulas, $\phi\wedge\psi$ and $\phi\vee\psi$
are formulas,

  * •

whenever $\phi$ is a formula and $x$ is a first-order variable, $\forall
x\,\phi$ and $\exists x\,\phi$ are formulas,

  * •

whenever $\phi$ is a formula and $X$ is a second-order variable,
$\forall^{2}X\,\phi$ and $\exists^{2}X\,\phi$ are formulas.

######  Definition 2.2.

We define the negation of a formula, ${\sim}\phi$, inductively by:

  * •

if $\sigma$ is an atomic formula, ${\sim}\sigma$ is $\neg\sigma$ and
${\sim}\neg\sigma$ is $\sigma$,

  * •

${\sim}(\phi\wedge\psi)$ is $({\sim}\phi)\vee({\sim}\psi)$,

  * •

${\sim}(\phi\vee\psi)$ is $({\sim}\phi)\wedge({\sim}\psi)$,

  * •

${\sim}\forall x\,\phi$ is $\exists x\,{\sim}\phi$,

  * •

${\sim}\exists x\,\phi$ is $\forall x\,{\sim}\phi$,

  * •

${\sim}\forall^{2}X\,\phi$ is $\exists^{2}X\,{\sim}\phi$,

  * •

${\sim}\exists^{2}X\,\phi$ is $\forall^{2}X\,{\sim}\phi$.

###  2.2. Inference Rules

######  Definition 2.3.

A _sequent_ is a set of formulas.

This definition, together with our choices below, builds the usual structural
rules (contraction, weakening, and exchange) into the definition of a
deduction.

######  Definition 2.4.

An _inference rule_ is a tuple
$\mathcal{R}=(I,\Delta,\\{\Delta_{\iota}\\}_{\iota\in
I},\\{E_{\iota}\\}_{\iota\in I})$ where $I$ is a set, $\Delta$ is a sequent,
$\\{\Delta_{\iota}\\}_{\iota\in I}$ is a set of sequents indexed by $I$, and
each $E_{\iota}$ is a subset of $Var\cup Var_{2}$.

We usually write inference rules using the notation

$\cdots$ $\Delta_{\iota}$ $\cdots\ (\iota\in I)$ $\mathcal{R}$
$!\\{E_{\iota}\\}!$ $\Delta$

When $|I|=1$, we simply write $!E!$ on the right hand side. When $|E|=1$, we
write $!x!$ or $!X!$ in place of $!\\{x\\}!$ or $!\\{X\\}!$, respectively.
When $E=\emptyset$, we omit the right-hand label entirely.

The label $\mathcal{R}$ is the name of the inference rule, the set $I$ is the
_premises of $\mathcal{R}$_, the sequent $\Delta$ is the _conclusion sequent_
, the sequent $\Delta_{\iota}$ is the _premise sequent at $\iota$_, and the
sets $E_{\iota}$ are the _eigenvariables_. When $\mathcal{R}$ is an inference
rule, we write $|\mathcal{R}|$ for its premises and $\Delta(\mathcal{R})$,
$\Delta_{\iota}(\mathcal{R})$ for the corresponding sequents. We write
$Eig_{\iota}(\mathcal{R})$ for the set of eigenvariables, again omitting
$\iota$ when $|I|=1$.

It is our assumption that the sets $I$, across all rules ever considered, are
disjoint—that is, given $\iota\in|\mathcal{R}|$, we can recover the rule
$\mathcal{R}$ from $\iota$, and we denote it $\mathcal{R}(\iota)$. We will
often equivocate notationally, writing rules whose sets of premises are
$\mathbb{N}$, $\\{L,R\\}$, or $\\{\top\\}$. We always take it as given that
the set of premises is _really_ some set of pairs from
$\\{t\\}\times\mathbb{N}$ or $\\{t\\}\times\\{L,R\\}$ or the like, where $t$
is a label for the rule.

For reasons that will become clear, our perspective on deductions emphasizes,
not that they are built from axioms in a well-founded way, but that they are
“read” from the root up. In particular, our basic object is a _proof-tree_ ,
the co-well-founded analog of a deduction.

######  Definition 2.5.

A _theory_ is a set of inference rules.

When $\mathfrak{T}$ is a theory, a _proof-tree in $\mathfrak{T}$_ is a
function $d$ where:

  * •

the range of $d$ is $\mathcal{T}$,

  * •

$\langle\rangle\in\operatorname{dom}(d)$,

  * •

if $\sigma\in\operatorname{dom}(d)$ and $\iota\in|d(\sigma)|$ then
$\sigma\iota\in\operatorname{dom}(d)$.

For any $\sigma\in\operatorname{dom}(d)$, we define $\Gamma(d,\sigma)$ to be
the set of $\phi$ such that there is some $\tau$ with
$\sigma\tau\in\operatorname{dom}(d)$, $\phi\in\Delta(d(\sigma\tau))$, and for
all $\tau^{\prime}\iota\sqsubseteq\tau$,
$\phi\not\in\Delta_{\iota}(d(\sigma\tau^{\prime}))$. We write $\Gamma(d)$ for
$\Gamma(d,\langle\rangle)$.

As usual, $\Gamma(d)$ is called the _conclusion_ of $d$.

######  Definition 2.6.

When $d$ is a proof-tree and $\sigma\in\operatorname{dom}(d)$, we write
$d_{\sigma}$ for the _sub-tree_ given by $d_{\sigma}(\tau)=d(\sigma\tau)$.

It is sometimes natural to consider some $\sigma$ which could be in the domain
of a deduction without referring to the specific deduction it comes from.

######  Definition 2.7.

When $\mathfrak{T}$ is a theory, a $\mathfrak{T}$-sequence is a finite
sequence $\sigma$ such that each element of $\sigma$ is some $\iota$ with
$\mathcal{R}(\iota)\in\mathfrak{T}$. We define
$\Delta(\langle\rangle)=\emptyset$ and
$\Delta(\sigma\iota)=\Delta_{\iota}(\mathcal{R}(\iota))$.

When $\sigma$ is a $\mathfrak{T}$-sequence, we define
$\Gamma^{\leftarrow}(\sigma)$ inductively by
$\Gamma^{\leftarrow}(\langle\rangle)=\emptyset$ and
$\Gamma^{\leftarrow}(\sigma\iota)=(\Gamma^{\leftarrow}(\langle\rangle)\setminus\Delta(\mathcal{R}(\iota)))\cup\Delta_{\iota}(\mathcal{R}(\iota))$.

We may think of $\Gamma^{\leftarrow}(\sigma)$ as representing the “formulas
permitted at the top of $\sigma$”: if $\sigma\in\operatorname{dom}(d)$ then
$\Gamma(d,\sigma)\subseteq\Gamma(d,\langle\rangle)\cup\Gamma^{\leftarrow}(\sigma)$.
(It is calculated, of course, by following the rules for calculating the
conclusion “backwards”.)

######  Definition 2.8.

A proof-tree $d$ is _valid_ if, for every $\sigma\in\operatorname{dom}(d)$ and
every $\iota\in|d(\sigma)$, no element of $Eig_{\iota}(d(\sigma))$ appears
free in any formula in $\Gamma(d,\sigma\iota)$.

Throughout this paper, all proof-trees will be assumed to be valid.

######  Definition 2.9.

A proof-tree $d$ is a _deduction_ if $d$ is well-founded.

Equivalently, $d$ is well-founded if there is an assignment of ordinals,
$o^{d}:\operatorname{dom}(\sigma)\rightarrow Ord$ such that
$o^{d}(\tau)<o^{d}(\sigma)$ whenever $\sigma\sqsubsetneq\tau$.

###  2.3. Second Order Arithmetic

The theory $PA_{2}$ contains the following rules.

True${}_{\dot{R}t_{1}\cdots t_{n}}$ $\eta$ where $t_{1},\cdots,t_{n}$ are
closed, $\eta\in\\{\dot{R}t_{1}\cdots t_{n},\neg\dot{R}t_{1}\cdots t_{n}\\}$,
and $\eta$ is true.

Ax{η,∼η} $\eta,\neg\eta$ where $\eta$ is a literal.

$\phi$ $\psi$ I$\wedge_{\phi\wedge\psi}$ $\phi\wedge\psi$

$\phi$ I$\vee^{L}_{\phi\vee\psi}$ $\phi\vee\psi$ $\psi$
I$\vee^{R}_{\phi\vee\psi}$ $\phi\vee\psi$

$\phi(y)$ I$\forall^{y}_{\forall x\phi}$ $!y!$, where $y$ is substitutable for
$x$ in $\phi$ $\forall x\,\phi$

$\phi(t)$ I$\exists^{t}_{\exists x\,\phi}$ where $t$ is substitutable for $x$
in $\phi$ $\exists x\,\phi$

$\phi(Y)$ I$\forall^{Y}_{\forall^{2}X\phi}$ $!Y!$, where $Y$ is substitutable
for $X$ in $\phi$ $\forall^{2}X\,\phi$

$\phi[X\mapsto\psi]$ I$\exists^{\psi}_{\exists^{2}X\,\phi}$ where $\psi$ is
substitutable for $X$ in $\phi$ $\exists^{2}X\,\phi$

Ind${}^{t}_{\phi(x)}$ where $t$ is substitutable for $x$ in $\phi$
${\sim}\phi(0),\exists x\,(\phi(x)\wedge{\sim}\phi(Sx)),\phi(t)$

$\phi$ ${\sim}\phi$ Cutϕ $\emptyset$

When one of these rules has a single premise, we call it $\top$. The two
premises of the I$\wedge$ are $L$ and $R$, for left and right. The two
premises of the Cut rule are $\top$ and $\bot$.

We write $PA_{2}\vdash\Sigma$ if there is a valid deduction $d$ in $PA_{2}$
with $\Gamma(d)\subseteq\Sigma$. We write $PA_{2,<0}$ for the fragment of
$PA_{2}$ omitting Cut, and similarly write $PA_{2,<0}\vdash\Sigma$ if there is
a valid deduction $d$ in $PA_{2,<0}$ with $\Gamma(d)\subseteq\Sigma$. An
ordinal analysis, such as the one we will give below, shows, among other
things, that $PA_{2}\not\vdash\emptyset$.

##  3\. Local Functions on Proof-Trees

In this section, we describe certain kinds of functions from proof-trees to
proof-trees, namely those which are defined “one rule at a time” starting from
the root.

Our motivating example is, of course, the cut-elimination operation itself. It
is an observation going back to [8, 4] that (at least when we have the Rep
rule  $\emptyset$ $\emptyset$ ), if $d$ is a deduction and $d^{\prime}$ is the
result of applying the cut-elimination operators to $d$, then the bottom part
of $d^{\prime}$ is determined by a suitable bottom part of $d$.

Here we introduce some machinery, building on [4] and [13], for representing
this operation as a proof-tree itself.

###  3.1. Encoding Local Functions

To deal with proof-trees that represent functions, we want to introduce a new
kind of “formula”, which we call a _tag_. When $F$ is a proof-tree, a tag in
$\Gamma(F)$ indicates that $F$ should be “interpreted as a function”. (Because
weakening is built into our system, note that we can then interpret _any_
proof-tree as a function: if there is no tag in $\Gamma(d)$ then $d$ will
represent a constant function.)

######  Definition 3.1.

A _tag_ is a triple $(\Theta_{0},\epsilon,\Theta)$ where
$\Theta_{0}\subseteq\Theta$ are sequents and $\epsilon$ is a
$\mathfrak{T}$-sequence for some $\mathfrak{T}$. We call $\Theta_{0}$ the
_root_ of the tag.

When $t=(\Theta_{0},\epsilon,\Theta)$, we write $\mathsf{r}(t)$ for
$\Theta_{0}$, $\epsilon(t)$ for $\epsilon$, and $\Theta(t)$ for $\Theta$.

The tag we expect to see in $\Gamma(F)$ is
$(\Theta_{0},\langle\rangle,\Theta_{0})$. At some internal position
$\Gamma(F,\sigma)$, we might instead see some $(\Theta_{0},\epsilon,\Theta)$;
this essentially means that, at position $\sigma$ in $F$, we have “looked at”
the part of the input up to $\epsilon$. The sequent $\Theta_{0}$ will be
removed from the conclusion of the input.

The link between the sequent $\Theta_{0}$ and the theory $\mathfrak{T}$ will
be built into our proof system.

We need to expand our sequents a bit.

######  Definition 3.2.

An _extended sequent_ is a pairs of sets $\Delta;\Upsilon$ where $\Delta$ is a
sequent and $\Upsilon$ is a set of tags. We write $\cdot_{\mathsf{t}}$ for the
tag part of a sequent, so $(\Delta;\Upsilon)_{\mathsf{t}}=\Upsilon$.

When $\Delta;\Upsilon$ is an extended sequent and
$(\mathfrak{T},\Theta_{0},\epsilon,\Theta)$ is a tag, we take
$\Delta;\Upsilon\setminus\\{(\Theta_{0},\epsilon,\Theta)\\}$ to mean
$\Delta;(\Upsilon\setminus\\{(\Theta_{0},\epsilon,\Theta^{\prime})\mid\Theta\subseteq\Theta^{\prime}\\})$.

That is, we abuse notation to understand removing a tag
$(\Theta_{0},\epsilon,\Theta)$ from an extended sequent to remove all tags of
the form $(\Theta_{0},\epsilon,\Theta^{\prime})$ with
$\Theta\subseteq\Theta^{\prime}$.

We apply this convention, in particular, to the definition of
$\Gamma(d,\sigma)$: $(\Theta_{0},\epsilon,\Theta^{\prime})\in\Gamma(d,\sigma)$
if there is a $\tau$ with $t\in\Delta(\tau)$ and for all
$\tau^{\prime}\iota\sqsubseteq\tau$, there is no
$(\Theta_{0},\epsilon,\Theta)\in\Delta_{\iota}(d(\sigma\tau^{\prime}))$ with
$\Theta\subseteq\Theta^{\prime}$.

Corresponding to this, we extend the definition of a tag to include extended
sequents. (More precisely, we have to define extended sequents and tags by a
simultaneous induction: new tags give us new extended sequents, which give us
yet more tags.)

The following rule is essential to representing local functions as proof-
trees.

$\Delta(\mathcal{R})\setminus\Theta;\\{(\Theta_{0},\epsilon\iota,\Theta)\mid\iota\in|\mathcal{R}|\\}$
$(\mathcal{R}\in\mathfrak{T})$
Read${}_{\mathfrak{T},\Theta_{0},\epsilon,\Theta}$
$\Delta(\epsilon)\setminus\Theta;(\Theta_{0},\epsilon,\Theta)$

Note that this rule branches over rules from $\mathfrak{T}$. Reading from the
bottom up (as we often read our proof-trees), we interpret this rule to say:
“look at the input corresponding to the tag $\Theta_{0}$, in the position
$\epsilon$; if the rule here is $\mathcal{R}$, follow the $\mathcal{R}$-branch
of this rule”.

We need one slightly ad hoc restriction on proof-trees to support our notion
of ordinal bounds later.

######  Definition 3.3.

When $d$ is a proof-tree, a _consecutive Read_ is a pair $(\sigma,\iota)$ with
$\sigma\in\operatorname{dom}(d)$, $\sigma\iota\in\operatorname{dom}(d)$ so
that $d(\sigma)=Read_{\mathfrak{T},t}$ and
$d(\sigma\iota)=Read_{\mathfrak{T},t^{\prime}}$ where $t$ and $t^{\prime}$
share the same root.

We say $d$ is _free of consecutive Reads_ if $d$ does not contain any
consecutive Reads.

We will always want our proof-trees to be free of consecutive Reads. (In
practice, we can accomplish this by including the Rep rule in our system and
using Rep rules to separate otherwise consecutive Reads.) Therefore, for the
remainder of this paper, we assume proof-trees are free of consecutive Reads.

######  Definition 3.4.

A _locally defined function from $\mathfrak{T}$ to $\mathfrak{T}^{\prime}$_ is
a sequent $\Theta_{0}$ together with a proof-tree $F$ in
$\mathfrak{T}^{\prime}+\\{\mathrm{Read}_{\mathfrak{T},\Theta_{0},\epsilon,\Theta}\mid\Theta_{0}\subseteq\Theta\\}$.

More generally, a _locally defined function from
$\mathfrak{T}_{1},\ldots,\mathfrak{T}_{k}$ in $\mathfrak{T}^{\prime}$_ is a
sequence of sequents $\Theta_{0}^{1},\ldots,\Theta_{0}^{k})$ together with a
proof-tree $F$ in $\mathfrak{T}^{\prime}+\bigcup_{i\leq
k}\\{\mathrm{Read}_{\mathfrak{T}^{i},\Theta^{i}_{0},\epsilon,\Theta}\mid\Theta^{i}_{0}\subseteq\Theta\\}$.

We will see that we can interpret a locally defined function as a function
from proof-trees in $\mathfrak{T}$ to proof-trees in $\mathfrak{T}^{\prime}$.
(Forbidding consecutive Reads is necessary to rule out a degenerate case.)

Note that a locally defined function is essentially just a proof-tree which we
choose—via our choice of the root tag—to view as a function. We typically
simply say $F$ is a locally defined function and write $\Theta_{F}$ for the
associated root.

######  Definition 3.5.

Let $d$ be a proof-tree in $\mathfrak{T}$ and $F$ a locally defined function
from $\mathfrak{T}$ to $\mathfrak{T}^{\prime}$. We define a proof-tree
$\bar{F}(d)$ in $\mathfrak{T}^{\prime}$ along with auxiliary functions
$h_{0},h$ from $\operatorname{dom}(\bar{F}(d))$ to $\operatorname{dom}(F)$:

  * •

$h_{0}(\langle\rangle)=\langle\rangle$,

  * •

if $F(h_{0}(\sigma))=\mathrm{Read}_{\mathfrak{T},t}$ where
$\mathsf{r}(t)=\Theta_{F}$ then $h(\sigma)=h_{0}(\sigma)d(\epsilon_{t})$;
otherwise $h(\sigma)=h_{0}(\sigma)$,

  * •

$\bar{F}(d)(\sigma)=F(h(\sigma))$ and, for all $\iota\in|F(h(\sigma))|$,
$h_{0}(\sigma\iota)=h(\sigma)\iota$,

That is, we copy over the proof-tree $F$, except that at $\mathrm{Read}$ rules
we delete the rule and use $d$ to decide which branch to take. (If we had
consecutive Read rules, we could have an infinite branch consisting entirely
of Read rules which looks at the input but never places any rules, which would
lead $\bar{F}(d)$ to be undefined.)

The key point is that the conclusion of $\bar{F}(d)$ is the combination of the
conclusions of $d$ and the conclusion of $F$ in precisely the way we expect.

######  Theorem 3.6.

$\Gamma(\bar{F}(d))\subseteq(\Gamma(d)\setminus\Theta_{F})\cup(\Gamma(F)\setminus\\{(\Theta_{F},\langle\rangle,\Theta_{F})\\})$.

###### Proof.

Suppose $\phi\in\Gamma(\bar{F}(d))$, so there is some
$\sigma\in\operatorname{dom}(\bar{F}(d))$ so that
$\phi\in\Delta(\bar{F}(d)(\sigma))$ and
$\phi\not\in\Delta_{\iota}(\bar{F}(d)(\tau))$ for any
$\tau\iota\sqsubseteq\sigma$.

If $\phi\in\Gamma(F)$, we are done, so suppose not. We have
$\phi\in\Delta(F(h(\sigma)))$. Choose $\sigma^{\prime}\sqsubseteq h(\sigma)$
minimal so that $\phi\in\Delta(F(\sigma^{\prime}))$. Since $\phi$ is not
removed at any rule of $\bar{F}(d)$ below $\sigma$, $\phi$ must be removed at
some Read${}_{\mathfrak{T},\Theta_{F},\epsilon,\Theta}$ inference below
$\sigma^{\prime}$, so $\phi\in\Delta(\mathcal{R})\setminus\Theta$ where
$\mathcal{R}$ is $d(\epsilon)$ for some $\epsilon\in\operatorname{dom}(d)$.

Suppose there is some $\epsilon^{\prime}\iota\sqsubseteq\epsilon$ with
$\phi\in\Delta_{\iota}(d(\epsilon^{\prime}))$. Then there is some
corresponding $\tau\sqsubseteq\sigma^{\prime}$ so that $F(\tau)$ is
Read${}_{\mathfrak{T},\Theta_{F},\epsilon^{\prime},\Theta^{\prime}}$ for some
$\Theta^{\prime}\subseteq\Theta$. Therefore $\phi\not\in\Theta^{\prime}$, so
$\phi\in\Delta(F(\tau))$, contradicting the minimality of $\sigma^{\prime}$.

Therefore $\phi\in\Gamma(d)$. ∎

###  3.2. Extensions of Locally Defined Function

One of the crucial features of locally defined functions is that there is a
natural way to extend them to apply to larger theories, simply by acting as
the identity on new rules. Given a locally defined function $F$ from
$\mathfrak{T}$ and some other theory $\mathfrak{T}^{+}$ (presumably extending
$\mathfrak{T}$, though we don’t need this assumption), we can try to extend
$F$ to $\mathfrak{T}^{+}$ by assuming $F$ “does nothing” on rules in
$\mathfrak{T}^{+}\setminus\mathfrak{T}$.

######  Definition 3.7.

Given a locally defined function $F$ on $\mathfrak{T}$ with tag $t$, we define
the _lift_ of $F$ to $\mathfrak{T}^{+}$, $F^{\uparrow}$, by induction as
follows, along with functions
$h:\operatorname{dom}(F^{\uparrow})\rightarrow\operatorname{dom}(F)$ and
$\pi_{\sigma}:I_{\ast}(s_{t}(h(\sigma)))\rightarrow I_{\ast}(s_{t}(\sigma))$:

  * •

$h(\langle\rangle)=\langle\rangle$,

  * •

$\pi_{\langle\rangle}(\langle\rangle)=\langle\rangle$,

  * •

if $F(h(\sigma))$ is a Read${}_{\mathfrak{T},\Theta_{F},\epsilon,\Theta}$ rule
then:

    * –

$F^{\uparrow}(\sigma)$ is
Read${}_{\mathfrak{T}^{+},\Theta_{F},\pi_{\sigma}(\epsilon),\Theta}$,

    * –

for each $\mathcal{R}$ in $\mathfrak{T}$,

      * *

$h(\sigma\mathcal{R})=h(\sigma)\mathcal{R}$,

      * *

for each $\epsilon^{\prime}\in I_{\ast}(s_{t}(h(\sigma)\mathcal{R}))$, if
$\epsilon^{\prime}\in I_{\ast}(s_{t}(h(\sigma)))$ then
$\pi_{\sigma\mathcal{R}}(\epsilon^{\prime})=\pi_{\sigma}(\epsilon^{\prime})$,
and if $\epsilon^{\prime}$ is $\epsilon\iota$ for some $\iota\in|\mathcal{R}|$
then $\pi_{\sigma\mathcal{R}}(\epsilon^{\prime})=\pi_{\sigma}(\epsilon)\iota$,

    * –

for each $\mathcal{R}$ in $\mathfrak{T}^{+}\setminus\mathfrak{T}$ other than a
Read rule:

      * *

$F^{\uparrow}(\sigma\mathcal{R})=\mathcal{R}$,

      * *

for $\iota\in|\mathcal{R}|$,
$h(\sigma\mathcal{R}\iota)=h(\sigma\mathcal{R})=h(\sigma)$,

      * *

for each $\epsilon^{\prime}\in
I_{\ast}(s_{t}(h(\sigma\mathcal{R}\iota)))=I_{\ast}(s_{t}(h(\sigma)))$, if
$\epsilon^{\prime}\neq\epsilon$ then
$\pi_{\sigma\mathcal{R}\iota}(\epsilon^{\prime})=\pi_{\sigma}(\epsilon^{\prime})$,
and $\pi_{\sigma\mathcal{R}\iota}(\epsilon)=\pi_{\sigma}(\epsilon)\iota$,

    * –

for each
Read${}_{\mathfrak{T}^{\prime},\Theta^{\prime},\epsilon^{\prime},\Theta^{\prime\prime}}$
in $\mathfrak{T}^{+}\setminus\mathfrak{T}$:

      * *

$F^{\uparrow}(\sigma\mathcal{R})$ is
Read${}_{\mathfrak{T}^{\prime},\Theta^{\prime},\epsilon^{\prime},\Theta^{\prime\prime}\cup\Theta}$,

      * *

for $\iota\in|\mathcal{R}|$,
$h(\sigma\mathcal{R}\iota)=h(\sigma\mathcal{R})=h(\sigma)$,

      * *

for each $\epsilon^{\prime}\in
I_{\ast}(s_{t}(h(\sigma\mathcal{R}\iota)))=I_{\ast}(s_{t}(h(\sigma)))$, if
$\epsilon^{\prime}\neq\epsilon$ then
$\pi_{\sigma\mathcal{R}\iota}(\epsilon^{\prime})=\pi_{\sigma}(\epsilon^{\prime})$,
and $\pi_{\sigma\mathcal{R}\iota}(\epsilon)=\pi_{\sigma}(\epsilon)\iota$,

  * •

If $F(h(\sigma))$ is any other rule then

    * –

$F^{\uparrow}(\sigma)=F(h(\sigma))$,

    * –

$h(\sigma\iota)=h(\sigma)\iota$ for all $\iota\in|F(h(\sigma))|$,

    * –

$\pi_{\sigma\iota}=\pi_{\sigma}$ for all $\iota\in|F(h(\sigma))|$,

######  Definition 3.8.

Let $\mathcal{F}$ be a set of formulas. We say $\mathfrak{T}^{+}$ is _rule-by-
rule conservative over $\mathfrak{T}$ for $\mathcal{F}$_ if:

  * •

whenever $\mathcal{R}\in\mathfrak{T}^{+}\setminus\mathfrak{T}$ is not a Read
inference, $\Delta(\mathcal{R})\cap\mathcal{F}=\emptyset$,

  * •

if $\mathcal{R}\in\mathfrak{T}^{+}\setminus\mathfrak{T}$ is a Read inference
then $\Delta(\mathcal{R})_{\mathsf{t}}\cap\mathcal{F}=\emptyset$.

######  Lemma 3.9.

Let $F$ be a locally defined function on $\mathfrak{T}$ and suppose that for
every Read${}_{\mathfrak{T},\Theta_{F},\epsilon,\Theta}$ rule appearing in
$F$, $\mathfrak{T}^{+}$ is rule-by-rule conservative over $\mathfrak{T}$ for
$\Theta$.

Then $\Gamma(F^{\uparrow})\subseteq\Gamma(F)$.

###### Proof.

Consider any $\sigma$ and any $\phi\in\Delta(F^{\uparrow}(\sigma))$ and
suppose $\phi\not\in\Gamma(F)$. We will show that there is a
$\tau\iota\sqsubseteq\sigma$ with $\phi\in\Delta_{\iota}(F^{\uparrow}(\tau))$.

Suppose $\Delta(F(h(\sigma)))=\Delta(F^{\uparrow}(\sigma))$. Since
$\phi\not\in\Gamma(F)$, there is some $\tau\iota\sqsubseteq h(\sigma)$ with
$\phi\in\Delta_{\iota}(F(\tau))$; but there is a
$\tau^{\prime}\iota\sqsubseteq\sigma$ with $h(\tau^{\prime})=\tau$ and
$F^{\uparrow}(\tau^{\prime})=F(\tau)$, and therefore
$\phi\in\Delta_{\iota}(F^{\uparrow}(\tau^{\prime}))$.

Otherwise $F^{\uparrow}(\sigma)$ must be $\mathcal{R}$ for some
$\mathcal{R}\in\mathfrak{T}^{+}\setminus\mathfrak{T}$, and therefore
$\sigma=\sigma^{\prime}\mathcal{R}$ where $F^{\uparrow}(\sigma^{\prime})$ is a
Read${}_{\mathfrak{T}^{+},\Theta_{F},\epsilon,\Theta}$ inference. If
$\mathcal{R}$ is not a Read inference then we have
$\Delta(F^{\uparrow}(\sigma))=\Delta(\mathcal{R})$ and therefore
$\Delta(F^{\uparrow}(\sigma))$ is disjoint from $\Theta$; but this means
$\phi\in\Delta_{\mathcal{R}}(\sigma^{\prime})$ as promised.

If $\mathcal{R}$ is a Read inference in
$\mathfrak{T}^{+}\setminus\mathfrak{T}$ then we have
$\Delta(\mathcal{R})\cap\Theta=\emptyset$, and therefore again
$\phi\in\Delta_{\mathcal{R}}(\sigma^{\prime})$. ∎

##  4\. Infinitary Theory

###  4.1. Language and Theories

We need to modify our language by requiring that free second-order variables
have a “level”. The level will be a natural number which roughly represents
the depth of nested parameters in the construction of sets. Bound variables
will not have a level.

######  Definition 4.1.

The language $\mathcal{L}_{2}^{\infty}$ is the language $\mathcal{L}_{2}$ with
the following modification:

  * •

the set $Var_{2}$ of second order variables is partitioned into infinitely
many sets $Var_{2}=\bigcup_{\ell\in\mathbb{N}\cup\\{\ast\\}}Var_{2}^{\ell}$
where each $Var_{2}^{\ell}=\\{X^{\ell},Y^{\ell},Z^{\ell},\ldots\\}$ is
infinite.

The second-order variables labeled by $\ast$ are the unleveled ones—that is,
the variables that appear bound. We omit the $\ast$ level when writing
variables, so free second-order variables should always have a level indicated
as a superscript, while bound second-order variables have no superscript.

For formal reasons, we will need the Rep rule:

$\emptyset$ Rep  $\emptyset$

As usual, our infinitary system will replace the I$\forall$ rule with the
$\omega$ rule:  $\cdots\phi(n)\cdots$ $(n\in\mathbb{N})$ $\omega_{\forall
x\,\phi}$ $\forall x\,\phi$

Finally, we introduce the distinctive rule for our infinitary system, a
modified form of the Buchholz $\Omega$ rule, which will let us include locally
defined functions inside our deductions.

When $\mathfrak{T}$ is a theory, the $\Omega^{\flat}$ rule555We think of this
as “flattening” Buchholz’s version of the $\Omega$ rule: it has a single
premise which is essentially an algorithm describing how to calculate a
function, where the premises of the $\Omega$ rule essentially encode the graph
of the function. is

$(\\{{\sim}\phi(Y^{\ell})\\},\langle\rangle,\\{{\sim}\phi(Y^{\ell})\\})$
$\Omega^{\flat}_{Y^{\ell},\exists^{2}X\,\phi}$ $\exists^{2}X\,\phi$

As usual [4][1], we need a partner rule that combines this rule with a Cut
inference:

${\sim}\phi(Z^{\ell})$
$(\\{{\sim}\phi(Y^{\ell})\\},\langle\rangle,\\{{\sim}\phi(Y^{\ell})\\})$
Cut$\Omega^{\flat}_{Z^{\ell},Y^{\ell},\exists^{2}X\,\phi}$
$!\\{Z^{\ell}\\},\emptyset!$ $\emptyset$

The eigenvariables here indicate, of course, that $Z^{\ell}$ is an eigenvalue
in the left premise and there are no eigenvariables in the right premise.

These are the only rules which can remove a tag from a premise without adding
one in the conclusion. These allows us to have proof-trees which infer
formulas from the existence of functions. We call the unique premise of
$\Omega^{\flat}$ the $\bot$ premise666This is inconsistent with the way we
have named the premises of other single premise rules, but reflects that we
think of the premise of an $\Omega^{\flat}$ rule as an essentially negative
thing, since it is a function on proofs of the positive thing., and then
Cut$\Omega^{\flat}$ has two premises, $\top$ and $\bot$.

We introduce two measures of complexity on formulas. Roughly speaking, the
_depth_ will measure the nesting of second-order quantifiers while the _level_
will measure how the formula depends on parameters. In particular, the formula
$\exists^{2}X\,\phi(X,\forall^{2}Y\,\psi(X,Y))$ will have depth $2$ and level
$0$, while the formula $\exists^{2}X\,\phi(X,\forall^{2}Y\,\psi(Y))$ will have
depth $1$ and level also $1$—the first formula involves a nested quantifier,
while the second involves a single quantifier relative to a parameter (the
completed formula $\forall^{2}Y\,\psi(Y)$). (More precisely, we are interested
in the quantities $dp(\phi,\\{X\\})$ and $lvl(\phi,\\{X\\})$ when considering
a formula $\exists^{2}X\,\phi$.)

######  Definition 4.2.

If $\mathcal{S}$ is a set of second-order variables, $dp(\phi,\mathcal{S})$ is
defined inductively by:

  * •

when $\phi$ is a literal, $dp(\phi,\mathcal{S})=0$,

  * •

when $\phi$ is $\psi_{0}\wedge\psi_{1}$ or $\psi_{0}\vee\psi_{1}$,
$dp(\phi,\mathcal{S})=max\\{dp(\psi_{0},\mathcal{S}),dp(\psi_{1},\mathcal{S})\\}$,

  * •

when $\phi$ is $\forall x\,\psi$ or $\exists x\,\psi$,
$dp(\phi,\mathcal{S})=dp(\psi,\mathcal{S})$,

  * •

if any variable in $\mathcal{S}$ is free in $\psi$ then
$dp(\forall^{2}Y\,\psi,\mathcal{S})=dp(\exists^{2}Y\,\psi,\mathcal{S})=dp(\psi,\mathcal{S}\cup\\{Y\\})+1$,

  * •

if no variable in $\mathcal{S}$ is free in $\psi$ then
$dp(\forall^{2}Y\,\psi,\mathcal{S})=dp(\exists^{2}Y\,\psi,\mathcal{S})=0$.

$lvl(\phi,\mathcal{S})$ is defined inductively by:

  * •

when $\phi$ is $X^{\ell}n$ or $\neg X^{\ell}n$ then
$lvl(\phi,\mathcal{S})=\ell+1$,

  * •

when $\phi$ is any other literal, $lvl(\phi,\mathcal{S})=0$,

  * •

when $\phi$ is $\psi_{0}\wedge\psi_{1}$ or $\psi_{0}\vee\psi_{1}$,
$lvl(\phi,\mathcal{S})=max\\{lvl(\psi_{0},\mathcal{S}),lvl(\psi_{1},\mathcal{S})\\}$,

  * •

when $\phi$ is $\forall x\,\psi$ or $\exists x\,\psi$,
$lvl(\phi,\mathcal{S})=lvl(\psi,\mathcal{S})$,

  * •

if any variable in $\mathcal{S}$ is free in $\psi$ then
$lvl(\forall^{2}Y\,\psi,\mathcal{S})=lvl(\exists^{2}Y\,\psi,\mathcal{S})=lvl(\psi,\mathcal{S}\cup\\{Y\\})$,

  * •

if no variable in $\mathcal{S}$ is free in $\psi$ then
$lvl(\forall^{2}Y\,\psi,\mathcal{S})=lvl(\exists^{2}Y\,\psi,\mathcal{S})=lvl(\psi,\emptyset)+1$.

We write $lvl(\phi)$ for $lvl(\phi,\emptyset)$.

Given a formula of the form $Q^{2}X\,\phi$, we write $comp(Q^{2}X\,\phi)$ for
the pair $(dp(\phi,\\{X\\}),lvl(\phi,\\{X\\}))$, which we call the
_complexity_ of $Q^{2}X\,\phi$. We compare complexities in reverse
lexicographic order: $(m^{\prime},\ell^{\prime})<(m,\ell)$ if
$\ell^{\prime}<\ell$ or $\ell^{\prime}=\ell$ and $m^{\prime}<m$.

We need to build a suitable hierarchy of theories, because using these rules
requires specifying suitable theories to use as the domains of our
$\Omega^{\flat}$ and Cut$\Omega^{\flat}$ rules.

In order to keep our bounds suitably uniform, we want to work in theories with
a global bound on the complexity. The theory $PA_{2,<0}^{\infty,N,L}$ will
only include $\Omega^{\flat}$ and Cut$\Omega^{\flat}$ rules introducing
formulas with complexity less than $(N,L)$. We do not attempt here to match
the strength of these theories to natural finitary theories (in particular,
while the theories $PA_{2,<0}^{\infty,N,L}$ as $L$ goes to infinity probably a
strength similar to that of $\Pi^{1}_{N}\mathchar 45\relax CA_{0}$, we have
not attempted to calibrate them to make this exact). (As motivation for the
system of levels, note that the systems $PA_{2,<0}^{\infty,1,L}$ have roughly
$L$ iterations of $\Pi^{1}_{1}$-comprehension—that is,
$PA_{2,<0}^{\infty,1,L}$ is similar in strength to $ID_{L}$, though again, we
have not attempted to make this exact.)

######  Definition 4.3.

  * •

the base theory $PA_{2,<0}^{\infty,N,L,-}$ consists of the following rules,
subject to the constraints that first-order variables do not appear free,
second-order variables of level $\ast$ do not appear free, and there are no
quantifiers over variables $Y^{\ell}$:

    * –

Rep,

    * –

$\mathrm{True}_{\eta}$ where $\eta$ is a true literal,

    * –

Ax, I$\wedge$, I$\vee$, $\omega$, I$\exists$,

    * –

I$\forall^{Y^{lvl(\forall^{2}X\,\phi)}}_{\forall^{2}X\,\phi}$,

    * –

$\Omega^{\flat}_{Y^{\ell},\exists^{2}X\,\phi}$ where $\ell$ is
$lvl(\phi,\\{X\\})$,

  * •

$C^{\infty,m,\ell}$ is the theory containing only rules
Cut$\Omega^{\flat}_{Z^{\ell},Y^{\ell},\exists^{2}X\,\phi}$ where
$(m,\ell)=\mathrm{comp}(\exists^{2}X\,\phi)$,

  * •

$R^{\infty,N,L,m,\ell}$ is the theory containing only rules
Read${}_{PA_{2,<0}^{\infty,N,L,m,\ell,-},{\sim}\phi(Y^{\ell}),\epsilon,\Theta}$
where $(m,\ell)=\mathrm{comp}(\exists^{2}X\,\phi)$,

  * •

$PA_{2,<0}^{\infty,N,L,m,\ell,-}$ is
$PA_{2,<0}^{\infty,N,L,-}+\bigcup_{(m^{\prime},\ell^{\prime})<(m,\ell)}C^{\infty,m^{\prime},\ell^{\prime}}+\bigcup_{m^{\prime}<m,\ell^{\prime}\leq
L}R^{\infty,N,L,m^{\prime},\ell^{\prime}}$,

  * •

$PA_{2,<0}^{\infty,N,L,m,\ell}$ is
$PA_{2,<0}^{\infty,n,m,\ell,-}+\bigcup_{m^{\prime}\leq
N,\ell^{\prime}<\ell}R^{\infty,N,L,m^{\prime},\ell^{\prime}}$.

  * •

$PA_{2,<r}^{\infty,N,L,m,\ell}$ is $PA_{2,<0}^{\infty,n,m,\ell}$ plus Cut
rules over all formulas of rank $<r$,

  * •

$PA_{2,<r}^{\infty,n<L}$ is
$\bigcup_{m<N,\ell<L}PA_{2,<r}^{\infty,N,L,m,\ell}$.

The difference between $PA_{2,<0}^{\infty,N,L,m,\ell,-}$ and
$PA_{2,<0}^{\infty,N,L,m,\ell}$ is the presence of Read rules for low level
($\ell^{\prime}<\ell$) but high depth ($m^{\prime}\geq m$) theories. We will
never really prove things in $PA_{2,<0}^{\infty,N,L,m,\ell,-}$; rather, we
will lift functions from the domain $PA_{2,<0}^{\infty,N,L,m,\ell,-}$ to the
domain $PA_{2,<0}^{\infty,N,L,m,\ell}$. However this restriction will play a
crucial role in our ordinal bounds.

######  Lemma 4.4.

For any $\phi$, $X$, letting $(m,\ell)=comp(\exists^{2}X\,\phi)$, for any
$n\geq m$ and $L\geq\ell$ there is a locally defined function
$\mathrm{Id}^{\phi}$ in $PA_{2,<0}^{\infty,N,L}$ so that
$\Gamma(\mathrm{Id}^{\phi})\subseteq\phi;(\phi,\langle\rangle,\phi)$ where

###### Proof.

We construct Idϕ by induction on $\sigma$. We set
Id${}^{\phi}(\langle\rangle)=Read_{PA_{2,<0}^{\infty,N,L,m,\ell,-},\phi,\langle\rangle,\phi}$.

Given any $\sigma$ with
Id${}^{\phi}(\sigma)=Read_{PA_{2,<0}^{\infty,N,L,m,\ell,-},\phi,\epsilon,\phi}$,
for each $\mathcal{R}$, we define
Id${}^{\phi}(\sigma\mathcal{R})=\mathcal{R}$, and for each
$\iota\in|\mathcal{R}|$, we define
Id${}^{\phi}(\sigma\mathcal{R}\iota)=Read_{PA_{2,<0}^{\infty,N,L,m,\ell,-},\phi,\epsilon\iota,\phi}$.
∎

######  Lemma 4.5.

For any closed formula $\phi$ there are $N,L$ large enough so there is a
proof-tree $d_{\phi}$ in PA${}^{\infty,N,L}_{2,<0}$ with
$\Gamma(d_{\phi})\subseteq\\{\phi,{\sim}\phi\\}$.

###### Proof.

By induction on $\phi$. When $\phi$ is a literal, we take
$d_{\phi}(\langle\rangle)=Ax_{\\{\phi,{\sim}\phi\\}}$.

If $\phi$ is constructed by $\wedge,\vee,\forall,\exists$, this is standard.

Suppose $\phi$ is $\forall^{2}X\,\psi$. Then, choosing a fresh variable
$Y^{\ell}$, we may take $d_{\phi}$ to be

Idψ $\vdots$ $\psi(Y^{\ell});(\psi(Y^{\ell}),\langle\rangle,\psi(Y^{\ell})))$
$\Omega^{\flat}_{Y^{\ell},\exists^{2}X\,{\sim}\psi}$
$\psi(Y^{\ell}),\exists^{2}X\,{\sim}\psi$
I$\forall^{Y^{\ell}}_{\forall^{2}X\,\psi}$
$\forall^{2}X\,\psi,\exists^{2}X\,{\sim}\psi$

where the values of $m,\ell$ are determined by $\psi$.

The $\exists^{2}X\,\psi$ case is identical, using ${\sim}\psi$ in place of
$\psi$. ∎

###  4.2. Embedding

We show that deductions in $PA_{2}$ can be embedded in
$PA_{2,<r}^{\infty,N,L}$ for suitable $N,L,r$. Most of the work here is
embedding the I$\exists^{2}$ rule, which has to be replaced by a suitable
$\Omega^{\flat}$ rule. (The I$\forall$ rule is, of course, replaced by an
$\omega$ rule, but this step is by now standard.)

Here, as well as in the cut-elimination functions we define later, there is a
technical matter of handling possible conflicts between names of second order
variables. We ignore this issue here: we assume all second-order variables
have already been suitably renamed.

######  Theorem 4.6.

For any formulas $\phi(X^{\ell})$ and $\psi$, taking
$(m,\ell)=comp(\exists^{2}X\,\phi(X))$, for all sufficiently large $N,L$ there
is a locally defined function $F^{\phi,X^{\ell}\mapsto\psi}$ in
$PA_{2}^{\infty,N,L,m,\ell}$ with
$\Gamma(F)\subseteq\phi(\psi);(\phi(X^{\ell}),\langle\rangle,\phi(X^{\ell}))$.

The construction is exactly what one would expect: we proceed through the
input proof, replacing $X^{\ell}$ with $\psi$ everywhere it appears. When we
encounter some $\Omega^{\flat}$ rule introducing a formula
$\exists^{2}Y\,\phi^{\prime}(X^{\ell},Y)$, we replace it with an
$\Omega^{\flat}$ rule introducing $\exists^{2}Y\,\phi^{\prime}(\psi,Y)$; this
may mean changing the theory we branch over—replacing $X^{\ell}$ with $\psi$
may change the level (but, importantly, not the depth) of the formula.

We have to keep track of this change in theories, since we will then encounter
Read rules whose root tag comes from that $\Omega^{\flat}$ rule, and we need
to replace these with Read rules with the modified root tag.

###### Proof.

We define $F^{\phi,X^{\ell}\mapsto\psi}$ by induction on $\sigma$. We set
$F^{\phi,X^{\ell}\mapsto\psi}(\langle\rangle)=Read_{PA_{2,<0}^{\infty,N,L,m,\ell,-},\phi(X^{\ell}),\langle\rangle,\phi(X^{\ell})}$
and $\epsilon_{\langle\rangle}=\langle\rangle$.

Consider some $\sigma$ where $F^{\phi,X^{\ell}\mapsto\psi}(\sigma)$ is
$Read_{PA_{2,<0}^{\infty,N,L,m,\ell,-},\phi(X^{\ell}),\epsilon,\Theta}$. We
will maintain inductively that whenever
$(\mathfrak{T},\Lambda_{0},\zeta,\Lambda)$ is a tag in $\Theta$, we have an
associated tag
$(\mathfrak{T}^{\prime},\Lambda^{\prime}_{0},\zeta^{\prime},\Lambda^{\prime})$
so that there is a $\tau\iota\sqsubseteq\sigma$ with
$(\mathfrak{T}^{\prime},\Lambda^{\prime}_{0},\zeta^{\prime},\Lambda^{\prime})\in\Delta_{\iota}(F^{\phi,X^{\ell}\mapsto\psi}(\tau))$,
and we will have
$\Lambda^{\prime}\subseteq\Lambda[X^{\ell}\mapsto\psi]\cup\Theta$.

For each $\mathcal{R}$ in $PA_{2,<0}^{\infty,N,L,m,\ell,-}$, we will define
$F^{\phi,X^{\ell}\mapsto\psi}(\sigma\mathcal{R})$.

If $\Delta(\mathcal{R})\cap\Theta=\emptyset$, we may take
$F^{\phi,X^{\ell}\mapsto\psi}(\sigma\mathcal{R})=\mathcal{R}$ and
$F^{\phi,X^{\ell}\mapsto\psi}(\sigma\mathcal{R}\iota)=Read_{PA_{2,<0}^{\infty,N,L,m,\ell,-},\phi(X^{\ell}),\epsilon\iota,\Theta}$.
(Note that, if $\mathcal{R}$ is Cut$\Omega^{\flat}$ then $X^{\ell}$ cannot
appear free in the cut formula.)

If $\Delta(\mathcal{R})\cap\Theta\neq\emptyset$ and $\mathcal{R}$ is anything
other than $Ax$ or a Read, then $\Delta(\mathcal{R})=\\{\theta\\}$ for some
formula $\theta$; then there is a corresponding rule $\mathcal{R}^{\prime}$
which introduces $\theta[X\mapsto\psi]$, so we take
$F^{\phi,X^{\ell}\mapsto\psi}(\sigma\mathcal{R})=\mathcal{R}^{\prime}$ and
$F^{\phi,X^{\ell}\mapsto\psi}(\sigma\mathcal{R}\iota)=Read_{PA_{2,<0}^{\infty,N,L,m,\ell},\phi(X^{\ell}),\epsilon\iota,\Theta\cup\Delta_{\iota}(\mathcal{R})}$.
In the case where $\mathcal{R}$ is $\Omega^{\flat}$, note that we do satisfy
the requirement on the presence of a replacement tag; the theory
$\mathfrak{T}$ in this case has the form
$PA_{2,<0}^{\infty,N,L,m^{\prime},\ell^{\prime},-}$, and we are replacing it
with some $PA_{2,<0}^{\infty,N,L,m^{\prime},\ell^{\prime\prime}}$—that is, the
level might change (and indeed, might increase), but substituting $\psi$ for
$X^{\ell}$ does not change the depth.

If $\mathcal{R}$ is Ax${}_{\\{X^{\ell}n,\neg X^{\ell}n\\}}$ then we may
replace it with $d_{\psi(n)}$ (that is, we set
$F^{\phi,X^{\ell}\mapsto\psi}(\sigma\mathcal{R}\tau)=d_{\psi(n)}(\tau)$ for
all $\tau$).

The remaining case is that $\mathcal{R}$ is a
Read${}_{\mathfrak{T},\Lambda_{0},\zeta,\Lambda^{\prime}}$ rule whose
conclusion overlaps with $\Theta$. Here $\mathfrak{T}$ must be
$PA^{\infty,N,L,m^{\prime},\ell^{\prime},-}_{2,<0}$ for some $m^{\prime}<m$
and $\ell^{\prime}\leq\ell$. If
$\Delta(\mathcal{R})\cap\Theta\subseteq\Delta(\zeta)$, we set
$F^{\phi,X^{\ell}\mapsto\psi}(\sigma\mathcal{R})=Read_{\mathfrak{T},\Lambda_{0},\zeta,\Lambda^{\prime}\cup\Theta}$
and, as usual, set
$F^{\phi,X^{\ell}\mapsto\psi}(\sigma\mathcal{R}\iota)=Read_{PA_{2,<0}^{\infty,N,L,m^{\prime},\ell^{\prime}},\phi(X^{\ell}),\epsilon\iota,\Theta\cup\Delta_{\iota}(\mathcal{R})}$.

The really new case is when
$(\mathfrak{T},\Lambda_{0},\zeta,\Lambda)\in\Theta$. In this case we replaced
this tag with a new tag,
$(\mathfrak{T}^{\prime},\Lambda^{\prime}_{0},\zeta^{\prime},\Lambda^{\prime})$,
and so we set
$F^{\phi,X^{\ell}\mapsto\psi}(\sigma\mathcal{R})=Read_{\mathfrak{T}^{\prime},\Lambda^{\prime}_{0},\zeta^{\prime},\Lambda^{\prime}}$.

Since $\mathfrak{T}^{\prime}$ need not be $\mathfrak{T}$, the premises do not
line up, so we have to consider how to handle
$\sigma\mathcal{R}\mathcal{R}^{\prime}$. Consider some
$\mathcal{R}^{\prime}\in\mathfrak{T}^{\prime}$. If
$\Delta(\mathcal{R}^{\prime})\cap\Lambda[X^{\ell}\mapsto\psi]=\emptyset$ then
it is simpler to ignore what the input would have done in the
$\mathcal{R}^{\prime}$ branch; we instead apply the same argument to
$\mathcal{R}^{\prime}$ that we applied to $\mathcal{R}$, making all extensions
to the $\epsilon\mathrm{Rep}$ branch of the input. (Note that this
recurses—$\mathcal{R}^{\prime}$ could itself be another Read rule—but only
finitely many times, since $m^{\prime}$ drops at each step.)

So suppose
$\Delta(\mathcal{R}^{\prime})\cap\Lambda[X^{\ell}\mapsto\psi]\neq\emptyset$.
In this case there is a rule $\mathcal{R}^{\leftarrow}\in\mathfrak{T}$ so that
$\Delta(\mathcal{R}^{\leftarrow})[X^{\ell}\mapsto\psi]=\Delta(\mathcal{R}^{\prime})$.
Then we take
$F^{\phi,X^{\ell}\mapsto\psi}(\sigma\mathcal{R}\mathcal{R}^{\prime})=Read_{PA_{2,<0}^{\infty,N,L,m,\ell,-},\phi(X^{\ell}),\epsilon\mathcal{R}^{\leftarrow},\Theta\cup\Delta_{\iota}(\mathcal{R})}$.
∎

######  Theorem 4.7.

Let $d$ be a valid deduction in $PA_{2}$ so that every formula in $\Gamma(d)$
has first-order free variables contained in $x_{1},\ldots,x_{a}$ and second-
order free variables contained in $X_{1},\ldots,X_{b}$.

Then for sufficiently large $n,L$ and $r$, for every
$n_{1},\ldots,n_{a},\ell_{1},\ldots,\ell_{b}$, there is a valid proof-tree
$d^{\infty}_{n_{1},\ldots,n_{a}}$ in $PA^{\infty,n,L}_{2,<r}$ with
$\Gamma(d^{\infty}_{n_{1},\ldots,n_{a},\ell_{1},\ldots,\ell_{b}})\subseteq\Gamma(d)[x_{i}\mapsto
n_{i},X_{j}\mapsto X_{j}^{\ell_{j}}]$.

###### Proof.

By induction on $d$. We consider cases on $d(\langle\rangle)$.

If $d(\langle\rangle)$ is True, it is already a deduction of the desired form,
and if $d(\langle\rangle)$ is Axσ then we may take
$d^{\infty}_{n_{1},\ldots,n_{a},\ell_{1},\ldots,\ell_{b}}(\langle\rangle)$ to
be $Ax_{\sigma[x_{i}\mapsto n_{i},X_{j}\mapsto X_{j}^{\ell}]}$.

If $d(\langle\rangle)$ is I$\wedge$, I$\vee$, I$\exists$, or $Cut$ the claim
follows immediately from the inductive hypothesis.

If $d(\langle\rangle)$ is I$\forall^{y}_{\forall x\,\phi}$ then, for each
$n_{a+1}$, we may apply the inductive hypothesis to obtain a deduction
$d^{\infty}_{n_{1},\ldots,n_{a},n_{a+1},\ell_{1},\ldots,\ell_{b}}$ with
$\Gamma(d^{\infty}_{n_{1},\ldots,n_{a},n_{a+1},\ell_{1},\ldots,\ell_{b}})\subseteq\Gamma(d)[x_{i}\mapsto
n_{i},X_{j}\mapsto X_{j}^{\ell_{j}}],\phi[x_{i}\mapsto n_{i},x\mapsto
n_{a+1},X_{j}\mapsto X_{j}^{\ell_{j}}]$. We then obtain
$d^{\infty}_{n_{1},\ldots,n_{a},\ell_{1},\ldots,\ell_{b}}$ by applying an
$\omega$ rule to these deductions.

If $d(\langle\rangle)$ is Ind${}^{t}_{\forall x\,\phi}$, let
$\phi^{\prime}=\phi[x_{i}\mapsto n_{i},X_{j}\mapsto X_{j}^{\ell_{j}}]$. We
will construct deductions $d^{\infty}_{n}$ with
$\Gamma(d^{\infty}_{n})\subseteq{\sim}\phi^{\prime}(0),\exists
x\,(\phi^{\prime}(x)\wedge{\sim}\phi^{\prime}(Sx)),\phi^{\prime}(n)$ by
induction on $n$, and then obtain
$d^{\infty}_{n_{1},\ldots,n_{a},\ell_{1},\ldots,\ell_{b}}$ by applying an
$\omega$ rule to these deductions. When $n=0$, $d^{\infty}_{0}$ is
$d_{\phi^{\prime}(0)}$.

Suppose we have constructed $d^{\infty}_{n}$. Then we may take
$d^{\infty}_{n+1}$ to be

$d^{\infty}_{n}$ $\vdots$ ${\sim}\phi^{\prime}(0),\exists
x\,\phi^{\prime}(x)\wedge{\sim}\phi^{\prime}(Sx),\phi^{\prime}(n)$
$d_{\phi^{\prime}(Sn)}$ $\vdots$ ${\sim}\phi^{\prime}(Sn),\phi^{\prime}(Sn)$
${\sim}\phi^{\prime}(0),\exists
x\,\phi^{\prime}(x)\wedge{\sim}\phi^{\prime}(Sx),\phi^{\prime}(n)\wedge{\sim}\phi^{\prime}(Sn),\phi^{\prime}(Sn)$
${\sim}\phi^{\prime}(0),\exists
x\,\phi^{\prime}(x)\wedge{\sim}\phi^{\prime}(Sx),\phi^{\prime}(Sn)$

If $d(\langle\rangle)$ is I$\forall^{Y}$ then we may choose a suitable $\ell$
and apply the inductive hypothesis.

Finally, if $d(\langle\rangle)$ is I$\exists^{\psi}_{\exists^{2}X\,\phi}$,
letting $\phi^{\prime}=\phi[x_{i}\mapsto n_{i},X_{j}\mapsto
X_{j}^{\ell_{j}}]$, $\psi^{\prime}=\psi[x_{i}\mapsto n_{i},X_{j}\mapsto
X_{j}^{\ell_{j}}]$, and $d^{\prime}$ be the result of the inductive
hypothesis, we have

$d^{\prime}$ $\vdots$ $\phi[\psi]$ $F^{{\sim}\phi,X^{\ell}\mapsto\psi}$
$\Omega^{\flat}$ $\exists^{2}X\,\phi,{\sim}\phi[\psi]$ Cut
$\exists^{2}X\,\phi$ ∎

###  4.3. Cut-Elimination

We describe the cut-elimination operators. These definitions below are
completely standard, expressed here in the language of locally defined
functions.

We need one final theory.

######  Definition 4.8.

$PA^{\infty,N,L,-}_{2,<r}$ is the result of removing all Read rules from
$PA^{\infty,N,L}_{2,<r}$.

######  Lemma 4.9 ($\bot$ Inversion).

If $\eta$ is a false literal then there is a locally defined function
$\mathrm{Inverse}^{\bot}_{\eta}$ on $PA^{\infty,N,L,-}_{2,<r}$ in
$PA^{\infty,N,L}_{2,<r}$ with
$\Gamma(\mathrm{Inverse}^{\bot}_{\eta})\subseteq(\eta,\langle\rangle,\eta)$.

###### Proof.

We define $\mathrm{Inverse}^{\bot}_{\eta}(\sigma)$ by induction on $\sigma$.
We set
$\mathrm{Inverse}^{\bot}_{\eta}(\langle\rangle)=Read_{PA^{\infty,N,L,-}_{2,<r},\eta,\epsilon,\eta}$.

Suppose
$\mathrm{Inverse}^{\bot}_{\eta}(\sigma)=Read_{PA^{\infty,N,L,-}_{2,<r},\eta,\epsilon,\eta}$.
If $\mathcal{R}$ is anything other than Ax{η,∼η} then
$\mathrm{Inverse}^{\bot}_{\eta}(\sigma\mathcal{R})=\mathcal{R}$ and
$\mathrm{Inverse}^{\bot}_{\eta}(\sigma\mathcal{R}\iota)=Read_{PA^{\infty,N,L,-}_{2,<r},\eta,\epsilon\iota,\eta}$.

If $\mathcal{R}$ is Ax{η,∼η} then
$\mathrm{Inverse}^{\bot}_{\eta}(\sigma\mathcal{R})=True_{{\sim}\eta}$. ∎

######  Lemma 4.10 ($\wedge$ Inversion).

For any $\phi_{L},\phi_{R}$ and any $B\in\\{L,R\\}$ there is a locally defined
function $\mathrm{Inverse}^{\wedge}_{\phi_{L},\phi_{R},B}$ on
$PA^{\infty,N,L,-}_{2,<r}$ in $PA^{\infty,N,L}_{2,<r}$ with
$\Gamma(\mathrm{Inverse}^{\wedge}_{\phi_{L},\phi_{R},B})\subseteq\phi_{B};(\phi_{L}\wedge\phi_{R},\epsilon_{\bot},\phi_{L}\wedge\phi_{R})$.

###### Proof.

As always, we define $\mathrm{Inverse}^{\wedge}_{\phi_{L},\phi_{R},B}$ by
induction on $\sigma$. We set
$\mathrm{Inverse}^{\wedge}_{\phi_{L},\phi_{R},B}(\langle\rangle)=Read_{PA^{\infty,N,L,-}_{2,<r},\phi_{L}\wedge\phi_{R},\epsilon_{\bot},\phi_{L}\wedge\phi_{R}}$.

If
$\mathrm{Inverse}^{\wedge}_{\phi_{L},\phi_{R},B}(\sigma)=Read_{PA^{\infty,N,L,-}_{2,<r},\phi_{L}\wedge\phi_{R},\epsilon,\phi_{L}\wedge\phi_{R}}$
and $\mathcal{R}$ is anything other than I$\wedge_{\phi_{L}\wedge\phi_{R}}$
then
$\mathrm{Inverse}^{\wedge}_{\phi_{L},\phi_{R},B}(\sigma\mathcal{R})=\mathcal{R}$
and
$\mathrm{Inverse}^{\wedge}_{\phi_{L},\phi_{R},B}(\sigma\mathcal{R}\iota)=Read_{PA^{\infty,N,L,-}_{2,<r},\phi_{L}\wedge\phi_{R},\epsilon\iota,\phi_{L}\wedge\phi_{R}}$.

So suppose $\mathcal{R}$ is I$\wedge_{\phi_{L}\wedge\phi_{R}}$. Then we set
$\mathrm{Inverse}^{\wedge}_{\phi_{B}b}(\sigma\mathcal{R})=Read_{PA^{\infty,N,L,-}_{2,<r},\phi_{L}\wedge\phi_{R},\epsilon
B,\phi_{L}\wedge\phi_{R}}$. ∎

######  Lemma 4.11 ($\forall$ Inversion).

For any $\phi(x)$ and any $n$ there is a locally defined function
$\mathrm{Inverse}^{\forall}_{\phi,x,n}$ on $PA^{\infty,N,L,-}_{2,<r}$ in
$PA^{\infty,N,L}_{2,<r}$ with
$\Gamma(\mathrm{Inverse}^{\forall}_{\phi,x,n})\subseteq\phi(n);(\forall
x\,\phi,\epsilon_{\bot},\forall x\,\phi)$.

###### Proof.

We set
$\mathrm{Inverse}^{\forall}_{\phi,x,n}(\langle\rangle)=Read_{PA^{\infty,N,L,-}_{2,<r},\forall
x\,\phi,\epsilon_{\bot},\forall x\,\phi}$.

If
$\mathrm{Inverse}^{\forall}_{\phi,x,n}(\sigma)=Read_{PA^{\infty,N,L,-}_{2,<r},\forall
x\,\phi,\epsilon,\forall x\,\phi}$ and $\mathcal{R}$ is anything other than
$\omega_{\forall x\,\phi}$ then
$\mathrm{Inverse}^{\forall}_{\phi,x,n}(\sigma\mathcal{R})=\mathcal{R}$ and
$\mathrm{Inverse}^{\forall}_{\phi,x,n}(\sigma\mathcal{R}\iota)=Read_{PA^{\infty,N,L,-}_{2,<r},\forall
x\,\phi,\epsilon\iota,\forall x\,\phi}$.

So suppose $\mathcal{R}$ is $\omega_{\forall x\,\phi}$. Then we set
$\mathrm{Inverse}^{\forall}_{\phi,x,n}(\sigma\mathcal{R})=Read_{PA^{\infty,N,L,-}_{2,<r},\forall
x\,\phi,\epsilon n,\forall x\,\phi}$. ∎

######  Lemma 4.12 ($\vee$ Elimination).

For any $\phi_{0},\phi_{1}$ there is a locally defined function
$\mathrm{Elim}^{\vee}_{\phi_{0},\phi_{1}}$ on $PA^{\infty,N,L,-}_{2,<r}$ in
$PA^{\infty,N,L}_{2,<r}$ with
$\Gamma(\mathrm{Elim}^{\vee}_{\phi_{0},\phi_{1}})\subseteq(\phi_{0}\vee\phi_{1},\epsilon_{\bot},\phi_{0}\vee\phi_{1}),({\sim}\phi_{0}\wedge{\sim}\phi_{1},\epsilon_{\bot},{\sim}\phi_{0}\wedge{\sim}\phi_{1})$.

###### Proof.

We set
$\mathrm{Elim}^{\vee}_{\phi_{0},\phi_{1}}(\langle\rangle)=Read_{PA^{\infty,N,L,-}_{2,<r},\phi_{0}\vee\phi_{1},\epsilon_{\bot},\phi_{0}\vee\phi_{1}}$.

If
$\mathrm{Elim}^{\vee}_{\phi_{0},\phi_{1}}(\sigma)=Read_{PA^{\infty,N,L,-}_{2,<r},\phi_{0}\vee\phi_{1},\epsilon,\phi_{0}\vee\phi_{1}}$
and $\mathcal{R}$ is anything other than I$\vee_{\phi_{0}\vee\phi_{1}}$,
$\mathrm{Elim}^{\vee}_{\phi_{0},\phi_{1}}(\sigma\mathcal{R})=\mathcal{R}$ and
$\mathrm{Elim}^{\vee}_{\phi_{0},\phi_{1}}(\sigma\mathcal{R}\iota)=Read_{PA^{\infty,N,L,-}_{2,<r},\phi_{0}\vee\phi_{1},\epsilon\iota,\phi_{0}\vee\phi_{1}}$.

If $\mathcal{R}$ is I$\vee^{B}_{\phi_{0}\vee\phi_{1}}$ then
$\mathrm{Elim}^{\vee}_{\phi_{0},\phi_{1}}(\sigma\mathcal{R})=Cut_{\phi_{B}}$,
$\mathrm{Elim}^{\vee}_{\phi_{0},\phi_{1}}(\sigma\mathcal{R}0)=Read_{PA^{\infty,N,L,-}_{2,<r},\phi_{0}\vee\phi_{1},\epsilon\top,\phi_{0}\vee\phi_{1}}$,
and for all $\tau$,
$\mathrm{Elim}^{\vee}_{\phi_{0},\phi_{1}}(\sigma\mathcal{R}1\tau)=\mathrm{Inverse}^{\wedge}_{\phi_{0},\phi_{1},B}(\tau)$.
∎

######  Lemma 4.13 ($\exists$ Elimination).

For any $\phi(x)$ there is a locally defined function
$\mathrm{Elim}^{\forall}_{\phi,x}$ on $PA^{\infty,N,L,-}_{2,<r}$ in
$PA^{\infty,N,L}_{2,<r}$ with
$\Gamma(\mathrm{Elim}^{\forall}_{\phi,x})\subseteq(\exists
x\,\phi,\epsilon_{\bot},\exists x\,\phi),(\forall
x\,{\sim}\phi,\epsilon_{\bot},\forall x\,{\sim}\phi)$.

###### Proof.

We set
$\mathrm{Elim}^{\forall}_{\phi,x}(\langle\rangle)=Read_{PA^{\infty,N,L,-}_{2,<r},\exists
x\,\phi,\epsilon_{\bot},\exists x\,\phi}$.

If
$\mathrm{Elim}^{\forall}_{\phi,x}(\sigma)=Read_{PA^{\infty,N,L,-}_{2,<r},\exists
x\,\phi,\epsilon,\exists x\,\phi}$ and $\mathcal{R}$ is anything other than
I$\exists_{\exists x\,\phi}$,
$\mathrm{Elim}^{\forall}_{\phi,x}(\sigma\mathcal{R})=\mathcal{R}$ and
$\mathrm{Elim}^{\forall}_{\phi,x}(\sigma\mathcal{R}\iota)=Read_{PA^{\infty,N,L,-}_{2,<r},\exists
x\,\phi,\epsilon\iota,\exists x\,\phi}$.

If $\mathcal{R}$ is I$\exists^{n}_{\exists x\,\phi}$ then
$\mathrm{Elim}^{\forall}_{\phi,x}(\sigma\mathcal{R})=Cut_{\phi_{0}}$,
$\mathrm{Elim}^{\forall}_{\phi,x}(\sigma\mathcal{R}0)=Read_{PA^{\infty,N,L,-}_{2,<r},\exists
x\,\phi,\epsilon\top,\exists x\,\phi}$, and, for all $\tau$,
$\mathrm{Elim}^{\forall}_{\phi,x}(\sigma\mathcal{R}1\tau)=\mathrm{Inverse}^{\forall}_{{\sim}\phi,x,n}(\tau)$.
∎

The next two elimination steps don’t have inversion lemmas, so we have do a
two sided process where we work our way back to introduction rules on both
sides.

######  Lemma 4.14 ($X^{\ell}$ Elimination).

For any $X^{\ell}$, $m$ there is a locally defined function
$\mathrm{Elim}^{X}_{X^{\ell},m}$ on $PA^{\infty,N,L,-}_{2,<r}$ in
$PA^{\infty,N,L}_{2,<r}$ with
$\Gamma(\mathrm{Elim}^{X}_{X^{\ell},m})\subseteq(X^{\ell}m,\epsilon_{\bot},X^{\ell}m),(\neg
X^{\ell}m,\epsilon_{\bot},\neg X^{\ell}m)$.

###### Proof.

We arbitrarily choose to proceed down the $X^{\ell}m$ branch first, so we set
$\mathrm{Elim}^{X}_{X^{\ell},m}(\langle\rangle)=Read_{PA^{\infty,N,L,-}_{2,<r},X^{\ell}m,\epsilon_{\bot},X^{\ell}m}$.

Suppose
$\mathrm{Elim}^{X}_{X^{\ell},m}(\sigma)=Read_{PA^{\infty,N,L,-}_{2,<r},X^{\ell}m,\epsilon,X^{\ell}m}$.
If $\mathcal{R}$ is anything other than $Ax_{\\{X^{\ell}m,\neg X^{\ell}m\\}}$
then $\mathrm{Elim}^{X}_{X^{\ell},m}(\sigma\mathcal{R})=\mathcal{R}$ and
$\mathrm{Elim}^{X}_{X^{\ell},m}(\sigma\mathcal{R}\iota)=Read_{PA^{\infty,N,L,-}_{2,<r},X^{\ell}m,\epsilon\iota,X^{\ell}m}$.

If $\mathcal{R}$ is $Ax_{\\{X^{\ell}m,\neg X^{\ell}m\\}}$ then
$\mathrm{Elim}^{X}_{X^{\ell},m}(\sigma\mathcal{R})=Read_{PA^{\infty,N,L,-}_{2,<r},\neg
X^{\ell}m,\epsilon_{\bot},\neg X^{\ell}m}$.

If
$\mathrm{Elim}^{X}_{X^{\ell},m}(\sigma)=Read_{PA^{\infty,N,L,-}_{2,<r},X^{\ell}m,\epsilon,X^{\ell}m}$
then, for any $\mathcal{R}$,
$\mathrm{Elim}^{X}_{X^{\ell},m}(\sigma\mathcal{R})=\mathcal{R}$ and
$\mathrm{Elim}^{X}_{X^{\ell},m}(\sigma\mathcal{R}\iota)=Read_{PA^{\infty,N,L,-}_{2,<r},\neg
X^{\ell}m,\epsilon\iota,\neg X^{\ell}m}$. ∎

######  Lemma 4.15 ($Q^{2}$ Elimination).

For any $\phi$ there is a locally defined function
$\mathrm{Elim}^{Q^{2}}_{\phi,X}$ on $PA^{\infty,N,L,-}_{2,<r}$ in
$PA^{\infty,N,L}_{2,<r}$ with
$\Gamma(\mathrm{Elim}^{Q^{2}}_{\phi,X})\subseteq(\forall^{2}X\,\phi,\epsilon_{\bot},\forall^{2}X\,\phi),(\exists^{2}X\,{\sim}\phi,\epsilon_{\bot},\exists^{2}X\,{\sim}\phi)$.

###### Proof.

Arbitrarily, we choose to pass down the $\forall^{2}$ branch first, so we set
$\mathrm{Elim}^{Q^{2}}_{\phi,X}(\langle\rangle)=Read_{PA^{\infty,N,L,-}_{2,<r},\forall^{2}X\,\phi,\epsilon_{\bot},\forall^{2}X\,\phi}$.
We keep track of additional values $\epsilon(\sigma)$ and
$\epsilon^{\prime}(\sigma)$; initially
$\epsilon(\langle\rangle)=\epsilon^{\prime}(\langle\rangle)=\langle\rangle$.

Suppose
$\mathrm{Elim}^{Q^{2}}_{\phi,X}(\sigma)=Read_{PA^{\infty,N,L,-}_{2,<r},\forall^{2}X\,\phi,\epsilon,\forall^{2}X\,\phi}$.
If $\mathcal{R}$ is anything other than
I$\forall^{\\{Y^{\ell}\\}}_{\forall^{2}X\,\phi}$ then
$\mathrm{Elim}^{Q^{2}}_{\phi,X}(\sigma\mathcal{R})=\mathcal{R}$ and
$\mathrm{Elim}^{Q^{2}}_{\phi,X}(\sigma\mathcal{R}\iota)=Read_{PA^{\infty,N,L,-}_{2,<r},\forall^{2}X\,\phi,\epsilon\iota,\forall^{2}X\,\phi}$.
Set $\epsilon(\sigma\mathcal{R}\iota)=\epsilon(\sigma)\iota$ and
$\epsilon^{\prime}(\sigma\mathcal{R}\iota)=\epsilon^{\prime}(\sigma)$.

If $\mathcal{R}$ is I$\forall^{Y^{\ell}}_{\forall^{2}X\,\phi}$ then
$\mathrm{Elim}^{Q^{2}}_{\phi,X}(\sigma\mathcal{R})=Read_{PA^{\infty,N,L,-}_{2,<r},\exists^{2}X\,{\sim}\phi,\epsilon^{\prime}(\sigma),\exists^{2}X\,{\sim}\phi}$.
We set $\epsilon(\sigma\mathcal{R})=\epsilon(\sigma)$ and
$\epsilon^{\prime}(\sigma\mathcal{R})=\epsilon^{\prime}(\sigma)$.

If
$\mathrm{Elim}^{Q^{2}}_{\phi,X}(\sigma)=Read_{PA^{\infty,N,L,-}_{2,<r},\exists^{2}X\,{\sim}\phi,\epsilon^{\prime},\exists^{2}X\,{\sim}\phi}$
and $\mathcal{R}$ is anything other than
$\Omega^{\flat}_{\mathfrak{T},Y^{\ell},\exists^{2}X\,{\sim}\phi}$ then
$\mathrm{Elim}^{Q^{2}}_{\phi,X}(\sigma\mathcal{R})=\mathcal{R}$ and
$\mathrm{Elim}^{Q^{2}}_{\phi,X}(\sigma\mathcal{R}\iota)=Read_{PA^{\infty,N,L,-}_{2,<r},\exists^{2}X\,{\sim}\phi,\epsilon^{\prime}\iota,\exists^{2}X\,{\sim}\phi}$.
In this case we set $\epsilon(\sigma\mathcal{R}\iota)=\epsilon(\sigma)$ and
$\epsilon^{\prime}(\sigma\mathcal{R}\iota)=\epsilon^{\prime}(\iota)$.

If $\mathcal{R}$ is
$\Omega^{\flat}_{\mathfrak{T},Y^{\ell},\exists^{2}X\,{\sim}\phi}$ then we set
$\mathrm{Elim}^{Q^{2}}_{\phi,X}(\sigma\mathcal{R})=Cut\Omega^{\flat}_{\mathfrak{T},Z^{\ell}(\sigma),Y^{\ell},\exists^{2}X\,{\sim}\phi}$.
We set
$\mathrm{Elim}^{Q^{2}}_{\phi,X}(\sigma\mathcal{R}\top)=Read_{PA^{\infty,N,L,-}_{2,<r},\forall^{2}X\,\phi,\epsilon(\sigma)\top,\forall^{2}X\,\phi}$
and
$\mathrm{Elim}^{Q^{2}}_{\phi,X}(\sigma\mathcal{R}\bot)=Read_{PA^{\infty,N,L,-}_{2,<r},\exists^{2}X\,{\sim}\phi,\epsilon^{\prime}(\sigma)\bot,\exists^{2}X\,{\sim}\phi}$.
We set $\epsilon(\sigma\mathcal{R}\top)=\epsilon(\sigma)\ell$,
$\epsilon^{\prime}(\sigma\mathcal{R}\top)=\epsilon^{\prime}(\sigma)$,
$\epsilon(\sigma\mathcal{R}\bot)=\epsilon(\sigma)$, and
$\epsilon^{\prime}(\sigma\mathcal{R}\bot)=\epsilon^{\prime}(\sigma)\bot$. ∎

######  Theorem 4.16.

There is a locally defined function $\mathrm{Reduce}_{r}$ on
$PA^{\infty,N,L,-}_{2,<r+1}$ in $PA^{\infty,N,L}_{2,<r}$ with
$\Gamma(\mathrm{Reduce}_{r})\subseteq(\emptyset,\epsilon_{\bot},\emptyset)$.

###### Proof.

The natural way to describe this function is coinductively. For any
$\epsilon$, we can describe the operation starting at position $\epsilon$, and
we do this simultaneously for all $\epsilon$, using the operations defined
above.

We define $\mathrm{Reduce}_{r,\epsilon}(\langle\rangle)$ to be
Read${}_{PA^{\infty,N,L,-}_{2,<r+1},\emptyset,\epsilon,\emptyset}$. Suppose we
have defined $\mathrm{Reduce}_{r,\epsilon}(\sigma)$ to be
Read${}_{PA^{\infty,N,L,-}_{2,<r+1},\emptyset,\epsilon\epsilon^{\prime},\emptyset}$
and consider some $\mathcal{R}$.

If $\mathcal{R}$ is anything other than Cutϕ with $rk(\phi)=r$, we set
$\mathrm{Reduce}_{r,\epsilon}(\sigma\mathcal{R})=\mathcal{R}$ and
$\mathrm{Reduce}_{r,\epsilon}(\sigma\mathcal{R}\iota)=Read_{PA^{\infty,N,L,-}_{2,<r},\emptyset,\epsilon\epsilon^{\prime}\iota,\emptyset}$.

So suppose $\mathcal{R}$ is Cutϕ where $rk(\phi)=r$. We consider cases on
$\phi$. If $\phi$ is $\psi_{0}\wedge\psi_{1}$, we take
$\mathrm{Reduce}_{r,\epsilon}(\sigma\mathcal{R}\tau)$ to be
$\mathrm{Elim}^{\vee}_{{\sim}\psi_{0},{\sim}\psi_{1}}(\mathrm{Reduce}_{r,\epsilon
1},\mathrm{Reduce}_{r,\epsilon 0})(\tau)$. Similarly, if $\phi$ is
$\psi_{0}\vee\psi_{1}$, we take
$\mathrm{Reduce}_{r,\epsilon}(\sigma\mathcal{R}\tau)$ to be
$\mathrm{Elim}^{\vee}_{\psi_{0},\psi_{1}}(\mathrm{Reduce}_{r,\epsilon
0},\mathrm{Reduce}_{r,\epsilon 1})(\tau)$.

If $\phi$ is $\forall x\,\psi$, we take
$\mathrm{Reduce}_{r,\epsilon}(\sigma\mathcal{R}\tau)$ to be
$\mathrm{Elim}^{\exists}_{{\sim}\psi,x}(\mathrm{Reduce}_{r,\epsilon
1},\mathrm{Reduce}_{r,\epsilon 0})(\tau)$. Similarly, if $\phi$ is $\exists
x\,\psi$, we take $\mathrm{Reduce}_{r,\epsilon}(\sigma\mathcal{R}\tau)$ to be
$\mathrm{Elim}^{\exists}_{\psi,x}(\mathrm{Reduce}_{r,\epsilon
0},\mathrm{Reduce}_{r,\epsilon 1})(\tau)$.

If $\phi$ is a literal $\dot{R}t_{1}\cdots t_{m}$ then, since it is closed, it
is true or false, so we take
$\mathrm{Reduce}_{r,\epsilon}(\sigma\mathcal{R}\tau)$ to be
$\mathrm{Inverse}^{\bot}_{{\sim}\phi}(\mathrm{Reduce}_{r,\epsilon 1})(\tau)$
or $\mathrm{Inverse}^{\bot}_{\phi}(\mathrm{Reduce}_{r,\epsilon 0})(\tau)$
respectively.

If $\phi$ is a literal $X^{\ell}m$ then we take
$\mathrm{Reduce}_{r,\epsilon}(\sigma\mathcal{R}\tau)$ to be
$\mathrm{Elim}^{X}_{X^{\ell},n}(\mathrm{Reduce}_{r,\epsilon
0},\mathrm{Reduce}_{r,\epsilon 1})(\tau)$, and if $\phi$ is $\neg X^{\ell}m$
then we take $\mathrm{Reduce}_{r,\epsilon}(\sigma\mathcal{R}\tau)$ to be
$\mathrm{Elim}^{X}_{X^{\ell},n}(\mathrm{Reduce}_{r,\epsilon
1},\mathrm{Reduce}_{r,\epsilon 0})(\tau)$.

If $\phi$ is $\forall^{2}X\,\psi$ then we take
$\mathrm{Reduce}_{r,\epsilon}(\sigma\mathcal{R}\tau)$ to be
$\mathrm{Elim}^{Q^{2}}_{\phi,X}(\mathrm{Reduce}_{r,\epsilon
1},\mathrm{Reduce}_{r,\epsilon 0})(\tau)$, and if $\phi$ is
$\exists^{2}X\,\psi$ then we take
$\mathrm{Reduce}_{r,\epsilon}(\sigma\mathcal{R}\tau)$ to be
$\mathrm{Elim}^{Q^{2}}_{\phi,X}(\mathrm{Reduce}_{r,\epsilon
0},\mathrm{Reduce}_{r,\epsilon 1})(\tau)$.

We take $\mathrm{Reduce}_{r}$ to be $\mathrm{Reduce}_{r,\langle\rangle}$. ∎

######  Corollary 4.17.

If $d$ is a deduction in $PA^{\infty,N,L}_{2,<r}$ then there is a deduction
$d^{\prime}$ in $PA^{\infty,n}_{2,<0}$ with
$\Gamma(d^{\prime})\subseteq\Gamma(d)$.

###### Proof.

By Lemma 3.9, we may extend each $\mathrm{Reduce}_{i}$ to a function on
$PA^{\infty,N,L}_{2,<i+1}$. We therefore take
$d^{\prime}=\overline{\mathrm{Reduce}_{0}^{\uparrow}}(\cdots\overline{\mathrm{Reduce}_{r-1}^{\uparrow}}(d))$.
∎

###  4.4. Collapsing

The remaining step in a proof of cut-elimination is collapsing: showing that
we can remove Cut$\Omega^{\flat}$ inference rules in our deduction.

######  Theorem 4.18.

Let $d$ be a proof-tree in $PA^{\infty,N,L,m,\ell}_{2,<0}$ with $m+\ell>0$
such that

  * •

whenever $\exists^{2}X\,\phi$ appears as a subformula of a formula in
$\Gamma(d)$, $comp(\exists^{2}X\,\phi)<(m,\ell)$,

  * •

if $t\in\Gamma(d)_{\mathsf{t}}$ then
$comp(\exists^{2}X\,\Theta_{t})<(m,\ell)$.

Let $(m^{\prime},\ell^{\prime})$ be the predecessor of $(m,\ell)$. Then there
is a proof-tree $D_{m,\ell}(d)$ in
$PA^{\infty,N,L,m^{\prime},\ell^{\prime}}_{2,<0}$ with
$\Gamma(D_{m,\ell}(d))\subseteq\Gamma(d)$.

$D_{m,\ell}$ is, itself, essentially a locally defined function modulo some
technicalities about consecutive Read rules, but we do not need to represent
it as one, so skip the technicalities to represent it as one.

$d$ cannot contain $\Omega^{\flat}$ inferences of complexity $(m,\ell)$, so
the issue is collapsing Cut$\Omega^{\flat}$ inferences. When
$d(\langle\rangle)$ is a Cut$\Omega^{\flat}$ inference of complexity
$(m,\ell)$, we would like to view $d_{\langle\bot\rangle}$ as a locally
defined function on domain $PA^{\infty,N,L,m,\ell,-}_{2,<0}$. We should be
able to collapse $d_{\langle\top\rangle}$, giving us
$D_{m,\ell}(d_{\langle\top\rangle})$ in
$PA^{\infty,N,L,m^{\prime},\ell^{\prime}}_{2,<0}$. We can lift our function
$d_{\langle\bot\rangle}$ to this domain, so we should end up with
$D_{m,\ell}(\overline{d_{\langle\bot\rangle}^{\uparrow}}(D_{m,\ell}(d_{\langle\top\rangle})))$.
Composing, this is the same as
$\overline{D_{m,\ell}(d_{\langle\bot\rangle})^{\uparrow}}(D_{m,\ell}(d_{\langle\top\rangle}))$.
The steps below represent precisely this process.

The restrictions on $\Gamma(d)$ do not hold inductively—$d$ could contain a
Cut$\Omega^{\flat}$ with complexity $(m^{\prime},\ell^{\prime})<(m,\ell)$, and
then an $\Omega^{\flat}$ above that introducing a formula with complexity
$(m^{\prime\prime},\ell^{\prime\prime})$ where $\ell^{\prime}$ is high even
though $m^{\prime\prime}$ is low. However the restriction that the conclusion
of this $\Omega^{\flat}$ rule is a subformula of our low complexity
Cut$\Omega^{\flat}$ rule ensures that no $X^{\ell}$ appears free, which is all
we really need.

###### Proof.

Again, we need to define “collapsing above $\epsilon$” as well. We will define
$D_{m,\ell,\epsilon}(d)(\sigma)$ by induction on $\sigma$, maintaining, for
each $t$ in $\Gamma^{\leftarrow}(\sigma)$ with
$comp(\exists^{2}X\,\Theta_{t})=(m,\ell)$, a $\pi_{t,\epsilon}(\sigma)$ in
$\operatorname{dom}(d)$.

We initially set $h(\langle\rangle)=\epsilon$. Suppose we have defined
$h(\sigma)$; we now wish to define $D_{m,\ell}(d)(\sigma)$. If $d(h(\sigma))$
is anything other than a
Cut$\Omega^{\flat}_{Z^{\ell},Y^{\ell},\exists^{2}X\,\phi}$ with
$comp(\exists^{2}X\,\phi)=(m,\ell)$ or a ReadT,t with
$comp(\exists^{2}X\,\Theta_{t})=(m,\ell)$ then we set
$D_{m,\ell,\epsilon}(d)(\sigma)=d(h(\sigma))$ and, for each $\iota$,
$h(\sigma\iota)=h(\sigma)\iota$ and for each $t$,
$\pi_{t}(\sigma\iota)=\pi_{t}(\sigma)$.

Suppose $d(h(\sigma))$ is a
Cut$\Omega^{\flat}_{Z^{\ell},Y^{\ell},\exists^{2}X\,\phi}$ with
$comp(\exists^{2}X\,\phi)=(m,\ell)$. Then we set $D_{m,\ell}(d)(\sigma)=Rep$,
$h(\sigma\top)=h(\sigma)\bot$, and
$\pi_{{\sim}\phi,\langle\rangle,{\sim}\phi}(\sigma\top)=\sigma\bot$.

Suppose $d(h(\sigma))$ is some ReadT,t with
$comp(\exists^{2}X\,\Theta_{t})=(m,\ell)$. Let $\mathcal{R}$ be
$D_{m,\ell,\pi_{t,\epsilon}(\sigma)}(\epsilon_{t})$. If $\mathcal{R}$ belongs
to $PA^{\infty,N,L,m,\ell,-}_{2,<0}$ then we extend
$h(\sigma)=h(\sigma)\mathcal{R}$ and continue. Otherwise, we set
$D_{m,\ell,\epsilon}(d)(\sigma)$ to be the rule given by Definition 3.7 (that
is, $\mathcal{R}$ if $\mathcal{R}$ is not a Read rule, the modification of
$\mathcal{R}$ if $\mathcal{R}$ is a Read rule) and, for each $\iota$,
$h(\sigma\iota)=h(\sigma)Rep$.

We can then take $D_{m,\ell}(d)$ to be $D_{m,\ell,\langle\rangle}(d)$. ∎

Putting these results together gives the following.

######  Theorem 4.19.

If there is a deduction of an arithmetic sequent $\Gamma$ in $PA_{2}$ then,
for some $N,L$, there is a proof-tree $d$ in $PA_{2,<0}^{\infty,N,L,0,0}$ with
$\Gamma(d)\subseteq\Gamma$.

This is rather unsatisfying on its own since $d$ might be ill-founded. The
next section shows that we can improve this to a well-founded deduction.

##  5\. Ordinals, Qualitatively

To complete a proof of cut-elimination, we will need to restrict to our analog
of well-founded deductions—deductions with ordinal bounds, in the sense we now
introduce. In many cases, these bounds will be functions on ordinals, not
simply ordinals. In this section we carry out the “qualitative” part of the
argument, that is, the part that can be carried out without a formal ordinal
notation.

###  5.1. Functions on Ordinals

We consider certain _sorts_ :

  * •

$Ord$ is the sort of ordinals,

  * •

if $\theta,\theta^{\prime}$ are sorts then $\theta\rightarrow\theta^{\prime}$
is the sort of functions from sort $\theta$ to sort $\theta^{\prime}$,

  * •

if $I$ is a set and, for each $i\in I$, $\theta_{i}$ is a sort then
$\prod_{i\in I}\theta_{i}$ is a sort.

######  Definition 5.1.

When $f,g$ have the same sort, we define $f<g$ by induction on the sort:

  * •

if the sort of $f,g$ is $Ord$ then $f<g$ is the usual comparison of ordinals,

  * •

if $f,g$ have sort $\theta\rightarrow\theta^{\prime}$ then $f<g$ if there is
some $a$ of sort $\theta$ so that whenever $a<b$, $f(a)<g(a)$,

  * •

if $f,g$ have sort $\prod_{i\in I}\theta_{i}$ then $f<g$ if, for each $i\in
I$, $f_{i}<g_{i}$.

######  Lemma 5.2.

In every sort, pairs have common upper bounds and increasing chains have upper
bounds.

###### Proof.

Both proofs are by induction on sorts. The casse where the sort is Ord is
immediate, as are the cases of a product sort.

Consider a sort $\theta\rightarrow\theta^{\prime}$. Given $f,g$, we can use
the inductive hypothesis to define $h(a)$ to be an upper bound of $f(a),g(a)$
for each $a$ of sort $\theta$.

Suppose we have $f_{0}<f_{1}<\cdots$ in this sort. We choose an increasing
sequence so $a_{i}$ is such that $b>a_{i}$ implies $f_{i}(b)<f_{i+1}(b)$. (At
successors, we can use the common upper bound with $a_{i}$ to make sure
$a_{i}<a_{i+1}$, and at limits we can use the inductive hypothesis followed by
the common upper bound.) Finally, we use the inductive hypothesis, giving us
an $a$ so that whenever $b>a$, $f_{i}(b)<f_{i+1}(b)$ for all $i$. Then we
define $f$ arbitrarily except for $b>a$, and for $b>a$ we choose some
$f(b)>f_{i}(b)$ for all $i$ using the inductive hypothesis. ∎

######  Lemma 5.3.

Every sort is well-founded under $<$.

###### Proof.

By induction on sorts. The case where the sort is Ord is immediate, as is the
case of a product sort. For the function case, if we have
$f_{0}>f_{1}>\cdots$, we can, as in the previous lemma, choose an $a$ so that
$f_{i}(b)>f_{i+1}(b)$ for all $b>a$ and all $i$. But this gives us a
decreasing sequence contradicting the inductive hypothesis. ∎

###  5.2. Ordinal Bounds

######  Definition 5.4.

Let $\sigma$ be a $PA^{\infty,N,L,m,\ell}_{2,<r}$-sequence and let $T$ be a
set of tags. We define $\mathcal{T}_{T}(\sigma)$, the _open tags at $\sigma$_,
inductively by:

  * •

$\mathcal{T}_{T}(\langle\rangle)=\\{\top_{m^{\prime},\ell^{\prime}}\\}_{m^{\prime}<m,\ell^{\prime}\leq
L}\cup\\{t\in T\mid\mathsf{r}(t)=\\{\exists^{2}X\,\phi\\}\text{ where
}dp(\phi,\\{X\\})<m\\}$,

  * •

if $\mathcal{R}(\iota)$ is an $\Omega^{\flat}_{X^{\ell},\exists^{2}X\,\phi}$
rule with $dp(\phi,{X})<m$ then
$\mathcal{T}_{T}(\sigma\iota)=\mathcal{T}_{T}(\sigma)\cup\\{({\sim}\phi(X^{\ell}),\langle\rangle,{\sim}\phi(X^{\ell}))\\}$,

  * •

if $\mathcal{R}(\iota)$ is an
Cut$\Omega^{\flat}_{X^{\ell},\exists^{2}X\,\phi}$ rule with $dp(\phi,{X})<m$
and $\iota=\bot$ then
$\mathcal{T}_{T}(\sigma\iota)=\mathcal{T}_{T}(\sigma)\cup\\{({\sim}\phi(X^{\ell}),\langle\rangle,{\sim}\phi(X^{\ell}))\\}$,

  * •

if $\mathcal{R}(\iota)$ is a Readt rule with $t\in\mathcal{T}_{T}(\sigma)$
then
$\mathcal{T}_{T}(\sigma\iota)=\mathcal{T}_{T}(\sigma)\cup\\{\Delta_{\iota}(\mathcal{R}_{\iota})_{\mathsf{t}}\\}$,

  * •

otherwise $\mathcal{T}_{T}(\sigma\iota)=\mathcal{T}_{T}(\sigma)$.

The important fact is that we include each tag for which
$PA^{\infty,N,L,m,\ell}_{2,<r}$ contains Read rules which branch over the
theory. Importantly, we do _not_ include Root tags introduced at an $\Omega$
or Cut$\Omega$ for which the corresponding Read rules are not present. We also
include a “placeholder” tag $\top_{m^{\prime},\ell^{\prime}}$ for each theory
we might encounter tags for.

The extra tags $T$ account for the possibility that $\sigma$ belongs to a
locally defined function; $T$ will typically be $\Gamma(d)_{\mathsf{t}}$.

######  Definition 5.5.

When $\sigma\sqsubseteq\tau$, there is a function
$\pi:\mathcal{T}_{T}(\tau)\rightarrow\mathcal{T}_{T}(\sigma)$; for $t$ in
$\mathcal{T}(\tau)$, $\pi(t)$ is the $t^{\prime}\in\mathcal{T}_{T}(\sigma)$
with $\mathsf{r}(t^{\prime})=\mathsf{r}(t)$ and $\epsilon_{t^{\prime}}$
maximal so $\epsilon_{t^{\prime}}\sqsubseteq\epsilon_{t}$ if there is one, and
$\top_{comp(\mathsf{r}(t))}$ otherwise.

######  Definition 5.6.

When $T$ is a set of root tags and $\sigma$ is a
$PA^{\infty,N,L,m,\ell}_{2,<r}$-sequence, we define sorts
$\mathcal{O}^{\mathrm{prem}}_{T}(\sigma)$ and $\mathcal{O}_{T}(\sigma)$ by
setting $\mathcal{O}^{\mathrm{prem}}_{T}(\sigma)$ to be
$\prod_{t\in\mathcal{T}_{T}(\sigma)}\mathcal{O}_{T}(\epsilon(t))$ and
$\mathcal{O}_{T}(\sigma)$ to be
$\mathcal{O}_{T}^{\mathrm{prem}}(\sigma)\rightarrow Ord$.

Given $\sigma\sqsubset\tau$ and $f_{\sigma},f_{\tau}$ of sorts
$\mathcal{O}^{\mathrm{prem}}_{T}(\sigma)$,
$\mathcal{O}^{\mathrm{prem}}_{T}(\tau)$ respectively, we say
$f_{\tau}<f_{\sigma}$ if, for each $t\in\mathcal{T}(\tau)$:

  * •

if $\pi(t)=t$ then $(f_{\tau})_{t}\leq(f_{\sigma})_{t}$,

  * •

if $\pi(t)\neq t$ then $(f_{\tau})_{t}<(f_{\sigma})_{\pi(t)}$.

When $d$ is a deduction, an _ordinal bound on $d$_ is an assignment, to each
$\sigma\in\operatorname{dom}(d)$ so that $d(\sigma)$ is not a Read rule, of an
$o_{\sigma}^{d}$ of sort $\mathcal{O}_{\Gamma(d)_{\mathsf{t}}}(\sigma)$ such
that whenever $\sigma\sqsubset\tau$ and $f_{\tau}<f_{\sigma}$,
$o^{d}_{\tau}(f_{\tau})<o^{d}_{\sigma}(f_{\sigma})$.

When $m=0$, $\mathcal{T}_{T}(\sigma)=\emptyset$, so
$\mathcal{O}^{\mathrm{prem}}_{T}(\sigma)$ is always an empty product—that is,
a single point—and so $\mathcal{O}_{T}(\sigma)$ is an ordinal. That is, an
ordinal bound on a deduction in $PA^{\infty,N,L,0,\ell}_{2,<r}$ is precisely a
decreasing assignment of ordinals as usual.

When $m=1$, $\mathcal{T}_{T}(\sigma)$ is a set of tags for theories where
$m=0$, so $\mathcal{O}^{\mathrm{prem}}_{T}(\sigma)$ is an indexed collection
of ordinals. An ordinal bound therefore assigns, to each $\sigma$, a function
from (possibly several) ordinals to an ordinal. As we will see when analyzing
the cut-elimination operators below, these are familiar ordinal bounds on
functions—for instance, when $d$ is the $\mathrm{Reduce}$ operator, we will be
able to assign the function $\lambda\beta.\omega^{\beta}$ to each $\sigma$.

The decision to not assign bounds to Read rules reflects the fact that Read
rules are “ephemeral”—they will disappear as we evaluate functions. (This is
related to why we need to prohibit consecutive Reads, because we need to avoid
infinite branches in which no bounds get assigned.)

We adopt the convention that we write elements of
$\mathcal{O}^{\mathrm{prem}}_{T}(\sigma)\rightarrow Ord$ as ordinal terms
using variables indexed by $\mathcal{T}_{T}(\sigma)$. The variable indexed by
$\top_{m,\ell}$ is written $\Omega_{m,\ell}$. For instance, we will write
$\Omega_{0,1}^{4}+\Omega_{0,0}^{2}\cdot 2$ as an abbreviation for
$\lambda\Omega_{1,1}\lambda\Omega_{0,0}.\Omega_{0,1}^{4}+\Omega_{0,0}^{2}\cdot
2$.

This notation means the sort may need to be inferred from context—we could
also write $\Omega_{0,1}^{4}+\Omega_{0,0}^{2}\cdot 2$ for
$\lambda\Omega_{0,1}\lambda\Omega_{1,0}\lambda\Omega_{0,0}.\Omega_{0,1}^{4}+\Omega_{0,0}^{2}\cdot
2$.

When $|T|=1$, we will write $\beta$ for the unique variable indexed by $T$; in
the case $|T|>1$, we will attach subscripts to $\beta$ to indicate which
variable we mean.

Finally, when $t$ is a term of sort $\theta\rightarrow Ord$, and $f$ is a term
of type $Ord\rightarrow Ord$, we write $f(t)$ for $\lambda s.f(ts)$. For
instance, we write $t+2$ for $\lambda s.ts+2$.

The following comparison observation is useful. Suppose $o$ is an ordinal
bound on $d$ and $d(\langle\rangle)$ is Cut$\Omega^{\flat}$. We can view
$o_{\langle\bot\rangle}$ as a bound of sort
$\mathcal{O}_{T}(d_{\langle\top\rangle})\rightarrow\mathcal{O}_{T}(d)$, and
observe that, for any $\alpha$,
$o_{\langle\bot\rangle}(\alpha)<o_{\langle\rangle}$—the tag corresponding to
the Cut$\Omega^{\flat}$ rule is the only tag present in
$\mathcal{T}_{T}(\langle\bot\rangle)\setminus\mathcal{T}_{T}(\langle\rangle)$,
so if we assign the same values to all other tags then, as soon as we choose
$\Omega_{m,\ell}>\alpha$, the comparison requirement on an ordinal bound
ensures
$o_{\langle\bot\rangle}(\alpha,\\{\beta_{i}\\})<o_{\langle\rangle}(\\{\beta_{i}\\})$.

###  5.3. Assigning Ordinal Bounds

We next show that all the deductions and operations we have used so far can be
assigned ordinal bounds.

######  Lemma 5.7.

The locally defined function Idϕ has an ordinal bound given by
$o_{\sigma}=\beta$.

Note that, according to our notation above, this is assigning the identity
function $\lambda\beta.\beta$ (more precisely, we are assigning
$\lambda\\{\Omega_{m,\ell}\\}\lambda\beta.\beta$).

###### Proof.

We only need to check the comparison condition: suppose $\sigma\sqsubset\tau$
are in $\operatorname{dom}(\mathrm{Id}^{\phi})$ and neither is a Read rule.
Let
$\\{f^{\sigma}_{t}\\}_{t\in\mathcal{T}_{(\phi,\epsilon_{\bot},\phi)}(\sigma)}$
and $\\{f^{\tau}_{t}\\}_{t\in\mathcal{T}_{(\phi,\epsilon_{\bot},\phi)}(\tau)}$
be given. By construction, there is a Read rule with root $\\{\phi\\}$ between
$\sigma$ and $\tau$, so in particular $f^{\tau}_{\phi}<f^{\sigma}_{\phi}$, as
needed. ∎

######  Lemma 5.8.

For any closed formula $\phi$ there are $N,L$ large enough so that the proof-
tree $d_{\phi}$ has an ordinal bound $o^{d_{\phi}}$ with
$o^{d_{\phi}}_{\sigma}=\max\\{\Omega_{m,\ell}\\}+k$.

We could restrict the maximum to those $m,\ell$ so that $\phi$ contains a
subformula of the form $\exists^{2}X\,\psi$ with
$comp(\exists^{2}X\,\psi)=(m,\ell)$ (indeed, we could restrict to _maximal_
subformulas of this kind).

######  Lemma 5.9.

The locally defined function $F^{\phi,X^{\ell}\mapsto\psi}$ has an ordinal
bound given by
$o_{\sigma}=\beta(\\{\Omega_{m^{\prime},\ell^{\prime}}\\}_{m^{\prime}<m})$
where $\ell^{\prime}=lvl(\psi)$.

######  Lemma 5.10.

For any deduction $d$ in $PA_{2}$, the deduction
$d^{\infty}_{n_{1},\ldots,n_{a},\ell_{1},\ldots,\ell_{b}}$ has an ordinal
bound with $o^{d^{\infty}}_{\langle\rangle}$ bounded by an expression of the
form $\sum_{i}t_{i}$ where each $t_{i}$ is one of:

  * •

a finite number,

  * •

$\omega$,

  * •

an expression
$\Omega_{m,\ell}(\\{\Omega_{m^{\prime},\ell^{\prime}}\\}_{m^{\prime}<m})$ for
some $\ell,\ell^{\prime}$.

The bounds on the cut-elimination operators are standard.

######  Theorem 5.11.

  1. (1)

$\mathrm{Inverse}^{\bot}_{\eta}(\sigma)$ is bounded by $o_{\sigma}=\beta$,

  2. (2)

$\mathrm{Inverse}^{\wedge}_{\phi_{L},\phi_{R},B}$ is bounded by
$o_{\sigma}=\beta$,

  3. (3)

$\mathrm{Inverse}^{\forall}_{\phi,x,n}(\sigma)$ is bounded by
$o_{\sigma}=\beta$,

  4. (4)

$\mathrm{Elim}^{\vee}_{\phi_{0},\phi_{1}}(\sigma)$ is bounded by
$o_{\sigma}=\beta_{\wedge}+\beta_{\vee}$,

  5. (5)

$\mathrm{Elim}^{\forall}_{\phi,x}(\sigma)$ is bounded by
$o_{\sigma}=\beta_{\forall}+\beta_{\exists}$,

  6. (6)

$\mathrm{Elim}^{X}_{X^{\ell},m}(\sigma)$ is bounded by
$o_{\sigma}=\beta_{X}\\#\beta_{\neg X}$,

  7. (7)

$\mathrm{Elim}^{Q^{2}}_{\phi,X}(\sigma)$ is bounded by
$o_{\sigma}=\beta_{\forall^{2}}\\#\beta_{\exists^{2}}$,

  8. (8)

$\mathrm{Reduce}_{r}(\sigma)$ is bounded by $o_{\sigma}=\omega^{\beta}$.

###  5.4. Calculating Ordinal Bounds

Of course, our definitions have been set up to ensure that when we interpret a
proof as a function, its ordinal bounds can be calculated using the same
functions.

######  Theorem 5.12.

Let $F$ be a locally defined function on $PA^{\infty,N,L,m,\ell}_{2,<r}$ with
ordinal bound $o^{F}$ and $d$ a deduction in $PA^{\infty,N,L,m,\ell}_{2,<r}$
with ordinal bound $o^{d}$. Then $\bar{F}(d)$ has an ordinal bound given by
$o^{\bar{F}(d)}_{\sigma}=o^{F}_{h(\sigma)}(\\{o^{d}_{\epsilon(t)}\\}_{t\mid\mathsf{r}(t)=t_{F}})$.

###### Proof.

We need only check the comparison rule. Suppose $\sigma\sqsubset\tau$ and
$f_{\tau}<f_{\sigma}$. We can lift these to tuples
$f^{\prime}_{h(\tau)},f^{\prime}_{h(\sigma)}$ by
$(f^{\prime}_{h(\tau)})_{t}=(f_{\tau})_{t}$ for $t\in\mathcal{T}_{T}(\tau)$
and $(f^{\prime}_{h(\tau)})_{t}=o^{d}_{\epsilon_{t}}$ when
$\mathsf{r}(t)=t_{F}$, and similarly for $\sigma$. Then
$f^{\prime}_{h(\tau)}<f^{\prime}_{h(\sigma)}$, so
$o^{\bar{F}(d)}_{\tau}(f_{\tau})=o^{F}_{h(\tau)}(f_{h(\tau)},o^{d}_{\epsilon(\tau)})=o^{F}_{h(\tau)}(f^{\prime}_{h(\tau)})<o^{F}_{h(\sigma)}(f^{\prime}_{h(\sigma)})=o^{\bar{F}(d)}_{\sigma}(f_{\sigma})$.
∎

We have an additional issue: some of our functions have the “wrong” domains—we
defined the function on one domain, but need to use lifting to get it to the
domain it needs to operate on. We need to show that we can lift ordinal bounds
as well.

######  Theorem 5.13.

Let $F$ be a locally defined function with ordinal bound $o^{F}$ and let
$F^{\uparrow}$ be the lift. Then the the bound
$o^{F^{\uparrow}}_{\sigma}=o^{F}_{h(\sigma)}$ is an ordinal bound on
$F^{\uparrow}$.

###  5.5. Collapsing

######  Theorem 5.14.

Let $d$ be a proof-tree in $PA^{\infty,N,L,m,\ell}_{2,<0}$ with $m+\ell>0$
such that

  * •

whenever $\exists^{2}X\,\phi$ appears as a subformula of a formula in
$\Gamma(d)$, $comp(\exists^{2}X\,\phi)<(m,\ell)$,

  * •

if $t\in\Gamma(d)_{\mathsf{t}}$ then
$comp(\exists^{2}X\,\Theta_{t})<(m,\ell)$.

If $d$ has an ordinal bound then $D_{m,\ell}(d)$ has an ordinal bound.

###### Proof.

We proceed by induction on the ordinal bound $o^{d}_{\langle\rangle}$. If the
last inference rule of $d$ is anything other than $\Omega^{\flat}$,
Cut$\Omega^{\flat}$ then the claim follows immediately from the inductive
hypothesis. (We will not encounter Read rules at complexity $(m,\ell)$, as we
will see below.)

If the last inference is a Cut$\Omega^{\flat}$ with complexity $(m,\ell)$, we
can use the fact that in this case, $D_{m,\ell}(d)$ is
$D_{m,\ell}(\overline{d_{\langle\bot\rangle}^{\uparrow}}(D_{m,\ell}(d_{\langle\top\rangle})))$.
The inductive hypothesis gives us an ordinal bound on
$D_{m,\ell}(d_{\langle\top\rangle})$, and therefore the ordinal bound on
$\overline{d_{\langle\bot\rangle}^{\uparrow}}(D_{m,\ell}(d_{\langle\top\rangle}))$
is less than $o^{d}$, so the inductive hypothesis applies again.

Suppose that last inference is an $\Omega^{\flat}$ inference. For any
$d^{\prime}$ in $PA^{\infty,N,m^{\prime},\ell^{\prime}}_{2,<0}$, we have a
deduction $\overline{d_{\langle\bot\rangle}^{\uparrow}}(d^{\prime})$, and if
$d^{\prime}$ has an ordinal bound then
$\overline{d_{\langle\bot\rangle}^{\uparrow}}(d^{\prime})$ has an ordinal
bound below the ordinal bound of $d$, so the inductive hypothesis applies to
$\overline{d_{\langle\bot\rangle}}(d^{\prime})$.

Taking the observation that $D_{m,\ell}(d_{\langle\bot\rangle})$ is
$d^{\prime}\mapsto
D_{m,\ell}(\overline{d_{\langle\bot\rangle}^{\uparrow}}(d^{\prime}))$, we can
assign an ordinal bound to $D_{m,\ell}(d_{\langle\bot\rangle})$: for any
$\sigma$ we assign to $\sigma$ the bound mapping $o^{*}$ to the supremum, over
all $d^{\prime}$ with bound $o^{*}$, of the bound in
$D_{m,\ell}(\overline{d_{\langle\bot\rangle}^{\uparrow}}(d^{\prime}))=\overline{D_{m,\ell}(d_{\langle\bot\rangle})^{\uparrow}}(d^{\prime})$
of those $\tau$ with $h(\tau)=\sigma$.

The Cut$\Omega^{\flat}$ case is similar, taking into account the bound on
$d_{\langle\top\rangle}$ as well. ∎

######  Theorem 5.15.

If $PA_{2}\vdash\phi$ where $\phi$ is a $\Sigma_{1}$ formula then
$PA_{2,<0}\vdash\phi$. In particular, $PA_{2}$ is consistent.

###### Proof.

Suppose $PA_{2}\vdash\phi$. Theorem 4.7 gives us $n,L,r$ and a proof-tree
$d^{\infty}$ in $PA^{\infty,N,L}_{2,<r}$ so that
$\Gamma(d^{\infty})\subseteq\\{\phi\\}$. By Lemma 5.10 there are ordinal
bounds on $d^{\infty}$.

Consider the deduction
$d^{\prime}=\mathrm{Reduce}_{0}^{\uparrow}(\cdots\mathrm{Reduce}_{r-1}^{\uparrow}(d^{\infty})\cdots)$;
by Theorems 5.11 and 5.13, $d^{\prime}$ has an ordinal bound as well.

Finally, we let $d^{\prime\prime}=D_{0,0}(\cdots D_{n,L}(d^{\prime})\cdots)$.
By Theorem 5.14, $d^{\prime\prime}$ has ordinal bounds as well. Since
$d^{\prime\prime}$ is a deduction in $PA^{\infty,N,L,-}_{2,<0}$, an ordinal
bound on $d^{\prime\prime}$ is simply an assignment of ordinals:
$d^{\prime\prime}$ is well-founded.

Since $PA^{\infty,N,L,-}_{2,<0}$ satisfies the subformula property, the only
rules that can appear in $d^{\prime\prime}$ are True, Ax, I$\wedge$, I$\vee$,
I$\exists$, and Rep. Removing Rep rules leaves us with a deduction in
$PA_{2,<0}$. ∎

## References

  * [1] Ryota Akiyoshi and Grigori Mints  “An extension of the omega-rule”  In _Arch. Math. Logic_ 55.3-4, 2016, pp. 593–603  DOI: 10.1007/s00153-016-0482-y
  * [2] Toshiyasu Arai  “An ordinal analysis of $\Pi_{N}$-Collection”, 2024  arXiv:2311.12459 [math.LO]
  * [3] Jeremy Avigad  “Ordinal analysis without proofs”  In _Reflections on the foundations of mathematics (Stanford, CA, 1998)_ 15, Lect. Notes Log.  Assoc. Symbol. Logic, Urbana, IL, 2002, pp. 1–36
  * [4] Wilfried Buchholz  “Relating ordinals to proofs in a perspicuous way” Essays in honor of Solomon Feferman, Papers from the symposium held at Stanford University, Stanford, CA, December 11–13, 1998  In _Reflections on the foundations of mathematics (Stanford, CA, 1998)_ 15, Lect. Notes Log.  Urbana, IL: Assoc. Symbol. Logic, 2002, pp. 37–59
  * [5] Wilfried Buchholz and Kurt Schütte  “Proof theory of impredicative subsystems of analysis” 2, Studies in Proof Theory. Monographs  Bibliopolis, Naples, 1988, pp. 125
  * [6] Jean-Yves Girard  “$\Pi^{1}_{2}$-logic. I. Dilators”  In _Ann. Math. Logic_ 21.2-3, 1981, pp. 75–219 (1982)  DOI: 10.1016/0003-4843(81)90016-4
  * [7] Jean-Yves Girard  “Proof theory and logical complexity” 1, Studies in Proof Theory. Monographs  Bibliopolis, Naples, 1987, pp. 505
  * [8] G.. Mints  “Finite investigations of transfinite derivations”  In _Journal of Soviet Mathematics_ 10.4 Springer ScienceBusiness Media LLC, 1978, pp. 548–596  DOI: 10.1007/bf01091743
  * [9] Wolfram Pohlers  “Proof theory: The First Step into Impredicativity”, Universitext  Berlin, Germany: Springer, 2008
  * [10] Michael Rathjen  “The art of ordinal analysis”  In _International Congress of Mathematicians. Vol. II_ Eur. Math. Soc., Zürich, 2006, pp. 45–69
  * [11] Michael Rathjen  “The realm of ordinal analysis”  In _Sets and proofs (Leeds, 1997)_ 258, London Math. Soc. Lecture Note Ser.  Cambridge Univ. Press, Cambridge, 1999, pp. 219–279
  * [12] Kurt Schütte  “Beweistheoretische Erfassung der unerdlichen Induktion in der Zahlentheorie”  In _Math. Ann._ 122, 1951, pp. 369–389  DOI: 10.1007/BF01342849
  * [13] Henry Towsner  “Ordinal analysis by transformations”  In _Ann. Pure Appl. Logic_ 157.2-3, 2009, pp. 269–280  DOI: 10.1016/j.apal.2008.09.011