1611 LABEL:LastPageSep. 12, 2018Jan. 06, 2020

# On the logical complexity of cyclic arithmetic

Anupam Das  University of Birmingham, United Kindgdom<EMAIL_ADDRESS>
###### Abstract.

We study the logical complexity of proofs in cyclic arithmetic
($\mathsf{CA}$), as introduced by Simpson in [Sim17], in terms of quantifier
alternations of formulae occurring. Writing $\mathrm{C}{\Sigma}_{n}$ for (the
logical consequences of) cyclic proofs containing only ${\Sigma}_{n}$
formulae, our main result is that $\mathrm{I}{\Sigma}_{n+1}$ and
$\mathrm{C}{\Sigma}_{n}$ prove the same ${\Pi}_{n+1}$ theorems, for $n\geq 0$.
Furthermore, due to the ‘uniformity’ of our method, we also show that
$\mathsf{CA}$ and Peano Arithmetic ($\mathsf{PA}$) proofs of the same theorem
differ only exponentially in size.

The inclusion $\mathrm{I}{\Sigma}_{n+1}\subseteq\mathrm{C}{\Sigma}_{n}$ is
obtained by proof theoretic techniques, relying on normal forms and structural
manipulations of $\mathsf{PA}$ proofs. It improves upon the natural result
that $\mathrm{I}{\Sigma}_{n}\subseteq\mathrm{C}{\Sigma}_{n}$. The converse
inclusion, $\mathrm{C}{\Sigma}_{n}\subseteq\mathrm{I}{\Sigma}_{n+1}$, is
obtained by calibrating the approach of [Sim17] with recent results on the
reverse mathematics of Büchi’s theorem [KMPS19], and carefully specialising to
the case of cyclic proofs. These results improve upon the bounds on proof
complexity and logical complexity implicit in [Sim17] and [BT17b].

The uniformity of our method also allows us to recover a metamathematical
account of fragments of $\mathsf{CA}$; in particular we show that, for $n\geq
0$, the consistency of $\mathrm{C}{\Sigma}_{n}$ is provable in
$\mathrm{I}{\Sigma}_{n+2}$ but not $\mathrm{I}{\Sigma}_{n+1}$. As a result, we
show that certain versions of McNaughton’s theorem (the determinisation of
$\omega$-word automata) are not provable in $\mathsf{RCA}_{0}$, partially
resolving an open problem from [KMPS19].

###### Key words and phrases:

Cyclic proofs, Proof theory, Logical complexity, Peano arithmetic, Induction

The author is supported by a Marie Skłodowska-Curie fellowship, ERC project
753431.

##  1\. Introduction

_Cyclic_ and _non-wellfounded_ proofs have been studied by a number of authors
as an alternative to proofs by induction. This includes cyclic systems for
fragments of the modal $\mu$-calculus, e.g. [NW96, SD03, DHL06, DBHS16, Dou17,
AL17], structural proof theory for logics with fixed-points, e.g. [San02,
FS13, For14, BDS16], (automated) proofs of program termination in separation
logic, e.g. [BBC08, BDP11, RB17] and, in particular, cyclic systems for first-
order logic with inductive definitions, e.g. [Bro05, Bro06, BS07, BS11]. Due
to the somewhat implicit nature of invariants they define, cyclic systems can
be advantageous for metalogical analysis, for instance offering better
algorithms for proof search, e.g. [BGP12, DP17].

Cyclic proofs may be seen as more intuitively analogous to proofs by ‘infinite
descent’ than proofs by induction (see, e.g., [Sim17]); this subtle difference
is enough to make inductive invariants rather hard to generate from cyclic
proofs. Indeed it was recently shown that simulating cyclic proofs using
induction is not possible for some sub-arithmetic languages [BT17a], but
becomes possible once arithmetic reasoning is available [Sim17, BT17b].

_Cyclic arithmetic_ was proposed as a general subject of study by Simpson in
[Sim17]. Working in the language of arithmetic, it replaces induction by non-
wellfounded proofs with a certain ‘fairness’ condition on the infinite
branches. The advantage of this approach to infinite proof theory as opposed
to, say, infinite well-founded proofs via an $\omega$-rule (see, e.g.,
[Sch77]), is that it admits a notion of _finite proofs_ : those that have only
finitely many distinct subproofs, and so may be represented by a finite
(possibly cyclic) graph.

Cyclic arithmetic itself is to cyclic proofs what Peano arithmetic is to
traditional proofs: it provides a general framework in which many arguments
can be interpreted and/or proved in a uniform manner, and this is one reason
why it is an interesting subject of study. This is already clear from, say,
the results of [BT17b], where the study of cyclic proofs for first-order logic
with inductive definitions relied on an underlying arithmetic framework. We
elaborate further on this in Sect. 10.

### Contribution

In [Sim17], Simpson showed that Peano Arithmetic ($\mathsf{PA}$) is able to
simulate cyclic reasoning by proving the soundness of the latter in the
former. (The converse result is obtained much more easily.) Nonetheless,
several open questions remain from [Sim17], concerning constructivity,
normalisation, logical complexity and proof complexity for cyclic and non-
wellfounded proofs.

In this work we address the _logical complexity_ and _proof complexity_ of
proofs in Cyclic Arithmetic ($\mathsf{CA}$), as compared to $\mathsf{PA}$.
Namely, we study how quantifier alternation of proofs in one system compares
to that in the other, and furthermore how the size of proofs compare. Writing
$\mathrm{C}{\Sigma}_{n}$ for (the logical consequences of) cyclic proofs
containing only ${\Sigma}_{n}$ formulae, we show, for $n\geq 0$:

  1. (1)

$\mathrm{I}{\Sigma}_{n+1}\subseteq\mathrm{C}{\Sigma}_{n}$ over ${\Pi}_{n+1}$
theorems (Sect. 4, Thm. 8).

  2. (2)

$\mathsf{CA}$ and $\mathsf{PA}$ proofs of the same theorem differ only
exponentially in size (Sect. 6, Thm. 20).

  3. (3)

$\mathrm{C}{\Sigma}_{n}\subseteq\mathrm{I}{\Sigma}_{n+1}$ over all theorems
(Sect. 7, Thm. 23).

(1) is obtained by proof theoretic techniques, relying on normal forms and
structural manipulations of Peano Arithmetic proofs. It improves upon the
natural result that $\mathrm{I}{\Sigma}_{n}\subseteq\mathrm{C}{\Sigma}_{n}$,
although induces a non-elementary blowup in the size of proofs. (2) is
obtained via a certain ‘uniformisation’ of the approach of [Sim17]. In
particular, by specialising the key intermediate results to the case of cyclic
proofs, we are able to extract small $\mathsf{PA}$ proofs of some required
properties of infinite word automata from analogous ones in ‘second-order’
(SO) arithmetic. Finally, (3) is obtained by calibrating the argument of (2)
with recent results on the reverse mathematics of Büchi’s theorem [KMPS19],
allowing us to bound the logical complexity of proofs in the simulation.
Together, these results almost completely characterise the logical and proof
complexity theoretic strength of cyclic proofs in arithmetic, answering the
questions (ii) and (iii), Sect. 7 of [Sim17].

After demonstrating these results, we give a metamathematical analysis of
provability in cyclic theories, in particular showing that the consistency of
$\mathrm{C}{\Sigma}_{n}$ is provable in $\mathrm{I}{\Sigma}_{n+2}$ but not
$\mathrm{I}{\Sigma}_{n+1}$, by appealing to a form of _Gödel incompleteness_
for cyclic theories. We also use these observations to show that certain
formulations of McNaughton’s theorem, that every nondeterministic Büchi
automaton has an equivalent deterministic parity (or Rabin, Muller, etc.)
automaton, are not provable in the SO theory $\mathsf{RCA}_{0}$. This
partially resolves the question of the logical strength of McNaughton’s
theorem left open in [KMPS19].

### Structure of the paper

In Sects. 2 and 3 we introduce some preliminaries on Peano Arithmetic, proof
theory, cyclic proofs and automaton theory. In Sect. 4 we present (1) and give
an example of the translation in App. A. The contents of Sects. 2, 3 and 4 and
App. A are more-or-less self contained and should be accessible to the general
proof theorist.

We briefly introduce some SO theories of arithmetic in Sect. 5 that are
conservative over the fragments of $\mathsf{PA}$ we need in order to conduct
some of the intermediate arguments on infinite word automata. In Sect. 6 we
present (2), and in Sect. 7 we adapt the argument to obtain (3). In Sect. 8 we
give our metamathematical analysis of cyclic theories, and in Sect. 9 we
explain their consequences for the logical strength of certain forms of
McNaughton’s theorem. We conclude with some further remarks and perspectives
in Sect. 10, including a comparison with the results of [Sim17] and [BT17b].

For Sects. 5, 6, 7 and 9 it would be helpful for the reader to have some
background in subsystems of second-order arithmetic (see e.g. [Sim09, Hir14])
and $\omega$-automaton theory (see e.g. [Tho97]). For Sect. 8 it would be
helpful for the reader to have some background in the metamathematics of
first-order arithmetic (see e.g. [HP93]). Nonetheless we aim to give
sufficient details for the general proof theorist to appreciate all the
content herein.

##  2\. Preliminaries on first-order arithmetic proof theory

We present only brief preliminaries, but the reader is encouraged to consult,
e.g., [Bus98] for a more thorough introduction to first-order arithmetic.

We work in first-order (FO) logic with equality, $=$, with variables written
$x,y,z$ etc., terms written $s,t,u$ etc., and formulae written $\varphi,\psi$
etc., construed over the logical basis
$\\{\neg,\vee,\wedge,\exists,\forall\\}$. We will usually assume formulae are
in De Morgan normal form, with negation restricted to atomic formulae.
Nonetheless, we may write $\neg\varphi$ for the De Morgan ‘dual’ of $\varphi$,
defined as follows:

$\neg\neg\varphi:=\varphi\quad\begin{array}[]{rcl}\neg(\varphi\wedge\psi)&:=&\neg\varphi\vee\neg\psi\\\
\neg(\varphi\vee\psi)&:=&\neg\varphi\wedge\neg\psi\end{array}\quad\begin{array}[]{rcl}\neg\forall
x.\varphi&:=&\exists x.\neg\varphi\\\ \neg\exists x.\varphi&:=&\forall
x.\neg\varphi\end{array}$

We also write $\varphi\supset\psi$ for $\neg\varphi\vee\psi$ and
$\varphi\equiv\psi$ for $(\varphi\supset\psi)\wedge(\psi\supset\varphi)$.

FO logic has equality ‘built-in’, i.e. we always assume the following axioms
are present:

  1. (eq1)

$\forall x.x=x$.

  2. (eq2)

$\forall\vec{x},\vec{y}.((x_{1}=y_{1}\wedge\cdots\wedge x_{k}=y_{k})\supset
f(\vec{x})=f(\vec{y})$, for each $k\in\mathbb{N}$ and each function symbol $f$
of arity $k$.

  3. (eq3)

$\forall x,y.(((x_{1}=y_{1}\wedge\cdots\wedge x_{k}=y_{k})\wedge
P(\vec{x}))\supset P(\vec{y}))$, for each $k\in\mathbb{N}$ and each predicate
symbol $P$ of arity $k$.

Following [Sim17], the language of arithmetic (with inequality) is formulated
as $\\{0,\mathsf{s},+,\times,<\\}$, with their usual interpretations over
$\mathbb{N}$. A theory is a set $T$ of closed formulae over this language. We
write $T\vdash\varphi$ if $\varphi$ is a logical consequence of $T$. We write
$T_{1}\subseteq T_{2}$ if $T_{1}\vdash\varphi$ implies $T_{2}\vdash\varphi$,
and $T_{1}=T_{2}$ if $T_{1}\subseteq T_{2}$ and $T_{2}\subseteq T_{1}$.

The theory of Robinson arithmetic (with inequality), written $\mathsf{Q}$, is
axiomatised by:

  1. (Q1)

$\forall x.\mathsf{s}x\neq 0$.

  2. (Q2)

$\forall x,y.(\mathsf{s}x=\mathsf{s}y\supset x=y)$.

  3. (Q3)

$\forall x.(x\neq 0\supset\exists y.x=\mathsf{s}y)$.

  4. (Q4)

$\forall x.\ x+0=x$.

  5. (Q5)

$\forall x,y.\ x+\mathsf{s}y=\mathsf{s}(x+y)$.

  6. (Q6)

$\forall x.\ x\cdot 0=0$.

  7. (Q7)

$\forall x,y.\ x\cdot\mathsf{s}y=x\cdot y+x$.

  8. (Q8)

$\forall x,y.(x<y\equiv\exists z.(x+\mathsf{s}z=y))$

Notice that, above and elsewhere, we may write $\cdot$ instead of $\times$ in
terms, or even omit the symbol altogether, and we assume it binds more
strongly than $+$. We also write $\forall x<t.\varphi$ and $\exists
x<t.\varphi$ as abbreviations for $\forall x.(x<t\supset\varphi)$ and $\exists
x.(x<t\wedge\varphi)$ resp. Formulae with only such quantifiers are called
bounded.

As usual, we may assume that $\mathsf{Q}$ is axiomatised by the universal
closures of bounded formulae. In particular the existential quantifiers in
axioms (Q3) and (Q8) above may be bounded by $x$ and $y$ resp., provably under
quantifier-free induction. We will implicitly assume this bounded
axiomatisation for the sequent calculus formulation of arithmetic later.

######  Remark 1.

Our basic axioms and, later, our inference rules differ slightly from those in
[Sim17], however it is routine to see that the theories $\mathsf{PA}$ and
$\mathsf{CA}$ defined in this work coincide with those of [Sim17]. In
particular the axiomatisations are equivalent once even open induction is
present (this is weaker than any theory we will consider). We chose a slightly
different presentation so that we could readily apply certain metalogical
results, such as Thm. 3, with no intermediate proof manipulation.

[Arithmetical hierarchy] For $n\geq 0$, we define:

  * •

${\Delta}_{0}={\Pi}_{0}={\Sigma}_{0}$ is the class of bounded formulae.

  * •

${\Sigma}_{n+1}$ is the class of formulae of the form
$\exists\vec{x}.\varphi$, where $\varphi\in{\Pi}_{n}$.

  * •

${\Pi}_{n+1}$ is the class of formulae of the form $\forall\vec{x}.\varphi$,
where $\varphi\in{\Sigma}_{n}$.

Notice in particular that, by definition of De Morgan normal form, if
$\varphi\in{\Sigma}_{n}$ then $\neg\varphi\in{\Pi}_{n}$ and vice-versa. In
practice we often consider these classes of formulae up to logical
equivalence. We say that a formula is in ${\Delta}_{n}$ (in a theory $T$) if
it is equivalent (resp. provably equivalent in $T$) to both a ${\Sigma}_{n}$
and ${\Pi}_{n}$ formula.

[Arithmetic] Peano Arithmetic ($\mathsf{PA}$) is axiomatised by $\mathsf{Q}$
and the axiom schema of induction:

$(\varphi(0)\wedge\forall
x.(\varphi(x)\supset\varphi(\mathsf{s}x)))\supset\forall x.\varphi(x)$ (1)

For a class of formulae $\Phi$, we write $\Phi\text{-}\mathsf{IND}$ for the
set of induction axiom instances when $\varphi\in\Phi$ in (1). We write
$\mathrm{I}\Phi$ for the theory $\mathsf{Q}+\Phi\text{-}\mathsf{IND}$.

The following is a classical result:

######  Proposition 2 (See e.g. [Bus98, Kay91]).

For $n\geq 0$, we have $\mathrm{I}{\Sigma}_{n}=\mathrm{I}{\Pi}_{n}$.

###  2.1. A sequent calculus presentation of $\mathsf{PA}$

$\begin{array}[]{ccc}{\vbox{\hbox{\kern
8.61105pt\hbox{\vbox{\offinterlineskip\hbox{\kern
25.49992pt\hbox{\hbox{\hbox{$$}}}\kern 25.49992pt}\kern 1.43518pt\hbox{\hbox
to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\mathit{id}\;$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to50.99986pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}}\kern 1.43518pt\hbox{\hbox{\hbox{$\kern
0.0pt\hbox{$\Gamma,\varphi\Rightarrow\Delta,\varphi$}\kern 0.0pt$}}}}}\kern
0.0pt}}}&\ {\vbox{\hbox{\kern
12.99988pt\hbox{\vbox{\offinterlineskip\hbox{\kern
27.56934pt\hbox{\hbox{\hbox{$$}}}\kern 27.56934pt}\kern 1.43518pt\hbox{\hbox
to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle=_{1}\;$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to55.13867pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}}\kern 1.43518pt\hbox{\hbox{\hbox{$\kern
0.0pt\hbox{$\Gamma\Rightarrow\Delta,t=t$}\kern 0.0pt$}}}}}\kern 0.0pt}}}&\
{\vbox{\hbox{\kern 12.99988pt\hbox{\vbox{\offinterlineskip\hbox{\kern
77.46446pt\hbox{\hbox{\hbox{$$}}}\kern 77.46446pt}\kern 1.43518pt\hbox{\hbox
to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle=_{2}\;$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to154.92894pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}}\kern 1.43518pt\hbox{\hbox{\hbox{$\kern
0.0pt\hbox{$\Gamma,s_{1}=t_{1},\dots,s_{k}=t_{k}\Rightarrow\Delta,f(\vec{s})=f(\vec{t})$}\kern
0.0pt$}}}}}\kern 0.0pt}}}\\\ {\vbox{\hbox{\kern
13.67073pt\hbox{\vbox{\offinterlineskip\hbox{\kern
29.66658pt\hbox{\hbox{\hbox{$$}}}\kern 29.66658pt}\kern 1.43518pt\hbox{\hbox
to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\neg\text{-}l\;$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to59.33318pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}}\kern 1.43518pt\hbox{\hbox{\hbox{$\kern
0.0pt\hbox{$\Gamma,\varphi,\neg\varphi\Rightarrow\Delta$}\kern
0.0pt$}}}}}\kern 0.0pt}}}&\ {\vbox{\hbox{\kern
14.79689pt\hbox{\vbox{\offinterlineskip\hbox{\kern
30.22214pt\hbox{\hbox{\hbox{$$}}}\kern 30.22214pt}\kern 1.43518pt\hbox{\hbox
to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\neg\text{-}r\;$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to60.44429pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}}\kern 1.43518pt\hbox{\hbox{\hbox{$\kern
0.0pt\hbox{$\Gamma\Rightarrow\Delta,\varphi,\neg\varphi$}\kern
0.0pt$}}}}}\kern 0.0pt}}}&\ {\vbox{\hbox{\kern
12.99988pt\hbox{\vbox{\offinterlineskip\hbox{\kern
76.2457pt\hbox{\hbox{\hbox{$$}}}\kern 76.2457pt}\kern 1.43518pt\hbox{\hbox
to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle=_{3}\;$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to152.4914pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}}\kern 1.43518pt\hbox{\hbox{\hbox{$\kern
0.0pt\hbox{$\Gamma,s_{1}=t_{1},\dots,s_{k}=t_{k},P(\vec{s})\Rightarrow\Delta,P(\vec{t})$}\kern
0.0pt$}}}}}\kern 0.0pt}}}\end{array}$

$\begin{array}[]{ccc}{\vbox{\hbox{\kern
18.93605pt\hbox{\vbox{\offinterlineskip\hbox{\kern
12.47224pt\hbox{\hbox{\hbox{$\Gamma\Rightarrow\Delta$}}}\kern 12.47224pt}\kern
1.43518pt\hbox{\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\theta\text{-}\mathit{sub}\;$}}$}}\vbox{\vbox
to0.4pt{\vfill\hbox to55.0833pt{\hrulefill}\vfill}}\hbox
to0.0pt{\hbox{$\smash{\lower 0.0pt\hbox{$$}}$}\hss}}\kern
1.43518pt\hbox{\hbox{\hbox{$\kern
0.0pt\hbox{$\theta(\Gamma)\Rightarrow\theta(\Delta)$}\kern 0.0pt$}}}}}\kern
0.0pt}}}&\ {{}{}\vbox{\hbox{\kern
12.49995pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\hbox{\hbox{\hbox{$\Gamma\Rightarrow\Delta,\varphi$}}\kern
10.00002pt}\hbox{\hbox{$\Gamma,\varphi\Rightarrow\Delta$}}}}}\kern
1.43518pt\hbox{\kern 0.0pt\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\mathit{cut}\;$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to91.13869pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}\kern 0.0pt}\kern 1.43518pt\hbox{\kern
30.49994pt\hbox{\hbox{$\Gamma\Rightarrow\Delta$}}\kern 30.49994pt}}}\kern
0.0pt}}}&\ {\vbox{\hbox{\kern
11.52773pt\hbox{\vbox{\offinterlineskip\hbox{\kern
11.33168pt\hbox{\hbox{\hbox{$\Gamma\Rightarrow\Delta$}}}\kern 11.33168pt}\kern
1.43518pt\hbox{\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\mathit{wk}\;$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to52.80217pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}}\kern 1.43518pt\hbox{\hbox{\hbox{$\kern
0.0pt\hbox{$\Gamma,\Gamma^{\prime}\Rightarrow\Delta,\Delta^{\prime}$}\kern
0.0pt$}}}}}\kern 0.0pt}}}\end{array}$

$\begin{array}[]{cccc}{{}{}\vbox{\hbox{\kern
14.22627pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\hbox{\hbox{\hbox{$\Gamma,\varphi\Rightarrow\Delta$}}\kern
10.00002pt}\hbox{\hbox{$\Gamma,\psi\Rightarrow\Delta$}}}}}\kern
1.43518pt\hbox{\kern 0.0pt\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\vee\text{-}l\;$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to89.99982pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}\kern 0.0pt}\kern 1.43518pt\hbox{\kern
16.18054pt\hbox{\hbox{$\Gamma,\varphi\vee\psi\Rightarrow\Delta$}}\kern
16.18054pt}}}\kern 0.0pt}}}&{\vbox{\hbox{\kern
14.22627pt\hbox{\vbox{\offinterlineskip\hbox{\kern
9.55063pt\hbox{\hbox{\hbox{$\Gamma,\varphi_{i}\Rightarrow\Delta$}}}\kern
9.55063pt}\kern 1.43518pt\hbox{\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\wedge\text{-}l\;$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to58.2666pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}}\kern 1.43518pt\hbox{\hbox{\hbox{$\kern
0.0pt\hbox{$\Gamma,\varphi_{0}\wedge\varphi_{1}\Rightarrow\Delta$}\kern
0.0pt$}}}}}\kern 0.0pt}}}&{\vbox{\hbox{\kern
12.89296pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\hbox{$\Gamma,\varphi[a/x]\Rightarrow\Delta$}}}}\kern
1.43518pt\hbox{\kern 0.0pt\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\exists\text{-}l\;$}}$}}\vbox{\vbox
to0.4pt{\vfill\hbox to66.01486pt{\hrulefill}\vfill}}\hbox
to0.0pt{\hbox{$\smash{\lower 0.0pt\hbox{$$}}$}\hss}\kern 0.0pt}\kern
1.43518pt\hbox{\kern 4.3096pt\hbox{\hbox{$\kern 0.0pt\hbox{$\Gamma,\exists
x.\varphi\Rightarrow\Delta$}\kern 0.0pt$}}\kern 4.3096pt}}}\kern
0.0pt}}}&{\vbox{\hbox{\kern
12.89296pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\hbox{$\Gamma,\varphi[t/x]\Rightarrow\Delta$}}}}\kern
1.43518pt\hbox{\kern 0.0pt\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\forall\text{-}l\;$}}$}}\vbox{\vbox
to0.4pt{\vfill\hbox to64.34009pt{\hrulefill}\vfill}}\hbox
to0.0pt{\hbox{$\smash{\lower 0.0pt\hbox{$$}}$}\hss}\kern 0.0pt}\kern
1.43518pt\hbox{\kern 3.47221pt\hbox{\hbox{$\kern 0.0pt\hbox{$\Gamma,\forall
x.\varphi\Rightarrow\Delta$}\kern 0.0pt$}}\kern 3.47221pt}}}\kern 0.0pt}}}\\\
\vskip 6.0pt plus 2.0pt minus 2.0pt\cr{{}{}\vbox{\hbox{\kern
15.35243pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\hbox{\hbox{\hbox{$\Gamma\Rightarrow\Delta,\varphi$}}\kern
10.00002pt}\hbox{\hbox{$\Gamma\Rightarrow\Delta,\psi$}}}}}\kern
1.43518pt\hbox{\kern 0.0pt\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\wedge\text{-}r\;$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to92.22205pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}\kern 0.0pt}\kern 1.43518pt\hbox{\kern
16.7361pt\hbox{\hbox{$\Gamma\Rightarrow\Delta,\varphi\wedge\psi$}}\kern
16.7361pt}}}\kern 0.0pt}}}&{\vbox{\hbox{\kern
15.35243pt\hbox{\vbox{\offinterlineskip\hbox{\kern
9.55063pt\hbox{\hbox{\hbox{$\Gamma\Rightarrow\Delta,\varphi_{i}$}}}\kern
9.55063pt}\kern 1.43518pt\hbox{\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\vee\text{-}r\;$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to62.15543pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}}\kern 1.43518pt\hbox{\hbox{\hbox{$\kern
0.0pt\hbox{$\Gamma\Rightarrow\Delta,\varphi_{0}\vee\varphi_{1}$}\kern
0.0pt$}}}}}\kern 0.0pt}}}&{\vbox{\hbox{\kern
14.01912pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\hbox{$\Gamma\Rightarrow\Delta,\varphi[a/x]$}}}}\kern
1.43518pt\hbox{\kern 0.0pt\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\forall\text{-}r\;$}}$}}\vbox{\vbox
to0.4pt{\vfill\hbox to67.12598pt{\hrulefill}\vfill}}\hbox
to0.0pt{\hbox{$\smash{\lower 0.0pt\hbox{$$}}$}\hss}\kern 0.0pt}\kern
1.43518pt\hbox{\kern 4.3096pt\hbox{\hbox{$\kern
0.0pt\hbox{$\Gamma\Rightarrow\Delta,\forall x.\varphi$}\kern 0.0pt$}}\kern
4.3096pt}}}\kern 0.0pt}}}&{\vbox{\hbox{\kern
14.01912pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\hbox{$\Gamma\Rightarrow\Delta,\varphi[t/x]$}}}}\kern
1.43518pt\hbox{\kern 0.0pt\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\exists\text{-}r\;$}}$}}\vbox{\vbox
to0.4pt{\vfill\hbox to65.4512pt{\hrulefill}\vfill}}\hbox
to0.0pt{\hbox{$\smash{\lower 0.0pt\hbox{$$}}$}\hss}\kern 0.0pt}\kern
1.43518pt\hbox{\kern 3.47221pt\hbox{\hbox{$\kern
0.0pt\hbox{$\Gamma\Rightarrow\Delta,\exists x.\varphi$}\kern 0.0pt$}}\kern
3.47221pt}}}\kern 0.0pt}}}\end{array}$

Figure 1. The sequent calculus for FO logic with equality, where $a$ occurs
only as indicated and $i\in\\{0,1\\}$.

We will work with a standard sequent calculus presentation of FO logic, given
in Fig. 1, where $i\in\\{0,1\\}$ and $a$, known as the ‘eigenvariable’, is
fresh, i.e. does not occur free in the lower sequent. Two important
considerations are that we work with cedents as _sets_ , i.e. there is no
explicit need for contraction rules, and that we have an explicit substitution
rule. In the $\theta$-$\mathit{sub}$ rule the ‘substitution’ $\theta$ is a
mapping from variables to terms, which is extended in the natural way to
cedents. Substitution is important for the definition of a cyclic arithmetic
proof in the next section, but does not change provability in usual proofs.

The sequent calculus for $\mathsf{Q}$ is obtained from the FO calculus in the
language of arithmetic by adding appropriate initial sequents for each
instantiation of an axiom of $\mathsf{Q}$ by terms. For theories extending
$\mathsf{Q}$ by (at least quantifier-free) induction, we assume that these
intial sequents contain only ${\Delta}_{0}$ formulae by appropriately bounding
the existential quantifiers. The schema $\Phi\text{-}\mathsf{IND}$, for $\Phi$
closed under subformulas and substitution, is implemented in the calculus by
adding the induction rule,

$\Gamma\Rightarrow\varphi(0),\Delta$$\Gamma,\varphi(a)\Rightarrow\varphi(\mathsf{s}a),\Delta$
$\scriptstyle\mathit{ind}\;$ $\Gamma\Rightarrow\varphi(t),\Delta$

for formulae $\varphi\in\Phi$. Here we require $a$ to not occur free in the
lower sequent. Notice that this satisfies the subformula property, in the
‘wide’ sense of FO logic, i.e. up to substitution. For fragments of
$\mathsf{PA}$ with induction axioms of bounded logical complexity, we also
have the _bounded quantifier rules_ :

$\begin{array}[]{cc}{\vbox{\hbox{\kern
0.0pt\hbox{\vbox{\offinterlineskip\hbox{\kern
4.04048pt\hbox{\hbox{\hbox{$\Gamma,a<s,\varphi(a)\Rightarrow\Delta$}}}\kern
4.04048pt}\kern 1.43518pt\hbox{\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to88.90945pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}}\kern 1.43518pt\hbox{\hbox{\hbox{$\kern
0.0pt\hbox{$\Gamma,\exists x<s.\varphi(x)\Rightarrow\Delta$}\kern
0.0pt$}}}}}\kern 0.0pt}}}&\quad{\vbox{\hbox{\kern
0.0pt\hbox{\vbox{\offinterlineskip\hbox{\kern
31.23595pt\hbox{\hbox{\hbox{$\Gamma\Rightarrow\Delta,\varphi(t)$}}}\kern
31.23595pt}\kern 1.43518pt\hbox{\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to114.9857pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}}\kern 1.43518pt\hbox{\hbox{\hbox{$\kern
0.0pt\hbox{$\Gamma,t<s\Rightarrow\Delta,\exists x<s.\varphi(x)$}\kern
0.0pt$}}}}}\kern 0.0pt}}}\\\ \vskip 12.0pt plus 4.0pt minus
4.0pt\cr{\vbox{\hbox{\kern 0.0pt\hbox{\vbox{\offinterlineskip\hbox{\kern
4.59604pt\hbox{\hbox{\hbox{$\Gamma,a<s\Rightarrow\Delta,\varphi(a)$}}}\kern
4.59604pt}\kern 1.43518pt\hbox{\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to90.02057pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}}\kern 1.43518pt\hbox{\hbox{\hbox{$\kern
0.0pt\hbox{$\Gamma\Rightarrow\Delta,\forall x<s.\varphi(x)$}\kern
0.0pt$}}}}}\kern 0.0pt}}}&\quad{\vbox{\hbox{\kern
0.0pt\hbox{\vbox{\offinterlineskip\hbox{\kern
31.7915pt\hbox{\hbox{\hbox{$\Gamma,\varphi(t)\Rightarrow\Delta$}}}\kern
31.7915pt}\kern 1.43518pt\hbox{\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to114.9857pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}}\kern 1.43518pt\hbox{\hbox{\hbox{$\kern
0.0pt\hbox{$\Gamma,t<s,\forall x<s.\varphi(x)\Rightarrow\Delta$}\kern
0.0pt$}}}}}\kern 0.0pt}}}\end{array}$

In all cases the eigenvariable $a$ occurs only as indicated,

The following normalisation result is well-known in the proof theory of
arithmetic, and will be one of the main structural proof theoretic tools in
this work:

######  Theorem 3 (Free-cut elimination, e.g. [Bus98]).

Let $\mathcal{S}$ be a sequent system extending FO by the induction rule and
some other nonlogical rules/axioms closed under substitution. Then any
$\mathcal{S}$-proof can be effectively transformed into one of the same
conclusion containing only (substitution instances of) subformulae of the
conclusion, an induction formula or a formula occurring in another nonlogical
step.

Naturally, this applies to the various fragments of $\mathsf{PA}$ that we
consider. In particular, notice that a free-cut free proof in
$\mathrm{I}{\Sigma}_{n}$ or $\mathrm{I}{\Pi}_{n}$ of sequents containing only
${\Sigma}_{n}$ or ${\Pi}_{n}$ formulae, resp., contains just ${\Sigma}_{n}$ or
${\Pi}_{n}$ formulae, resp. It is well known that Thm. 3 can itself be proved
within $\mathrm{I}{\Sigma}_{1}$ and even weaker theories (see, e.g., [HP93]),
under an appropriate coding of mathematical objects. We use this observation
later in Sect. 8.

We say that a sequent is ${\Sigma}_{n}$ (or ${\Pi}_{n}$) if it contains only
${\Sigma}_{n}$ (resp. ${\Pi}_{n}$) formulae. A slight issue that will be
relevant later in Sect. 4 is that we have not defined ${\Sigma}_{n}$ and
${\Pi}_{n}$ as being syntactically closed under positive Boolean combinations,
even if semantically we know that they are. In fact, this does not cause a
problem for the result above, since we can always prenex ‘on the fly’ in a
proof by cutting against appropriate derivations. For instance, in a proof, a
step of the form,

$\Gamma\Rightarrow\Delta,\forall x.\varphi$$\Gamma\Rightarrow\Delta,\forall
y.\psi$ $\scriptstyle\wedge\;$ $\Gamma\Rightarrow\Delta,\forall
x.\varphi\wedge\forall y.\psi$

may be locally replaced by a derivation of the form:

$\Gamma\Rightarrow\Delta,\forall x.\varphi$ $\Gamma\Rightarrow\Delta,\forall
y.\psi$ $\forall x.\varphi,\forall y.\psi\Rightarrow\forall
x,y.(\varphi\wedge\psi)$ $\scriptstyle\mathit{cut}\;$ $\Gamma,\forall
y.\psi\Rightarrow\Delta,\forall x,y.(\varphi\wedge\psi)$
$\scriptstyle\mathit{cut}\;$ $\Gamma\Rightarrow\Delta,\forall
x,y.(\varphi\wedge\psi)$

In a similar way we will often assume that a ‘block’ of existential or
universal quantifiers is coded by a single quantifier, using pairings and
Gödel $\beta$ functions, whose basic properties are all formalisable already
in $\mathrm{I}{\Delta}_{0}$ (see, e.g., [Bus98]).

##  3\. Preliminaries on cyclic arithmetic and automata

Before presenting ‘cyclic arithmetic’, we will present the general notion of
non-wellfounded proofs in arithmetic, from [Sim17].

By convention, we say _binary tree_ to mean a nonempty set
$T\subseteq\\{0,1\\}^{*}$ that is prefix-closed, i.e. if $\sigma i\in T$ then
$\sigma\in T$. We construe such $T$ as a bona fide tree with nodes $T$ and
directed edges from $\sigma$ to $\sigma i$, if $\sigma i\in T$, for
$i\in\\{0,1\\}$. The empty word, $\varepsilon$, is the _root_ of $T$. A
preproof is a possibly infinite binary tree labelled by sequents and rules in
a locally correct manner in the calculus for $\mathsf{Q}$. Following [Sim17],
we treat inference steps as nodes of the tree and sequents as edges. A
preproof is regular if it has only finitely many distinct (labelled) subtrees
or, equivalently, if it is the unfolding of a finite labelled directed graph,
possibly with cycles.

The following notions are variants of those from Dfns. 1 and 2 in [Sim17]:
[Precursors, traces, $\infty$-proofs] Let
$(\Gamma_{i}\Rightarrow\Delta_{i})_{i\geq 0}$ be an infinite branch through a
preproof. For terms $t,t^{\prime}$ we say that $t^{\prime}$ is a precursor of
$t$ at $i$ if one of the following holds:

  1. i)

$\Gamma_{i}\Rightarrow\Delta_{i}$ concludes a $\theta$-$\mathit{sub}$-step and
$t$ is $\theta(t^{\prime})$.

  2. ii)

$\Gamma_{i}\Rightarrow\Delta_{i}$ concludes any other step and $t^{\prime}=t$
occurs in $\Gamma_{i}$.

  3. iii)

$\Gamma_{i}\Rightarrow\Delta_{i}$ concludes any other step and $t^{\prime}$ is
$t$.

A trace along $(\Gamma_{i}\Rightarrow\Delta_{i})_{i\geq 0}$ is a sequence
$(t_{i})_{i\geq n}$, for some $n\geq 0$, such that whenever $i\geq n$ the term
$t_{i}$ occurs in $\Gamma_{i}\Rightarrow\Delta_{i}$ and,

  1. (a)

$t_{i+1}$ is a precursor of $t_{i}$ at $i$; or

  2. (b)

the atomic formula $t_{i+1}<t$ occurs in $\Gamma_{i+1}$, where $t$ is a
precursor of $t_{i}$ at $i$.

When (b) holds, we say that the trace progresses at $i+1$.

An $\infty$-proof is a preproof for which any infinite branch has a trace that
progresses infinitely often. If it is regular then we simply call it a cyclic
proof. $\mathsf{CA}$ is the theory induced by cyclic proofs in the calculus
for $\mathsf{Q}$.

######  Remark 4.

When defining explicit traces, for the precursor case iii), we will typically
not worry about whether the term $t_{i}$ in a trace occurs in the sequent or
not. All that matters is that, if the current step is $\exists\text{-}l$,
$\forall\text{-}r$ or $\mathit{sub}$, $t_{i}$ does not contain the associated
eigenvariables.111We say that $a$ is an eigenvariable of a
$\theta$-$\mathit{sub}$ step if it is in the support of the substitution
$\theta$. As long as we satisfy this constraint we may simply consider an
equivalent proof that prepends $t_{i}=t_{i}$ to the antecedent to make sure
that $t_{i}$ ‘occurs’. We use this assumption implicitly in the remainder of
this work.

The reader may consult [Sim17] for several examples of $\infty$-proofs.
Notably, $\infty$-proofs are sound and complete for the standard model
$\mathbb{N}$ (Thm. 4, [Sim17]). (Similar results for other logics, with
respect to standard models, were known before [Bro06, BS11].) We recall the
proof of soundness since we will have to formalise a variant of it in Sect. 6,
and also since the quantifier case in the argument of [Sim17] is omitted,
whereas this subtlety will need some consideration when it is formalised.

######  Proposition 5 (Soundness of $\infty$-proofs).

If $\pi$ is an $\infty$-proof of $\varphi$, then $\mathbb{N}\vDash\varphi$.

######  Proof 3.1.

Suppose otherwise, i.e. $\mathbb{N}\vDash\neg\varphi$. We will inductively
construct an infinite branch $(\Gamma_{i}\Rightarrow\Delta_{i})_{i\geq 0}$ of
$\pi$ and associated assignments $\rho_{i}$ of natural numbers to each
sequent’s free variables, such that
$\mathbb{N},\rho_{i}\nvDash\Gamma_{i}\Rightarrow\Delta_{i}$. Assuming
$\varphi$ is closed (by taking its universal closure), we set
$\Gamma_{0}\Rightarrow\Delta_{0}$ to be $\Rightarrow\varphi$ and
$\rho_{0}=\varnothing$.

Each step except for substitution, $\forall\text{-}r$ and $\exists\text{-}l$
constitutes a true implication, so if
$\mathbb{N},\rho_{i}\nvDash\Gamma_{i}\Rightarrow\Delta_{i}$ then $\rho_{i}$
also must not satisfy one of its premisses. We may thus choose one such
premiss as $\Gamma_{i+1}\Rightarrow\Delta_{i+1}$ and set
$\rho_{i+1}=\rho_{i}$.

If $\Gamma_{i}\Rightarrow\Delta_{i}$ concludes a $\theta$-$\mathit{sub}$ step,
we may set $\rho_{i+1}=\rho_{i}\circ\theta$. If
$\Gamma_{i}\Rightarrow\Delta_{i}$ concludes a $\forall\text{-}r$ step, let
$\forall x.\varphi$ be the principal formula and assume $x$ does not occur
free in the conclusion. Since
$\mathbb{N},\rho_{i}\nvDash\Gamma_{i}\Rightarrow\Delta_{i}$, we must have that
$\mathbb{N},\rho_{i}\vDash\exists x.\neg\varphi$. We choose a value
$k\in\mathbb{N}$ witnessing this existential and set
$\rho_{i+1}=\rho_{i}\cup\\{x\mapsto k\\}$. The $\exists\text{-}l$ case is
dealt with similarly.

This infinite branch must have an infinitely progressing trace, say
$(t_{i})_{i\geq n}$, by the definition of $\infty$-proof. However notice that,
for $i\geq n$, $\rho_{i}(t_{i})\geq\rho_{i+1}(t_{i+1})$ and, furthermore, at a
progress point along the trace, $\rho_{i}(t_{i})>\rho_{i+1}(t_{i+1})$. Thus,
$(\rho_{i}(t_{i}))_{i\geq n}$ is a monotone decreasing sequence of natural
numbers that does not converge, contradicting the fact that $\mathbb{N}$ is
well-ordered.

Later, in Sect. 6, we will use the fact that the choices for generating an
invalid branch in the proof above can be made _uniformly_ in an arithmetic
setting.

###  3.1. Defining $\mathrm{C}{\Sigma}_{n}$

Simpson proposes in [Sim17] to study systems of cyclic proofs containing only
${\Sigma}_{n}$ formulae, and to compare such systems to
$\mathrm{I}{\Sigma}_{n}$. This is rather pertinent in light of the free-cut
elimination result we stated, Thm. 3: any $\mathrm{I}{\Sigma}_{n}$-proof of a
${\Sigma}_{n}$-sequent can be assumed to contain just ${\Sigma}_{n}$ formulae
(possibly at a non-elementary cost in proof size), whence the comparison.
However, in order to be able to admit routine derivations of more complex
formulae, e.g. the ${\Sigma}_{n+1}$ law of excluded middle or the universal
closure of a ${\Sigma}_{n}$ sequent, we will close this notion under _logical
consequence_.

Let $\Phi$ be a set of formulae closed under subformulae and substitution.
$\mathrm{C}\Phi$ is the first-order theory axiomatised by the universal
closures of conclusions of cyclic proofs containing only $\Phi$-formulae.
Notice that, by the free-cut elimination result, Thm. 3, and the subformula
property, any $\mathrm{C}{\Sigma}_{n}$ proofs of ${\Sigma}_{n}$-sequents
contain only ${\Sigma}_{n}$-sequents anyway, without loss of generality. This
more ‘robust’ definition allows us to easily compare fragments of cyclic
arithmetic. For instance, we have the following:

######  Proposition 6.

$\mathrm{C}{\Sigma}_{n}=\mathrm{C}{\Pi}_{n}$, for $n\geq 0$.

######  Proof 3.2.

For the left-right inclusion, replace each ${\Sigma}_{n}$ sequent
$\vec{p},\Gamma\Rightarrow\Delta$ with the sequent
$\vec{p},\overline{\Delta}\Rightarrow\overline{\Gamma}$, where
$\overline{\Gamma}$ and $\overline{\Delta}$ contain the De Morgan dual
formulae of $\Gamma$ and $\Delta$ resp. and $\vec{p}$ exhausts the atomic
formulae of the antecedent. Any traces will be preserved and the proof can be
made correct by locally adding some logical steps. The converse implication is
proved in the same way.

Using a standard technique, e.g. from [Bro06], we also can rather simply show
the following result, which we will later strengthen in Sect. 4:222A similar
result was given in [Sim17], but that argument rather shows that
$\mathrm{I}{\Sigma}_{n}\subseteq\mathrm{C}{\Sigma}_{n+1}$.

######  Proposition 7.

$\mathrm{C}{\Sigma}_{n}$ proves any ${\Pi}_{n+1}$ theorem of
$\mathrm{I}{\Sigma}_{n}$, for $n\geq 0$.

######  Proof 3.3 (Proof sketch).

Suppose $\mathrm{I}{\Sigma}_{n}$ proves $\forall\vec{x}.\psi(\vec{x})$ where
$\varphi$ is ${\Sigma}_{n}$. Let $\pi$ be a free-cut free
$\mathrm{I}{\Sigma}_{n}$ proof of $\psi(\vec{a})$, so in particular contains
only ${\Sigma}_{n}$ formulas, by the subformula property. We may now construct
a $\mathrm{C}{\Sigma}_{n}$ proof of $\varphi(\vec{a})$ by simply simulating
every local inference step of $\pi$; the only nontrivial case is the induction
rule:

$\Gamma\Rightarrow\varphi(0),\Delta$$\Gamma,\varphi(a)\Rightarrow\varphi(\mathsf{s}a),\Delta$
$\scriptstyle\mathit{ind}\;$ $\Gamma\Rightarrow\varphi(t),\Delta$

This is simulated by the following cyclic derivation (omitting some routine
proof steps),

$\Gamma\Rightarrow\varphi(0),\Delta$ $\scriptstyle=\;$
$0=b,\Gamma\Rightarrow\varphi(b),\Delta$ $\vdots$ $\scriptstyle\mathit{cut}\;$
$\;\bullet$ $\Gamma\Rightarrow\varphi(b),\Delta$ $\scriptstyle\mathit{sub}\;$
$\Gamma\Rightarrow\varphi(a),\Delta$
$\Gamma,\varphi(a)\Rightarrow\varphi(\mathsf{s}a),\Delta$
$\scriptstyle\mathit{cut}\;$
$\underline{a<b},\Gamma\Rightarrow\varphi(\mathsf{s}a),\Delta$
$b=\mathsf{s}a,\Gamma\Rightarrow\varphi(b),\Delta$
$0<b,\Gamma\Rightarrow\varphi(b),\Delta$ $\scriptstyle\mathit{cut}\;$
$\;\bullet$ $\Gamma\Rightarrow\varphi(b),\Delta$ $\scriptstyle\mathit{sub}\;$
$\Gamma\Rightarrow\varphi(t),\Delta$

where we have written $\bullet$ to mark roots of identical subtrees. An
infinite branch that does not have a tail in the proofs of the two premisses
of $\mathit{ind}$ must eventually loop on $\bullet$. Therefore it admits an
infinitely progressing trace alternating between $a$ and $b$, with the
progress point underlined above. Now the proposition follows by simple
application of $\forall\text{-}r$.

Following Rmk. 4, notice that, e.g. in the simulation of induction above,
traces need not be connected in the graph of ancestry of a proof. This
deviates from other settings where it is _occurrences_ that are tracked,
rather than terms, e.g. in [DBHS16, BDS16, Dou17].

###  3.2. Büchi automata: checking correctness of cyclic proofs

A cyclic preproof can be effectively checked for correctness by reduction to
the inclusion of ‘Büchi automata’, yielding a $\mathbf{PSPACE}$ bound. As far
as the author is aware, this is the best known upper bound, although no
corresponding lower bound is known. As we will see later in Sect. 6, this is
one of the reasons why we cannot hope for a ‘polynomial simulation’ of cyclic
proofs in a usual proof system, and so why elementary simulations are more
pertinent.

A nondeterministic Büchi automaton (NBA) $\mathcal{A}$ is a tuple
$(A,Q,\delta,q_{0},F)$ where: $A$ is a finite set, called the alphabet, $Q$ is
a finite set of states, $\delta\subseteq(Q\times A)\times Q$ is the transition
relation, $q_{0}\in Q$ is the initial state, and $F\subseteq Q$ is the set of
final or accepting states. We say that $\mathcal{A}$ is deterministic (a DBA)
if $\delta$ is (the graph of) a function $Q\times A\to Q$. A ‘word’
$(a_{i})_{i\geq 0}\in A^{\omega}$ is accepted or recognised by $\mathcal{A}$
if there is a sequence $(q_{i})_{i\geq 0}\in Q^{\omega}$ such that: for each
$i\geq 0$, $(q_{i},a_{i},q_{i+1})\in\delta$, and for infinitely many $i\geq 0$
we have $q_{i}\in F$. We write $\mathcal{L}(\mathcal{A})$ for the set of words
in $A^{\omega}$ accepted by $\mathcal{A}$.

From a cyclic preproof $\pi$ we can easily define two automata, say
$\mathcal{A}^{\pi}_{b}$ and $\mathcal{A}^{\pi}_{t}$,333These are rather called
$B_{p}$ and $B_{t}$ respectively in [Sim17]. respectively accepting just the
infinite branches and just the infinite branches with infinitely progressing
traces. See [Sim17] for a construction of $\mathcal{A}^{\pi}_{t}$. We point
out that $\mathcal{A}^{\pi}_{b}$ is essentially just the dependency graph of
$\pi$ with all states final, and so is in fact deterministic;444Technically
the transition relation here is not total, but this can be ‘completed’ in the
usual way by adding a non-final ‘sink’ state for any outstanding transitions.
we will rely on this observation later in Sects. 6, 7 and 9. We now state the
well-known ‘correctness criterion’ for cyclic proofs:

[[Sim17]] A cyclic preproof $\pi$ is a $\infty$-proof iff
$\mathcal{L}(\mathcal{A}^{\pi}_{b})\subseteq\mathcal{L}(\mathcal{A}^{\pi}_{t})$.

##  4\. A translation from $\mathrm{I}{\Sigma}_{n+1}$ to
$\mathrm{C}{\Sigma}_{n}$, over ${\Pi}_{n+1}$-theorems

We show in this section our first result, that cyclic proofs containing only
${\Sigma}_{n}$-formulae are enough to simulate $\mathrm{I}{\Sigma}_{n+1}$ over
not-too-complex formulae:

######  Theorem 8.

$\mathrm{I}{\Sigma}_{n+1}\subseteq\mathrm{C}{\Sigma}_{n}$, over ${\Pi}_{n+1}$
theorems, for $n\geq 0$.

One example of such logical power in cyclic proofs was given in [Sim17], in
the form of $\mathrm{C}{\Sigma}_{1}$ proofs of the totality of the Ackermann-
Péter function. This already separates it from $\mathrm{I}{\Sigma}_{1}$, which
only proves the totality of the primitive recursive functions [Par72]. To
prove the theorem above, we will rather work in $\mathrm{I}{\Pi}_{n+1}$, cf.
Prop. 2, since the exposition is more intuitive. We first prove the following
intermediate lemma.

######  Lemma 9.

Let $\pi$ be a $\mathrm{I}{\Pi}_{n+1}$ proof, containing only ${\Pi}_{n+1}$
formulae, of a sequent,

$\Gamma,\forall x_{1}.\varphi_{1},\dots,\forall
x_{l}.\varphi_{l}\Rightarrow\Delta,\forall y_{1}.\psi_{1},\dots,\forall
y_{m}.\psi_{m}$ (2)

where $\Gamma,\Delta,\varphi_{i},\psi_{j}$ are ${\Sigma}_{n}$ and
$x_{i},y_{j}$ occur only in $\varphi_{i},\psi_{j}$ respectively. Then there is
a $\mathrm{C}{\Sigma}_{n}$ derivation $\lceil\pi\rceil$ of the form:

$\left\\{\Gamma\Rightarrow\Delta,\varphi_{i}\right\\}_{i\leq l}$
$\textstyle{\scriptstyle\lceil\pi\rceil}$
$\Gamma\Rightarrow\Delta,\psi_{1},\dots,\psi_{m}$

Moreover, no free variables of (2) occur as eigenvariables for
$\exists\text{-}l$, $\forall\text{-}r$ or $\mathit{sub}$ steps in
$\lceil\pi\rceil$.

######  Proof 4.1.

We proceed by induction on the structure of $\pi$. Notice that we may assume
that any ${\Pi}_{n+1}$ formulae occurring have just a single outermost
$\forall$ quantifier, by interpreting arguments as pairs and using Gödel’s
$\beta$ functions. (This introduces only cuts on formulae of the same form.)
We henceforth write $\vec{\varphi}$ for $\varphi_{1},\dots,\varphi_{l}$ and
$\vec{\psi}$ for $\psi_{1},\dots,\psi_{m}$ and, as an abuse of notation,
$\forall\vec{x}.\vec{\varphi}$ and $\forall\vec{y}.\vec{\psi}$ for $\forall
x_{1}.\varphi_{1},\dots,\forall x_{l}.\varphi_{l}$ and $\forall
y_{1}.\psi_{1},\dots,\forall y_{m}.\psi_{m}$ respectively. (Notice that this
is a reasonable abuse of notation, since $\forall$s can be prenexed outside
conjunctions and disjunctions already in pure FO logic.)

Propositional logical steps are easily dealt with, relying on invertibility
and cuts, with possible structural steps. Importantly, due to the statement of
the lemma, such steps apply to only ${\Sigma}_{n}$ formulae (recall the
discussion at the end of Sect. 2). For instance, if $\pi$ extends a proof
$\pi^{\prime}$ by a $\wedge$-left step,

$\Gamma,\chi_{0},\chi_{1},\forall\vec{x}.\vec{\varphi}\Rightarrow\Delta,\forall\vec{y}.\vec{\psi}$
$\scriptstyle\wedge\text{-}l\;$
$\Gamma,\chi_{0}\wedge\chi_{1},\forall\vec{x}.\vec{\varphi}\Rightarrow\Delta,\forall\vec{y}.\vec{\psi}$

then we define $\lceil\pi\rceil$ as,

$\left\\{{{}{}\vbox{\hbox{\kern
12.49995pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\hbox{\hbox{\kern
0.0pt\hbox{\vbox{\offinterlineskip\hbox{\kern
31.16933pt\hbox{\hbox{\hbox{$$}}}\kern 31.16933pt}\kern
1.43518pt\kern-0.7pt\hbox{\hbox
to0.0pt{\hss\hbox{$\smash{\lower-0.7pt\hbox{$$}}$}}\vbox{\vbox
to1.8pt{\vfill\hbox to62.33865pt{\hrulefill}\kern 1.0pt\hbox
to62.33865pt{\hrulefill}\vfill}}\hbox
to0.0pt{\hbox{$\smash{\lower-0.7pt\hbox{$$}}$}\hss}}\kern
1.43518pt\kern-0.7pt\hbox{\hbox{\hbox{$\kern
0.0pt\hbox{$\chi_{0},\chi_{1}\Rightarrow\chi_{0}\wedge\chi_{1}$}\kern
0.0pt$}}}}}\kern 0.0pt}\kern
10.00002pt}\hbox{\hbox{$\Gamma,\chi_{0}\wedge\chi_{1}\Rightarrow\Delta,\varphi_{i}$}}}}}\kern
1.43518pt\hbox{\kern 0.0pt\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\mathit{cut}\;$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to142.95111pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}\kern 0.0pt}\kern 1.43518pt\hbox{\kern
38.39156pt\hbox{\hbox{$\Gamma,\chi_{0},\chi_{1}\Rightarrow\Delta,\varphi_{i}$}}\kern
38.39156pt}}}\kern 0.0pt}}}\right\\}_{i\leq l}$
$\textstyle{\scriptstyle\lceil\pi^{\prime}\rceil}$
$\Gamma,\chi_{0},\chi_{1}\Rightarrow\Delta,\vec{\psi}$
$\scriptstyle\wedge\text{-}l\;$
$\Gamma,\chi_{0}\wedge\chi_{1}\Rightarrow\Delta,\vec{\psi}$

and if $\pi$ extends proofs $\pi_{0}$ and $\pi_{1}$ by a $\wedge$-right step,

$\Gamma,\forall\vec{x}.\vec{\varphi}\Rightarrow\Delta,\chi_{0},\forall\vec{y}.\vec{\psi}$$\Gamma,\forall\vec{x}.\vec{\varphi}\Rightarrow\Delta,\chi_{1},\forall\vec{y}.\vec{\psi}$
$\scriptstyle\wedge\text{-}r\;$
$\Gamma,\forall\vec{x}.\vec{\varphi}\Rightarrow\Delta,\chi_{0}\wedge\chi_{1},\forall\vec{y}.\vec{\psi}$

then we define $\lceil\pi\rceil$ as:

$\left\\{{{}{}\vbox{\hbox{\kern
12.49995pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\hbox{\hbox{\hbox{$\Gamma\Rightarrow\Delta,\chi_{0}\wedge\chi_{1},\varphi_{i}$}}\kern
10.00002pt}\hbox{\kern 0.0pt\hbox{\vbox{\offinterlineskip\hbox{\kern
24.332pt\hbox{\hbox{\hbox{$$}}}\kern 24.332pt}\kern
1.43518pt\kern-0.7pt\hbox{\hbox
to0.0pt{\hss\hbox{$\smash{\lower-0.7pt\hbox{$$}}$}}\vbox{\vbox
to1.8pt{\vfill\hbox to48.664pt{\hrulefill}\kern 1.0pt\hbox
to48.664pt{\hrulefill}\vfill}}\hbox
to0.0pt{\hbox{$\smash{\lower-0.7pt\hbox{$$}}$}\hss}}\kern
1.43518pt\kern-0.7pt\hbox{\hbox{\hbox{$\kern
0.0pt\hbox{$\chi_{0}\wedge\chi_{1}\Rightarrow\chi_{j}$}\kern 0.0pt$}}}}}\kern
0.0pt}}}}\kern 1.43518pt\hbox{\kern 0.0pt\hbox
to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\mathit{cut}\;$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to133.16528pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}\kern 0.0pt}\kern 1.43518pt\hbox{\kern
38.39156pt\hbox{\hbox{$\Gamma\Rightarrow\Delta,\chi_{j},\varphi_{i}$}}\kern
38.39156pt}}}\kern 0.0pt}}}\right\\}_{i\leq l}$
$\textstyle{\scriptstyle\lceil\pi_{j}\rceil}$
$\Gamma\Rightarrow\Delta,\chi_{j},\vec{\psi}$ $\scriptstyle\wedge\text{-}r\;$
$\;\forall j<2$ $\Gamma\Rightarrow\Delta,\chi_{0}\wedge\chi_{1},\vec{\psi}$

If $\pi$ extends a proof $\pi^{\prime}$ by a thinning step,

$\Gamma,\forall\vec{x}.\vec{\varphi}\Rightarrow\Delta,\forall\vec{y}.\vec{\psi}$
$\scriptstyle\mathit{wk}\;$
$\Gamma^{\prime},\Pi,\Gamma,\forall\vec{x}.\vec{\varphi}\Rightarrow\Delta,\forall\vec{y}.\vec{\psi},\Delta^{\prime},\forall\vec{z}.\vec{\chi}$

where $\Gamma^{\prime},\Delta^{\prime},\vec{\chi}$ are ${\Sigma}_{n}$ and
$\Pi$ is ${\Pi}_{n+1}$, then we define $\lceil\pi\rceil$ as:

$\left\\{\Gamma^{\prime},\Gamma\Rightarrow\Delta,\varphi_{i},\Delta^{\prime}\right\\}_{i\leq
l}$
$\textstyle{\scriptstyle\Gamma^{\prime},\lceil\pi^{\prime}\rceil,\Delta^{\prime}}$
$\Gamma^{\prime},\Gamma\Rightarrow\Delta,\vec{\psi},\Delta^{\prime}$
$\scriptstyle\mathit{wk}\;$
$\Gamma^{\prime},\Gamma\Rightarrow\Delta,\vec{\psi},\Delta^{\prime},\vec{\chi}$

where $\Gamma^{\prime},\lceil\pi^{\prime}\rceil,\Delta^{\prime}$ is obtained
from $\lceil\pi^{\prime}\rceil$ by prepending $\Gamma^{\prime}$ and appending
$\Delta^{\prime}$ to each sequent. For this we might need to rename some free
variables in $\pi^{\prime}$ so that eigenvariable conditions are preserved
after the transformation; this does not affect the cedents $\Gamma,\Delta$ by
the assumption from the inductive hypothesis. Notice that we are simply
ignoring the extra premisses due to $\Pi$.

If $\pi$ extends proofs $\pi_{0}$ and $\pi_{1}$ by a $\mathit{cut}$ step on a
${\Pi}_{n+1}$ formula,

$\Gamma,\forall\vec{x}.\vec{\varphi}\Rightarrow\Delta,\forall\vec{y}.\vec{\psi},\forall
z.\chi$$\Gamma,\forall\vec{x}.\vec{\varphi},\forall
z.\chi\Rightarrow\Delta,\forall\vec{y}.\vec{\psi}$
$\scriptstyle\mathit{cut}\;$
$\Gamma,\forall\vec{x}.\vec{\varphi}\Rightarrow\Delta,\forall\vec{y}.\vec{\psi}$

then we define $\lceil\pi\rceil$ as:

$\left\\{\Gamma\Rightarrow\Delta,\varphi_{i}\right\\}_{i\leq l}$
$\textstyle{\scriptstyle\lceil\pi_{0}\rceil}$
$\Gamma\Rightarrow\Delta,\vec{\psi},\chi$ $\left\\{{\vbox{\hbox{\kern
11.52773pt\hbox{\vbox{\offinterlineskip\hbox{\kern
4.65799pt\hbox{\hbox{\hbox{$\Gamma\Rightarrow\Delta,\varphi_{i}$}}}\kern
4.65799pt}\kern 1.43518pt\hbox{\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\mathit{wk}\;$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to52.37015pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}}\kern 1.43518pt\hbox{\hbox{\hbox{$\kern
0.0pt\hbox{$\Gamma\Rightarrow\Delta,\vec{\psi},\varphi_{i}$}\kern
0.0pt$}}}}}\kern 0.0pt}}}\right\\}_{i\leq l}$
$\textstyle{\scriptstyle\lceil\pi_{1}\rceil,\vec{\psi}}$
$\Gamma\Rightarrow\Delta,\vec{\psi},\vec{\psi}$ .
$\Gamma\Rightarrow\Delta,\vec{\psi}$

The final dotted ‘contraction’ step is implicit, since we treat cedents as
sets. Again, we might need to rename some variables in $\pi_{1}$. If instead
the cut formula were ${\Sigma}_{n}$, say $\chi$, we would define
$\lceil\pi\rceil$ as:

$\\{\Gamma\Rightarrow\Delta,\varphi_{i}\\}_{i\leq l}$
$\textstyle{\scriptstyle\lceil\pi_{0}\rceil}$
$\Gamma\Rightarrow\Delta,\chi,\vec{\psi}$ $\left\\{{\vbox{\hbox{\kern
11.52773pt\hbox{\vbox{\offinterlineskip\hbox{\kern
4.7951pt\hbox{\hbox{\hbox{$\Gamma\Rightarrow\Delta,\varphi_{i}$}}}\kern
4.7951pt}\kern 1.43518pt\hbox{\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\mathit{wk}\;$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to52.64438pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}}\kern 1.43518pt\hbox{\hbox{\hbox{$\kern
0.0pt\hbox{$\Gamma,\chi\Rightarrow\Delta,\varphi_{i}$}\kern 0.0pt$}}}}}\kern
0.0pt}}}\right\\}_{i\leq l}$ $\textstyle{\scriptstyle\lceil\pi_{1}\rceil}$
$\Gamma,\chi\Rightarrow\Delta,\vec{\psi}$ $\scriptstyle\mathit{cut}\;$
$\Gamma\Rightarrow\Delta,\vec{\psi}$

If $\pi$ extends a proof $\pi^{\prime}$ by a $\forall$-left step,

$\Gamma,\chi(t),\forall\vec{x}.\vec{\varphi}\Rightarrow\Delta,\forall\vec{y}.\vec{\psi}$
$\scriptstyle\forall\text{-}l\;$ $\Gamma,\forall
z.\chi(z),\forall\vec{x}.\vec{\varphi}\Rightarrow\Delta,\forall\vec{y}.\vec{\psi}$

where $\forall z.\chi(z)$ is ${\Pi}_{n+1}$, we define $\lceil\pi\rceil$ as
follows:

$\Gamma\Rightarrow\Delta,\chi(z)$ $\scriptstyle\mathit{sub}\;$
$\Gamma\Rightarrow\Delta,\chi(t)$ $\left\\{{\vbox{\hbox{\kern
11.52773pt\hbox{\vbox{\offinterlineskip\hbox{\kern
10.48956pt\hbox{\hbox{\hbox{$\Gamma\Rightarrow\Delta,\varphi_{i}$}}}\kern
10.48956pt}\kern 1.43518pt\hbox{\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\mathit{wk}\;$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to64.0333pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}}\kern 1.43518pt\hbox{\hbox{\hbox{$\kern
0.0pt\hbox{$\Gamma,\chi(t)\Rightarrow\Delta,\varphi_{i}$}\kern
0.0pt$}}}}}\kern 0.0pt}}}\right\\}_{i\leq l}$
$\textstyle{\scriptstyle\lceil\pi^{\prime}\rceil}$
$\Gamma,\chi(t)\Rightarrow\Delta,\vec{\psi}$ $\scriptstyle\mathit{cut}\;$
$\Gamma\Rightarrow\Delta,\vec{\psi}$

(Notice that, although $z$ occurs as an eigenvariable for a $\mathit{sub}$
step here, it is already bound in the conclusion of $\pi$, so we preserve the
inductive hypothesis.) If $\pi$ extends a proof $\pi^{\prime}$ by a
$\forall$-right step,

$\Gamma,\forall\vec{x}.\vec{\varphi}\Rightarrow\Delta,\forall\vec{y}.\vec{\psi},\chi$
$\scriptstyle\forall\text{-}r\;$
$\Gamma,\forall\vec{x}.\vec{\varphi}\Rightarrow\Delta,\forall\vec{y}.\vec{\psi},\forall
z.\chi$

where $\forall z.\chi$ is ${\Pi}_{n+1}$, then we define $\lceil\pi\rceil$ as:

$\left\\{{\vbox{\hbox{\kern 11.52773pt\hbox{\vbox{\offinterlineskip\hbox{\kern
5.35066pt\hbox{\hbox{\hbox{$\Gamma\Rightarrow\Delta,\varphi_{i}$}}}\kern
5.35066pt}\kern 1.43518pt\hbox{\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\mathit{wk}\;$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to53.7555pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}}\kern 1.43518pt\hbox{\hbox{\hbox{$\kern
0.0pt\hbox{$\Gamma\Rightarrow\Delta,\varphi_{i},\chi$}\kern 0.0pt$}}}}}\kern
0.0pt}}}\right\\}_{i\leq l}$
$\textstyle{\scriptstyle\lceil\pi^{\prime}\rceil,\chi}$
$\Gamma\Rightarrow\Delta,\vec{\psi},\chi$

If $\pi$ extends a proof $\pi^{\prime}$ by a $\exists$-right step,

$\Gamma,\forall\vec{x}.\vec{\varphi}\Rightarrow\Delta,\forall\vec{y}.\vec{\psi},\chi(t)$
$\scriptstyle\exists\text{-}r\;$
$\Gamma,\forall\vec{x}.\vec{\varphi}\Rightarrow\Delta,\forall\vec{y}.\vec{\psi},\exists
z.\chi(z)$

where $\exists z.\chi(z)$ is ${\Sigma}_{n}$, then we define $\lceil\pi\rceil$
as:

$\left\\{{\vbox{\hbox{\kern 11.52773pt\hbox{\vbox{\offinterlineskip\hbox{\kern
11.04512pt\hbox{\hbox{\hbox{$\Gamma\Rightarrow\Delta,\varphi_{i},\exists
z.\chi(z)$}}}\kern 11.04512pt}\kern 1.43518pt\hbox{\hbox
to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\mathit{wk}\;$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to105.47075pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}}\kern 1.43518pt\hbox{\hbox{\hbox{$\kern
0.0pt\hbox{$\Gamma\Rightarrow\Delta,\varphi_{i},\chi(t),\exists
z.\chi(z)$}\kern 0.0pt$}}}}}\kern 0.0pt}}}\right\\}_{i\leq l}$
$\textstyle{\scriptstyle\lceil\pi^{\prime}\rceil,\exists z.\chi(z)}$
$\Gamma\Rightarrow\Delta,\vec{\psi},\chi(t),\exists z.\chi(z)$
$\scriptstyle\exists\text{-}r\;$ $\Gamma\Rightarrow\Delta,\vec{\psi},\exists
z.\chi(z)$

Again, some eigenvariables of $\pi^{\prime}$ might have to be renamed. Any
other quantifier steps are dealt with routinely.

Finally, if $\pi$ extends proofs $\pi_{0}$ and $\pi^{\prime}$ by an induction
step,

$\Gamma,\forall\vec{x}.\vec{\varphi}\Rightarrow\Delta,\forall\vec{y}.\vec{\psi},\forall
z.\chi(0)$$\Gamma,\forall\vec{x}.\vec{\varphi},\forall
z.\chi(c)\Rightarrow\Delta,\forall\vec{y}.\vec{\psi},\forall
z.\chi(\mathsf{s}c)$ $\scriptstyle\mathit{ind}\;$
$\Gamma,\forall\vec{x}.\vec{\varphi}\Rightarrow\Delta,\forall\vec{y}.\vec{\psi},\forall
z.\chi(t)$

we define $\lceil\pi\rceil$ to be the following cyclic proof,

$\left\\{\Gamma\Rightarrow\Delta,\varphi_{i}\right\\}_{i\leq l}$
$\textstyle{\scriptstyle\lceil\pi_{0}\rceil}$
$\Gamma\Rightarrow\Delta,\vec{\psi},\chi(0)$
$d=0,\Gamma\Rightarrow\Delta,\vec{\psi},\chi(d)$ $\vdots$ $\;\bullet$
$\Gamma\Rightarrow\Delta,\vec{\psi},\chi(d)$ $\scriptstyle\mathit{sub}\;$
$\Gamma\Rightarrow\Delta,\vec{\psi},\chi(c)$ $\left\\{{\vbox{\hbox{\kern
11.52773pt\hbox{\vbox{\offinterlineskip\hbox{\kern
4.65799pt\hbox{\hbox{\hbox{$\Gamma\Rightarrow\Delta,\varphi_{i}$}}}\kern
4.65799pt}\kern 1.43518pt\hbox{\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\mathit{wk}\;$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to52.37015pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}}\kern 1.43518pt\hbox{\hbox{\hbox{$\kern
0.0pt\hbox{$\Gamma\Rightarrow\Delta,\vec{\psi},\varphi_{i}$}\kern
0.0pt$}}}}}\kern 0.0pt}}}\right\\}_{i\leq l}$
$\textstyle{\scriptstyle\lceil\pi^{\prime}\rceil,\vec{\psi}}$
$\Gamma\Rightarrow\Delta,\vec{\psi},\chi(\mathsf{s}c)$
$\underline{c<d},d=\mathsf{s}c,\Gamma\Rightarrow\Delta,\vec{\psi},\chi(d)$
$\;\bullet$ $\Gamma\Rightarrow\Delta,\vec{\psi},\chi(d)$
$\scriptstyle\mathit{sub}\;$ $\Gamma\Rightarrow\Delta,\vec{\psi},\chi(t)$

where we have written $\bullet$ to mark roots of identical subtrees. Notice
that any branch hitting $\bullet$ infinitely often will have an infinitely
progressing trace alternating between $c$ and $d$, by the underlined progress
point $c<d$: thanks to the assumption from the inductive hypothesis, $c$ will
not occur in $\lceil\pi^{\prime}\rceil$ as an eigenvariable for
$\exists\text{-}l$, $\forall\text{-}r$ or $\mathit{sub}$ steps so the trace
along $c$ in $\lceil\pi^{\prime}\rceil$ remains intact, cf. Rmk. 4. Any other
infinite branch has a tail that is already in $\lceil\pi^{\prime}\rceil$ or
$\lceil\pi_{0}\rceil$ and so has an infinitely progressing trace by the
inductive hypothesis.

The lemma above gives us a simple proof of the main result of this section:

######  Proof 4.2 (Proof of Thm. 8).

Let $\pi$ be a $\mathrm{I}{\Pi}_{n+1}$ proof of a sequent $\Rightarrow\forall
x.\varphi$, where $\varphi\in{\Sigma}_{n}$, under Prop. 2. By Thm. 3 we may
assume that $\pi$ contains only ${\Pi}_{n+1}$ cuts, whence we may simply apply
Lemma 9 to obtain a $\mathrm{C}{\Sigma}_{n}$ proof of $\Rightarrow\varphi$.
(Notice that there are no assumption sequents after applying the lemma since
the antecedent is empty.) Now the result follows simply by an application of
$\forall\text{-}r$.

For the interested reader, we have given an example of this translation in
action in App. A, for a ‘relativised’ version of arithmetic with an
uninterpreted function symbol.

##  5\. Second-order theories for reasoning about automata

We now consider a two-sorted, or ‘second-order’ (SO), version of FO logic,
with variables $X,Y,Z,$ etc. ranging over sets of individuals, and new atomic
formulae $t\in X$, sometimes written $X(t)$. We also have SO quantifiers
binding the SO variables with the natural interpretation. Again, we give only
brief preliminaries, but the reader is encouraged to consult the standard
texts [Sim09] and [Hir14].

We write $\mathsf{Q}_{2}$ for an appropriate extension of $\mathsf{Q}$ by
basic axioms governing sets (see, e.g., [Sim09] or [Hir14]), and write
${\Sigma}^{0}_{n}$ and ${\Pi}^{0}_{n}$ for the classes ${\Sigma}_{n}$ and
${\Pi}_{n}$ respectively, but now allowing free set variables to occur.

The recursive comprehension axiom schema is the following:555Notice that there
is an unfortunate coincidence of the notation $\mathsf{CA}$ for ‘comprehension
axiom’ and ‘cyclic arithmetic’, but the context of use should always avoid any
ambiguity.

${\Delta}^{0}_{1}\text{-}\mathsf{CA}\ :\ \forall\vec{y},\vec{Y}.(\forall
x.(\varphi(x,\vec{y},\vec{Y})\equiv\neg\psi(x,\vec{y},\vec{Y}))\supset\exists
X.\forall x.(X(x)\equiv\varphi(x)))$

where $\varphi,\psi$ are in ${\Sigma}^{0}_{1}$ and $X$ does not occur free in
$\varphi$ or $\psi$. From here, the theory $\mathsf{RCA}_{0}$ is defined as
$\mathsf{Q}_{2}+{\Delta}^{0}_{1}\text{-}\mathsf{CA}+{\Sigma}^{0}_{1}\text{-}\mathsf{IND}$.

Since we will always work in extensions of $\mathsf{RCA}_{0}$, which proves
the totality of primitive recursive functions, we will conservatively add
function symbols for primitive recursive functions on individuals whenever we
need them. We will also henceforth consider FO theories extended by ‘oracles’,
i.e. uninterpreted set/predicate variables, in order to access ‘uniform’
classes of FO proofs. We write $\mathrm{I}{\Sigma}_{n}(X)$ for the same class
of proofs as $\mathrm{I}{\Sigma}_{n}$ but where $X$ is allowed to occur as a
predicate symbol. The usefulness of a $\mathrm{I}{\Sigma}_{n}(X)$ proof is
that we may later substitute $X$ for a FO formula, say
$\varphi(-)\in{\Delta}_{m+1}$, to arrive at a $\mathrm{I}{\Sigma}_{m+n}$ proof
of size $O(|\varphi|)$. This ‘parametrisation’ of a FO proof allows us to
avoid unnecessary blowups in proof size induced by ‘non-uniform’ translations
from second-order theories; we implicitly use this observation for proof
complexity bounds later, particularly in Sect. 6.

The following result is an adaptation of well known conservativity results,
e.g. as found in [Sim09, Hir14], but we include a proof anyway for
completeness.

######  Proposition 10.

$\mathsf{RCA}_{0}+{\Sigma}^{0}_{n}\text{-}\mathsf{IND}$ is conservative over
$\mathrm{I}{\Sigma}_{n}(X)$.

######  Proof 5.1 (Proof sketch).

First we introduce countably many fresh set symbols
$X^{\vec{t},\vec{Y}}_{\varphi,\psi}$, indexed by ${\Sigma}^{0}_{1}$ formulae
$\varphi(x,\vec{x},\vec{X}),\psi(x,\vec{x},\vec{X})$ with all free variables
indicated, FO terms $\vec{t}$ with $|\vec{t}|=|\vec{x}|$ and SO variables
$\vec{Y}$ with $|\vec{Y}|=|\vec{X}|$. These will serve as witnesses to the
sets defined by comprehension. We replace the comprehension axioms by initial
sequents of the form:

$\Gamma,\forall
x.(\varphi(x,\vec{t},\vec{Y})\equiv\neg\psi(x,\vec{t},\vec{Y})),\varphi(t,\vec{t},\vec{Y})\Rightarrow
t\in X^{\vec{t},\vec{Y}}_{\varphi,\psi},\Delta$ (3) $\Gamma,\forall
x.(\varphi(x,\vec{t},\vec{Y})\equiv\neg\psi(x,\vec{t},\vec{Y})),t\in
X^{\vec{t},\vec{Y}}_{\varphi,\psi}\Rightarrow\varphi(t,\vec{t},\vec{Y}),\Delta$
(4)

It is routine to show that these new initial sequents are equivalent to the
comprehension axioms for $\varphi,\psi$.

Now we apply free-cut elimination, Thm. 3, to a proof in such a system and
replace every occurrence of $t\in X^{\vec{t},\vec{Y}}_{\varphi,\psi}$ with
$\varphi(t,\vec{t},\vec{Y})$, and every occurrence of $t\notin
X^{\vec{t},\vec{Y}}_{\varphi,\psi}$ with $\psi(t,\vec{t},\vec{Y})$. (Recall
here that we assume formulae are in De Morgan normal form.) Any comprehension
initial sequents affected by this replacement become purely logical theorems.
Furthermore, any induction formulae remain ${\Sigma}^{0}_{n}$, provably in
pure logic, thanks to our consideration of whether
$X^{\vec{t},\vec{Y}}_{\varphi,\psi}$ occurs positively or negatively. Any
extraneous free set variables in induction steps (except $X$), e.g. $Y$, may
be safely dealt with by replacing any atomic formula $Y(s)$ with $\top$. The
resulting proof is in $\mathrm{I}{\Sigma}_{n}(X)$.

It is worth pointing out that, in general, the transformation from a SO proof
to a FO proof can yield a possibly non-elementary blowup in the size of
proofs, due to, e.g., the application of (free-)cut elimination.

###  5.1. Formalisation of Büchi acceptance

From now on we will be rather informal when talking about finite objects, e.g.
automata, finite sequences, or even formulae. In particular we may freely use
such meta-level objects within object-level formulae when, in fact, we are
formally referring to their ‘Gödel numbers’. Also, statements inside
quotations, “-”, will usually be (provably) recursive in any free variables
occurring, i.e. ${\Delta}^{0}_{1}$. This way quantifier complexity is
(usually) safely measured by just the quantifiers outside quotations.

We often treat a set symbol $X$ as a binary predicate by interpreting its
argument as a pair and using Gödel’s ‘$\beta$ functions’ to primitive-
recursively extract its components. We use such predicates to encode sequences
by interpreting $X(x,y)$ as “the $x$th symbol of $X$ is $y$”; this
interpretation presumes we already have the totality and determinism of $X$ as
a binary relation. Formally, for a set $S$ and a set symbol $X$ treated as a
binary predicate, we will write $X\in S^{\omega}$ for the conjunction of the
following two formulae,

$\forall x.\exists y\in S.X(x,y)$ (5) $\forall x,y,z.((X(x,y)\wedge
X(x,z))\supset y=z)$ (6)

i.e. $X$ is, in fact, the graph of a function $\mathbb{N}\to S$. When we know
that these formulae hold true for $X$, we may construe the expression $X(x)$
as a term in formulae, for instance writing $\varphi(X(x))$ as shorthand for
$\exists y.(X(x,y)\wedge\varphi(y))$ or, equivalently, $\forall
y.(X(x,y)\supset\varphi(y))$.

[Language membership] Let $\mathcal{A}=(A,Q,\delta,q_{0},F)$ be a NBA and
treat $X$ as a binary predicate symbol. We define the formula
$X\in\mathcal{L}(\mathcal{A})$ as:

$X\in A^{\omega}\ \wedge\ \exists Y\in
Q^{\omega}.\left(\begin{array}[]{rl}&Y(0,q_{0})\\\ \wedge&\forall x.\
(Y(x),X(x),Y(\mathsf{s}x))\in\delta\\\ \wedge&\forall x.\exists x^{\prime}>x.\
Y(x^{\prime})\in F\end{array}\right)$ (7)

If $\mathcal{A}$ is deterministic and $X\in A^{\omega}$, we write $q_{X}(x,y)$
for “$y$ is the $x$th state of the run of $X$ on $\mathcal{A}$”, which is
provably recursive in $\mathsf{RCA}_{0}$. Similarly to before, we may write
$\varphi(q_{X}(x))$ as shorthand for $\exists y.(q_{X}(x,y)\wedge\varphi(y))$
or, equivalently in $\mathsf{RCA}_{0}$, for $\forall
y.(q_{X}(x,y)\supset\varphi(y))$. For DBA, we alternatively define
$X\in\mathcal{L}(\mathcal{A})$ as:

$X\in A^{\omega}\ \wedge\ \forall x.\exists x^{\prime}>x.\
q_{X}(x^{\prime})\in F$ (8)

This ‘double definition’ will not be problematic for us, since
$\mathsf{RCA}_{0}$ can check if an automaton is deterministic or not and, if
so, even prove the equivalence between the two definitions:

######  Proposition 11.

$\mathsf{RCA}_{0}\vdash\forall\text{ DBA }\mathcal{A}.(\eqref{eqn:nd-
memb}\equiv\eqref{eqn:det-acc})$.

######  Proof 5.2 (Proof sketch).

Let $\mathcal{A}=(A,Q,\delta,q_{0},F)$ be a deterministic automaton. For the
left-right implication let $Y\in Q^{\omega}$ be an ‘accepting run’ of $X$ on
$\mathcal{A}$ and use induction to show that $Y(x,q_{X}(x))$. For the right-
left implication, we use comprehension to define an ‘accepting run’ $Y\in
Q^{\omega}$ by: $Y(x,q)\ \equiv\ q_{X}(x,q)$. Clearly the definition of $Y$ is
${\Delta}^{0}_{1}$, and we can show that such $Y$ is a ‘correct run’ by
induction on $x$.

Notice that, for a deterministic automaton, the formula for acceptance is
_arithmetical_ in $X$, i.e. there are no SO quantifiers. This will be rather
important for uniformity in the simulation of cyclic proofs in the next
section.

###  5.2. Formalisations of some automaton constructions

Recall that we may freely add symbols for primitive recursive functions to our
language. Since we rely on various results from [KMPS19] as the ‘engine’
behind some of our proofs, we will use their notions for manipulating
automata.

For NBA $\mathcal{A},\mathcal{A}^{\prime}$, we write $\mathcal{A}^{c}$ and
$\mathcal{A}\sqcup\mathcal{A}^{\prime}$ to denote the complement and union
constructions of automata from [KMPS19] (Sects. 5 and 6 resp.). We also write
$\mathrm{Empty}(\mathcal{A})$ for the recursive algorithm from [KMPS19] (Sect.
6), expressed as a ${\Sigma}_{1}$ formula in $\mathcal{A}$, determining
whether $\mathcal{A}$ computes the empty language. It will also be useful for
us later, in order to bound logical and proof complexity, to notice that DBA
can already be complemented in $\mathsf{RCA}_{0}$. This is a rather
unsurprising result but does not appear in [KMPS19], so we give it here.

For a DBA $\mathcal{A}=(A,Q,\delta,q_{0},F)$, we define a complementary NBA
$\mathcal{A}^{c}$ as follows,

$\mathcal{A}^{c}\ :=\ (A,(Q\times\\{0\\})\cup((Q\setminus
F)\times\\{1\\}),\delta^{c},(q_{0},0),(Q\setminus F)\times\\{1\\})$

where $\delta^{c}\subseteq(Q^{c}\times A)\times Q^{c}$ (writing $Q^{c}$ for
$Q\times\\{0\\}\cup(Q\setminus F)\times\\{1\\}$) is defined as:

$\begin{array}[]{rl}&\\{((q,0),a,(q^{\prime},0))\ :\
(q,a,q^{\prime})\in\delta\\}\\\ \cup&\\{((q,i),a,(q^{\prime},1))\ :\
(q,a,q^{\prime})\in\delta,i=0,1,q^{\prime}\in Q\setminus F\\}\end{array}$

The idea behind this construction is that a run of $\mathcal{A}^{c}$ follows
$\mathcal{A}$ freely for some finite time (in the ‘$0$’ component), after
which it may no longer visit final states of $\mathcal{A}$ (once in the ‘$1$’
component). The determinism of $\mathcal{A}$ guarantees that such a word is
not accepted by it.

By directly inspecting the definitions from [KMPS19], and DBA complementation
above, we have the following properties:

For NBA $\mathcal{A},\mathcal{A}^{\prime}$ we have that:

  1. (1)

$\mathrm{Empty}(\mathcal{A})$ is a polynomial-time predicate in $\mathcal{A}$.

  2. (2)

$\mathcal{A}\sqcup\mathcal{A}^{\prime}$ is constructible in polynomial-time
from $\mathcal{A}$ and $\mathcal{A}^{\prime}$.

  3. (3)

$\mathcal{A}^{c}$ is constructible in exponential-time from $\mathcal{A}$.

For a DBA $\mathcal{A}$, we have that:

  1. (4)

$\mathcal{A}^{c}$ is constructible in polynomial-time from $\mathcal{A}$.

None of these bounds are surprising, due to known bounds on the complexity of
union, complementation and emptiness checking for (non)deterministic Büchi
automata. Nonetheless it is important to state them for the particular
constructions used in this work for bounds on proof complexity later.

######  Lemma 12.

From [KMPS19] we have the following:

  1. (1)

$\mathsf{RCA}_{0}\vdash\forall\text{ NBA
}\mathcal{A}.(\mathrm{Empty}(\mathcal{A})\equiv\forall X\in
A^{\omega}.X\notin\mathcal{L}(\mathcal{A}))$.

  2. (2)

$\mathsf{RCA}_{0}\vdash\forall\text{ NBA
}\mathcal{A}_{1},\mathcal{A}_{2}.(X\in\mathcal{L}(\mathcal{A}_{1}\sqcup\mathcal{A}_{2})\equiv(X\in\mathcal{L}(\mathcal{A}_{1})\vee
X\in\mathcal{L}(\mathcal{A}_{2})))$.

  3. (3)

$\mathsf{RCA}_{0}+{\Sigma}^{0}_{2}\text{-}\mathsf{IND}\vdash\forall\text{ NBA
}\mathcal{A}.(X\in A^{\omega}\supset(X\in\mathcal{L}(\mathcal{A}^{c})\equiv
X\notin\mathcal{L}(\mathcal{A})))$.

We also have that:

  1. (4)

$\mathsf{RCA}_{0}\vdash\forall\text{ DBA }\mathcal{A}.\ (X\in
A^{\omega}\supset(X\in\mathcal{L}(\mathcal{A}^{c})\equiv
X\notin\mathcal{L}(\mathcal{A})))$.

######  Proof 5.3.

1, 2 and 3 follow from [KMPS19], namely from Prop. 6.1 and Lemma 5.2, so we
give a proof of 4.

Working in $\mathsf{RCA}_{0}$, let $\mathcal{A}=(A,Q,\delta,q_{0},F)$ be a
DBA. For the right-left implication, if $X\notin\mathcal{L}(\mathcal{A})$ then
$\exists x.\forall x^{\prime}>x.\ q_{X}(x)\notin F$, so let $x_{0}$ witness
this existential. Now, define by comprehension the run $Y\in(Q^{c})^{\omega}$
as follows:

$Y(x,y)\ \equiv\ ((x\leq x_{0}\wedge y=(q_{X}(x),0))\vee(x>x_{0}\wedge
y=(q_{X}(x),1)))$

Now, indeed $Y(0,(q_{0},0))$, since $q_{X}(0)=q_{0}$, and $Y$ is a correct run
of $X$ on $\mathcal{A}^{c}$ by considering separately the cases $x<x_{0}$,
$x=x_{0}$ and $x>x_{0}$. Finally, for any $x$, $Y$ hits a final state at
$\max(x,x_{0})+1>x$.

For the left-right implication, suppose $X\in\mathcal{L}(\mathcal{A}^{c})$ and
let $Y\in(Q^{c})^{\omega}$ be an accepting run. By induction we have $\forall
x.(Y(x)=(q_{X}(x),0)\vee Y(x)=(q_{X}(x),1))$. Now, $Y$ must eventually hit an
accepting state of $\mathcal{A}^{c}$, i.e. in the $1$-component, say at
position $x_{0}$. Again by induction, we may show that $Y$ remains in the
$1$-component of $\mathcal{A}^{c}$ after $x_{0}$, and hence $q_{X}(x)\notin F$
for $x\geq x_{0}$, as required.

##  6\. An exponential simulation of $\mathsf{CA}$ in $\mathsf{PA}$

In this section we will adapt Simpson’s approach in [Sim17] for showing that
$\mathsf{CA}\subseteq\mathsf{PA}$ into a _uniform_ result in $\mathsf{PA}$.
This essentially constitutes a formalisation of the soundness argument, Prop.
5, in a SO theory conservative over the target fragment of $\mathsf{PA}$. The
‘uniformity’ we aim for ensures that the possibly non-elementary blowup
translating from SO proofs to FO proofs occurs once and for all for a single
arithmetical theorem. Only then do we instantiate the theorem (inside
$\mathsf{PA}$) by the cyclic proof in question, leading to an only elementary
blowup.

To give an idea of how the result is obtained, and how our exposition refines
that of [Sim17], we take advantage of the following aspects of the soundness
argument for cyclic proofs:

  1. (a)

The Büchi automaton accepting all infinite branches of a cyclic proof is, in
fact, deterministic, and so we can express acceptance of an $\omega$-word in
this automaton arithmetically.

  2. (b)

A branch of invalid sequents and corresponding assignments, as in the proof of
Prop. 5, can be uniformly generated from an initial unsatisfying assignment by
an arithmetical formula.

  3. (c)

Since all inductions are only up to $\omega$, we need only _arbitrarily often_
progressing traces, rather than explicit infinitely progressing traces.

Together, these properties give us just enough ‘wiggle room’ to carry out the
soundness argument in a sufficiently uniform way.

Throughout this section we will also carefully track how much quantifier
complexity is used in theorem statements, since we will later modify this
argument to obtain a converse result to Thm. 8.

###  6.1. An arithmetically uniform treatment of automata

Referring to (c) above, we define an arithmetical corollary of NBA acceptance
that is nonetheless sufficiently strong to formalise the soundness argument
for cyclic proofs: [Arithmetic acceptance] Let
$\mathcal{A}=(A,Q,\delta,q_{0},F)$ be a NBA and $X\in A^{\omega}$, and
temporarily write:

  * •

$F(x):=$ “$x$ is a finite run of $X$ on $\mathcal{A}$ ending at a final
state”.

  * •

$E(z,x,y):=$ “$z$ extends $x$ to a finite run of $X$ on $\mathcal{A}$ hitting
$\geq y$ final states”

We define:

$\mathrm{ArAcc}(X,\mathcal{A})\ :=\ X\in A^{\omega}\wedge\exists
x.\left(F(x)\wedge\forall y.\exists z.E(z,x,y)\right)$ (9)

For intuition, we may consider $\omega$-regular expressions rather than
automata, which are of the form $\sum\limits_{i<n}e_{i}\cdot f_{i}^{\omega}$,
for some $n\in\mathbb{N}$, without loss of generality. The formula
$\mathrm{ArAcc}$ for this expression essentially recognises infinite words
that have prefixes of the form $\sigma\tau_{k}$ for some
$\sigma\in\mathcal{L}(e_{i})$, for some $i<n$, and
$\tau_{k}\in\mathcal{L}(f_{i}^{k})$ for each $k\in\mathbb{N}$. Clearly the
condition $\mathrm{ArAcc}$ is a (provable) consequence of acceptance itself:

######  Proposition 13.

$\mathsf{RCA}_{0}\vdash\forall\mathcal{A}.(X\in\mathcal{L}(\mathcal{A})\supset\mathrm{ArAcc}(X,\mathcal{A}))$.

######  Proof 6.1.

Working in $\mathsf{RCA}_{0}$, fix $\mathcal{A}=(A,Q,\delta,q_{0},F)$ and
suppose $X\in\mathcal{L}(\mathcal{A})$. Let $Y\in Q^{\omega}$ be an ‘accepting
run’ of $X$ on $\mathcal{A}$, cf. (7). We may show that,

$\exists z\in Q^{*}.\text{``$z$ is a finite prefix of $Y$ hitting $\geq y$
final states in $\mathcal{A}$''}$ (10)

by ${{\Sigma}^{0}_{1}}$-induction on $y$, appealing to the unboundedness of
final states in $Y$ for both the base case and the inductive steps. Now, in
the definition of $\mathrm{ArAcc}$ in (9), we set $x$ to be the least such $z$
for which (10)$[1/y]$ holds (again by induction), so that $F(x)$ from (9)
holds. Thus, for any $y\in\mathbb{N}$, we may find an appropriate $z$ making
$E(z,x,y)$ in (9) true by appealing to (10). The fact that $z$ extends $x$
follows from leastness of $x$ and that $Y$ is a sequence, cf. (5) and (6).

Let us write $\mathcal{A}_{1}\sqsubseteq\mathcal{A}_{2}$ for
$\mathrm{Empty}((\mathcal{A}_{1}^{c}\sqcup\mathcal{A}_{2})^{c})$. We may now
present our main ‘uniform’ result needed to carry out our soundness proof in
FO theories.

######  Theorem 14.

$\mathsf{RCA}_{0}+{\Sigma}^{0}_{2}\text{-}\mathsf{IND}$ proves:

$\forall\ \text{DBA}\ \mathcal{A}_{1},\forall\ \text{NBA}\ \mathcal{A}_{2}.\
\left((\mathcal{A}_{1}\sqsubseteq\mathcal{A}_{2}\wedge
X\in\mathcal{L}(\mathcal{A}_{1}))\supset\mathrm{ArAcc}(X,\mathcal{A}_{2})\right)$
(11)

######  Proof 6.2.

Working in $\mathsf{RCA}_{0}+{\Sigma}^{0}_{2}\text{-}\mathsf{IND}$, let
$\mathcal{A}_{1}$ be a DBA and $\mathcal{A}_{2}$ be a NBA such that
$X\in\mathcal{L}(\mathcal{A}_{1})$ and
$\mathcal{A}_{1}\sqsubseteq\mathcal{A}_{2}$. We have:

$\begin{array}[]{rll}&\mathrm{Empty}((\mathcal{A}_{1}^{c}\sqcup\mathcal{A}_{2})^{c})&\text{since
$\mathcal{A}_{1}\sqsubseteq\mathcal{A}_{2}$}\\\ \implies&\forall Y\in
A^{\omega}.\
Y\notin\mathcal{L}((\mathcal{A}_{1}^{c}\sqcup\mathcal{A}_{2})^{c})&\text{by
Lemma~{}\ref{lem:aut-clos-props-in-so-arith}.\ref{item:emptiness-rca}}\\\
\implies&\forall Y\in A^{\omega}.\
Y\in\mathcal{L}(\mathcal{A}_{1}^{c}\sqcup\mathcal{A}_{2})&\text{by
Lemma~{}\ref{lem:aut-clos-props-in-so-arith}.\ref{item:compl-rca-s2ind}}\\\
\implies&\forall Y\in A^{\omega}.(Y\in\mathcal{\mathcal{L}}(A_{1}^{c})\vee
Y\in\mathcal{L}(\mathcal{A}_{2}))&\text{ by Lemma \ref{lem:aut-clos-props-in-
so-arith}.\ref{item:union-rca}}\\\ \implies&\forall Y\in
A^{\omega}.(Y\in\mathcal{L}(\mathcal{A}_{1})\supset
Y\in\mathcal{L}(\mathcal{A}_{2}))&\text{by Lemma \ref{lem:aut-clos-props-in-
so-arith}.\ref{item:compl-dba-rca}}\\\
\implies&X\in\mathcal{L}(\mathcal{A}_{2})&\text{since
$X\in\mathcal{L}(\mathcal{A}_{1})$}\\\
\implies&\mathrm{ArAcc}(X,\mathcal{A}_{2})&\text{by Prop.~{}\ref{prop:arith-
acc}.}\end{array}$

Noticing that DBA acceptance is also purely arithmetical in $X$ (cf. (a)), by
the conservativity result Prop. 10, we have:

######  Corollary 15.

$\mathrm{I}{\Sigma}_{2}(X)$ proves (11).

###  6.2. Formalising the soundness argument for cyclic proofs

At this point we are able to mostly mimic the formalisation of the soundness
argument from [Sim17], although we must further show that a branch of invalid
sequents, cf. the proof of Prop. 5, is uniformly describable (cf. (b)).

For $n\geq 0$, let $\mathbb{N},\rho\vDash_{n}\varphi$ be an appropriate
${\Delta}_{n+1}$ formula (provably in $\mathrm{I}{\Sigma}_{n+1}$) asserting
that a formula $\varphi$ is true in $\mathbb{N}$ under the assignment $\rho$
of its free variables to natural numbers, as long as $\varphi$ is a Boolean
combination of ${\Sigma}_{n}$ (or ${\Pi}_{n}$) formulae.666If $\varphi$ is not
a Boolean combination of ${\Sigma}_{n}$ formulae then
$\mathbb{N},\rho\vDash_{n}\varphi$ crashes and returns $\bot$. Formally, the
formula $\mathbb{N},\rho\vDash_{n}\varphi$ takes as arguments the _codes_ of
$\rho$ and $\varphi$, i.e. their Gödel numbers; the construction of such a
formula for $\vDash_{n}$ is standard (see, e.g., [Bus98, Kay91, HP93]) and it
has size polynomial in $n$. Importantly, there are $\mathrm{I}{\Sigma}_{n+1}$
proofs that $\vDash_{n}$ satisfies ‘Tarski’s truth conditions’. Writing
$\mathrm{Bool}(\Phi)$ for the class of Boolean combinations of
$\Phi$-formulae, we have:

######  Proposition 16 (Properties of $\vDash_{n}$, see e.g. [HP93]).

For $n\geq 0$, the following ${\Pi}_{n+1}$ formulae have
$\mathrm{I}{\Sigma}_{n+1}$ proofs of size polynomial in $n$:

  1. (1)

$\forall\varphi\in\mathrm{Bool}({\Sigma}_{n}).\forall\rho.\
(\mathbb{N},\rho\vDash_{n}\neg\varphi\ \equiv\
\mathbb{N},\rho\nvDash_{n}\varphi)$.

  2. (2)

$\forall\varphi,\psi\in\mathrm{Bool}({\Sigma}_{n}).\forall\rho.\
(\mathbb{N},\rho\vDash_{n}(\varphi\vee\psi)\ \equiv\
(\mathbb{N},\rho\vDash_{n}\varphi\ \vee\ \mathbb{N},\rho\vDash\psi))$.

  3. (3)

$\forall\varphi,\psi\in\mathrm{Bool}({\Sigma}_{n}).\forall\rho.\
(\mathbb{N},\rho\vDash_{n}(\varphi\wedge\psi)\ \equiv\
(\mathbb{N},\rho\vDash_{n}\varphi\ \wedge\ \mathbb{N},\rho\vDash\psi))$.

  4. (4)

$\forall\varphi\in{\Sigma}_{n}.\forall\rho.\ (\mathbb{N},\rho\vDash_{n}\exists
x.\varphi\ \equiv\ \exists y.(\mathbb{N},\rho\cup\\{x\mapsto
y\\}\vDash_{n}\varphi))$.

  5. (5)

$\forall\varphi\in{\Pi}_{n}.\forall\rho.\ (\mathbb{N},\rho\vDash_{n}\forall
x.\varphi\ \equiv\ \forall y.(\mathbb{N},\rho\cup\\{x\mapsto
y\\}\vDash_{n}\varphi))$.

We also have $\mathrm{I}{\Sigma}_{n+1}$ proofs of size polynomial in $n$ of
the _substitution property_ :

  1. (6)

$\forall\varphi\in\mathrm{Bool}({\Sigma}_{n}).\forall\rho.\forall\text{ terms
}t.\ (\mathbb{N},\rho\cup\\{a\mapsto\rho(t)\\}\vDash_{n}\varphi\ \equiv\
\mathbb{N},\rho\vDash_{n}\varphi[t/a])$.

In particular we have the _reflection property_ :

######  Proposition 17 (Reflection).

For $n\geq 0$ we have
$\mathrm{I}{\Sigma}_{1}\vdash\varphi\equiv(\mathbb{N},\varnothing\vDash_{n}\varphi)$
with proofs of size polynomial in $n$ and $|\varphi|$, for any closed formula
$\varphi\in{\Sigma}_{n}\cup{\Pi}_{n}$.

Henceforth, all our proof complexity bounds in $n$ follow from the fact that
proofs are parametrised by $\vDash_{n}$ and its basic properties from Prop. 16
above.

[Uniform description of an invalid branch] Let $\pi$ be a $\mathsf{CA}$
preproof of a sequent $\Gamma\Rightarrow\Delta$, and let $n\in\mathbb{N}$ be
such that all formulae occurring in $\pi$ are ${\Sigma}_{n}$. Let $\rho_{0}$
be an assignment such that $\mathbb{N},\rho_{0}\vDash_{n}\bigwedge\Gamma$ but
$\mathbb{N},\rho_{0}\nvDash_{n}\bigvee\Delta$. The branch of $\pi$ generated
by $\rho_{0}$ is the invalid branch as constructed in the proof of Prop. 5,
where at each step that there is a choice of premiss the leftmost one is
chosen, and at each step when there is a choice of assignment of a natural
number to a free variable the least one is chosen. We write
$\mathrm{Branch}_{n}(\pi,\rho_{0},x,y)$ for the following predicate:

“the $x$th element of the branch generated by $\rho_{0}$ in $\pi$ is $y$”

To be precise, the ‘element’ $y$ is given as a pair
$\langle\rho_{x},\Gamma_{x}\Rightarrow\Delta_{x}\rangle$ consisting of a
sequent $\Gamma_{x}\Rightarrow\Delta_{x}$ and an assignment $\rho_{x}$ that
invalidates it.

Notice that $\mathrm{Branch}_{n}(\pi,\rho_{0},x,y)$ is recursive w.r.t. the
oracle $\vDash_{n}$, and so is expressible by a ${\Delta}_{1}(\vDash_{n})$
formula, making it altogether ${\Delta}_{n+1}$ in its arguments. In fact, this
is demonstrably the case in $\mathrm{I}{\Sigma}_{n+1}$, which can prove that
$\mathrm{Branch}_{n}(\pi,\rho_{0},-,-)$ is the graph of a _function_ , as
shown in Prop. 18 below.

Let us write $\mathsf{conc}(\pi)$ for the conclusion of a $\mathsf{CA}$ proof
$\pi$ and, as in Sect. 3.2, $\mathcal{A}^{\pi}_{b}$ and
$\mathcal{A}^{\pi}_{t}$ for its branch and trace automata, resp. When we write
$\mathbb{N},\rho\vDash_{n}(\Gamma\Rightarrow\Delta)$ we mean the
${\Delta}_{n+1}$ formula
$(\mathbb{N},\rho\nvDash_{n}\bigwedge\Gamma)\vee(\mathbb{N},\rho\vDash_{n}\bigvee\Delta)$.

######  Proposition 18.

For $n\geq 0$, there are $\mathrm{I}{\Sigma}_{n+1}$ proofs of size polynomial
in $n$ of:

$\begin{array}[]{l}\forall\pi\text{ a $\mathsf{CA}$ preproof containing only
${\Sigma}_{n}$ formulae}.\\\ \forall\rho_{0}.\
((\mathbb{N},\rho_{0}\nvDash_{n}\mathsf{conc}(\pi))\supset\mathrm{Branch}_{n}(\pi,\rho_{0},-,-)\in\mathcal{L}(\mathcal{A}^{\pi}_{b}))\end{array}$
(12)

######  Proof 6.3.

Working in $\mathrm{I}{\Sigma}_{n+1}$, let $\pi$ and $\rho_{0}$ satisfy the
hypotheses of (12) above. The fact that
$\mathrm{Branch}_{n}(\pi,\rho_{0},-,-)$ is deterministic, cf. (6), follows
directly by induction on the position of the branch. The difficult part is to
show that $\mathrm{Branch}_{n}(\pi,\rho_{0},-,-)$ is total, cf. (5), i.e. that
it never reaches a deadlock. For this we show,

$\forall x.\exists\langle\rho_{x},\Gamma_{x}\Rightarrow\Delta_{x}\rangle.\
(\mathrm{Branch}_{n}(\pi,\rho_{0},x,\langle\rho_{x},\Gamma_{x}\Rightarrow\Delta_{x}\rangle)\wedge\
\mathbb{N},\rho_{x}\nvDash_{n}(\Gamma_{x}\Rightarrow\Delta_{x}))$ (13)

by ${{\Sigma}_{n+1}}$-induction on $x$. The base case, when $x=0$, follows by
assumption, so we proceed with the inductive case. For a given $x$ let
$\langle\rho_{x},\Gamma_{x}\Rightarrow\Delta_{x}\rangle$ witness (13) above
and let $\mathsf{r}$ be the rule instance in $\pi$ that
$\Gamma_{x}\Rightarrow\Delta_{x}$ concludes.

If $\mathsf{r}$ is a $\exists\text{-}r$ step with associated term $t$, then
there is only one premiss which we show remains false in the current
assignment. This follows from:

$\begin{array}[]{rcll}\mathbb{N},\rho\nvDash_{n}\exists
x.\varphi&\implies&\mathbb{N},\rho\vDash_{n}\forall x.\neg\varphi&\text{by
Prop.~{}\ref{prop:tarski}.\ref{item:tarski-not}}\\\ &\implies&\forall
y.(\mathbb{N},\rho\cup\\{x\mapsto y\\}\vDash_{n}\neg\varphi)&\text{by
Prop.~{}\ref{prop:tarski}.\ref{item:tarski-forall}}\\\
&\implies&\mathbb{N},\rho\cup\\{x\mapsto\rho(t)\\}\vDash_{n}\neg\varphi&\text{by
pure logic}\\\ &\implies&\mathbb{N},\rho\vDash_{n}\neg\varphi[t/x]&\text{by
Prop.~{}\ref{prop:tarski}.\ref{item:tarski-subst}}\\\
&\implies&\mathbb{N},\rho\nvDash_{n}\varphi[t/x]&\text{by
Prop.~{}\ref{prop:tarski}.\ref{item:tarski-not}.}\end{array}$

If $\mathsf{r}$ is a $\forall\text{-}r$ step then there is only one premiss,
for which we show that the appropriate invalidating assignment exists. This
follows from,

$\begin{array}[]{rcll}\mathbb{N},\rho\nvDash_{n}\forall
x.\varphi&\implies&\mathbb{N},\rho\vDash_{n}\exists x.\neg\varphi&\text{by
Prop.~{}\ref{prop:tarski}.\ref{item:tarski-not}}\\\ &\implies&\exists
y.(\mathbb{N},\rho\cup\\{x\mapsto y\\}\vDash_{n}\neg\varphi)&\text{by
Prop.~{}\ref{prop:tarski}.\ref{item:tarski-exists}}\\\ &\implies&\exists\text{
least }y.(\mathbb{N},\rho\cup\\{x\mapsto y\\}\vDash_{n}\neg\varphi)&\text{by
${\Sigma}_{n+1}\text{-}\mathsf{IND}$ }\\\ &\implies&\exists\text{ least
}y.(\mathbb{N},\rho\cup\\{x\mapsto y\\}\nvDash_{n}\varphi)&\text{by
Prop.~{}\ref{prop:tarski}.\ref{item:tarski-not}.}\end{array}$

where, in the penultimate implication, we rely on the fact that the
appropriate ‘minimisation’ property is provable in
${\Sigma}_{n+1}\text{-}\mathsf{IND}$ (see, e.g., [Bus98]).

If $\mathsf{r}$ is a left quantifier step then it is treated similarly to the
two right quantifier cases above by De Morgan duality. If $\mathsf{r}$ is a
propositional step then the treatment is simple, following directly from Prop.
16. If $\mathsf{r}$ is an initial sequent we immediately hit a contradiction,
since all of the axioms are provably true in all assignments. If $\mathsf{r}$
is a substitution step, then the existence of the appropriate assignment
follows directly from the substitution property, Prop. 16.6.

Finally, we may show that every state of the run of
$\mathrm{Branch}_{n}(\pi,\rho_{0},-,-)$ on $\mathcal{A}^{\pi}_{b}$ is final,
by ${\Sigma}_{n+1}$-induction, since it always correctly follows a branch of
$\pi$. Thus we have that
$\mathrm{Branch}_{n}(\pi,\rho_{0},-,-)\in\mathcal{L}(\mathcal{A}^{\pi}_{b})$.

Now we can give a formalised proof of the soundness of cyclic proofs:

######  Theorem 19 (Soundness of cyclic proofs, formalised).

For $n\geq 0$, there are $\mathrm{I}{\Sigma}_{n+2}$ proofs of size polynomial
in $n$ of:

$\begin{array}[]{l}\forall\pi\text{ a $\mathsf{CA}$ preproof containing only
${\Sigma}_{n}$ formulae}.\\\
(\mathcal{A}^{\pi}_{b}\sqsubseteq\mathcal{A}^{\pi}_{t}\ \supset\
\forall\rho_{0}.\ \mathbb{N},\rho_{0}\vDash_{n}\mathsf{conc}(\pi))\end{array}$
(14)

######  Proof 6.4.

First, instantiating $X$ in Cor. 15 with a ${\Delta}_{n+1}$ formula
$\varphi_{n}$ yields $O(|\varphi_{n}|)$-size $\mathrm{I}{\Sigma}_{n+2}$ proofs
of (11)$[\varphi_{n}/X]$. Hence, setting $\varphi_{n}$ to be
$\mathrm{Branch}_{n}(\pi,\rho_{0},-,-)$ and appealing to Prop. 18 above, we
arrive at $\mathrm{I}{\Sigma}_{n+2}$ proofs of size polynomial in $n$ of:

$\begin{array}[]{l}\forall\pi\text{ a $\mathsf{CA}$ preproof containing only
${\Sigma}_{n}$ formulae}.\\\
\mathcal{A}^{\pi}_{b}\sqsubseteq\mathcal{A}^{\pi}_{t}\supset\forall\rho_{0}.(\mathbb{N},\rho_{0}\nvDash_{n}\mathsf{conc}(\pi)\supset\mathrm{ArAcc}(\mathrm{Branch}_{n}(\pi,\rho_{0},-,-),\mathcal{A}^{\pi}_{t}))\end{array}$
(15)

Now, working in $\mathrm{I}{\Sigma}_{n+2}$, to prove (14) let $\pi$ satisfy
$\mathcal{A}^{\pi}_{b}\sqsubseteq\mathcal{A}^{\pi}_{t}$. For contradiction
assume, for some $\rho_{0}$, that
$\mathbb{N},\rho_{0}\nvDash_{n}\mathsf{conc}(\pi)$. By Prop. 18 we have
$\mathrm{Branch}_{n}(\pi,\rho_{0},-,-)\in\mathcal{L}(\mathcal{A}^{\pi}_{b})$,
so we henceforth write $\Gamma_{x}\Rightarrow\Delta_{x}$ and $\rho_{x}$ for
the sequent and assignment at the $x$th position of
$\mathrm{Branch}_{n}(\pi,\rho_{0},-,-)$. By (15) above we have
$\mathrm{ArAcc}(\mathrm{Branch}_{n}(\pi,\rho_{0},-,-),\mathcal{A}^{\pi}_{t})$,
so let $x$ witness its outer existential, cf. (9). Now, let $y$ be the maximum
value of $\rho_{x}(t)$ for all terms $t$ occurring in
$\Gamma_{x}\Rightarrow\Delta_{x}$. Again by
$\mathrm{ArAcc}(\mathrm{Branch}_{n}(\pi,\rho_{0},-,-),\mathcal{A}^{\pi}_{t})$,
we have that there is some (finite) trace $z$ beginning from
$\Gamma_{x}\Rightarrow\Delta_{x}$ that progresses $y+1$ times. Writing $z(i)$
to denote the $i$th term in the trace $z$, we may show by induction on
$i\leq|z|$ that, if there are $j$ progress points between $z(0)$ and $z(i)$,
then we have that $\rho_{x}(z(0))\geq\rho_{x+i}(z(i))+j$. In particular,
$y\geq\rho_{x}(z(0))\geq\rho_{x+|z|}(z(|z|))+(y+1)\geq y+1$, yielding a
contradiction.

###  6.3. $\mathsf{PA}$ exponentially simulates $\mathsf{CA}$

We can now give our main proof complexity result:

######  Theorem 20.

If $\pi$ is a $\mathsf{CA}$ proof of $\varphi$, then we can construct a
$\mathsf{PA}$ proof of $\varphi$ of size exponential in $|\pi|$.

######  Proof 6.5.

Take the least $n\in\mathbb{N}$ such that $\pi$ contains only ${\Sigma}_{n}$
formulae; in particular $n\leq|\pi|$. Since $\pi$ is a correct cyclic proof,
there is a $\mathsf{PA}$ proof of
$\mathcal{A}^{\pi}_{b}\sqsubseteq\mathcal{A}^{\pi}_{t}$, by exhaustive search.
In fact, such a proof in $\mathsf{Q}$ may be constructed in exponential time
in $|\pi|$, thanks to Obs. 5.2 and $\Sigma_{1}$-completeness of $\mathsf{Q}$
(see, e.g., [HP93]). Hence, by instantiating $\pi$ in Thm. 19, we have
$\mathrm{I}{\Sigma}_{n+2}$ proofs of $\mathbb{N},\varnothing\vDash_{n}\varphi$
of size exponential in $|\pi|$. Finally by the reflection property, Prop. 17,
we have that $\mathrm{I}{\Sigma}_{n+2}\vdash\varphi$ with proofs of size
exponential in $|\pi|$.

Notice that we already have a converse polynomial simulation of $\mathsf{PA}$
in $\mathsf{CA}$ by the results of [Sim17] or, alternatively, by Prop. 7.

##  7\. $\mathrm{I}{\Sigma}_{n+1}$ contains $\mathrm{C}{\Sigma}_{n}$

In fact the proof method we developed in the last section allows us to recover
a result on logical complexity too. By tracking precisely all the bounds
therein, we obtain that $\mathrm{C}{\Sigma}_{n}$ is contained in
$\mathrm{I}{\Sigma}_{n+2}$, which is already an improvement to Simpson’s
result (see Sect. 10 for a comparison). To derive such bounds, in this section
we concern ourselves only with cyclic proofs containing ${\Sigma}_{n}$
formulae. The universal closures of the conclusions of such proofs axiomatise
$\mathrm{C}{\Sigma}_{n}$, cf. Dfn. 3.1, so more complex theorems of
$\mathrm{C}{\Sigma}_{n}$ are thence derivable by pure logic.

In fact, we may actually improve this logical bound and arrive at an optimal
result (given Thm. 8). By more carefully analysing the proof methods of
[KMPS19], namely an inspection of the proofs of Thms. 5 and 12 in that work,
we have that:

######  Proposition 21 (Implicit in [KMPS19]).

$\mathsf{RCA}_{0}\vdash\forall X\in
A^{\omega}.(X\in\mathcal{L}(\mathcal{A}^{c})\equiv
X\notin\mathcal{L}(\mathcal{A}))$, for any NBA $\mathcal{A}$.

Notice here that the universal quantification over NBA is _external_ , so that
the complementation proofs are not necessarily uniform. This is not a trivial
result, since it relies on a version of Ramsey’s theorem, the _additive Ramsey
theorem_ , which can be proved by induction on the number of ‘colours’. Usual
forms of Ramsey’s theorem are not proved by such an argument, and in fact it
is well known that $\mathsf{RCA}_{0}$ cannot even prove Ramsey’s theorem for
pairs with only two colours (see, e.g., [Hir14]). We include in App. B a self-
contained (and somewhat simpler) proof of Prop. 21 above, for completeness.

This allows us to ‘un-uniformise’ the results of the previous section, using
Prop. 21 above instead of Lemma 12.3, in order to ‘trade off’ proof complexity
for logical complexity:

######  Proposition 22 (Soundness of cyclic proofs, non-uniformly formalised).

Let $n\geq 0$ and $\pi$ be a $\mathsf{CA}$ proof containing only
${\Sigma}_{n}$ formulae.
$\mathrm{I}{\Sigma}_{n+1}\vdash\forall\rho_{0}.(\mathbb{N},\rho_{0}\vDash_{n}\mathsf{conc}(\pi))$.

######  Proof 7.1 (Proof sketch).

We mimic the entire argument of Thm. 19 by instantiating the fixed proof $\pi$
and using Prop. 21 above instead of Lemma 12.3. In particular, the required
‘non-uniform’ versions of Thm. 14 and Cor. 15 become derivable in
$\mathsf{RCA}_{0}$ and $\mathrm{I}{\Sigma}_{1}(X)$ resp., thus reducing the
global induction complexity by one level. Hence we arrive at a ‘non-uniform’
version of Thm. 19, peculiar to the fixed proof $\pi$ we began with, proved
entirely within $\mathrm{I}{\Sigma}_{n+1}$, as required.

######  Theorem 23.

For $n\geq 0$, we have that
$\mathrm{C}{\Sigma}_{n}\subseteq\mathrm{I}{\Sigma}_{n+1}$.

######  Proof 7.2.

By the definition of $\mathrm{C}{\Sigma}_{n}$, cf. Dfn. 3.1, it suffices to
derive in $\mathrm{I}{\Sigma}_{n+1}$ just the (possibly open) conclusions of
$\mathrm{C}{\Sigma}_{n}$ proofs containing only ${\Sigma}_{n}$ formulae, and
so the result follows directly from Props. 22 and 17.

###  7.1. On the proof complexity of $\mathrm{C}{\Sigma}_{n}$

One might be tempted to conclude that the elementary simulation of
$\mathsf{CA}$ by $\mathsf{PA}$ should go through already for
$\mathrm{C}{\Sigma}_{n}$ by $\mathrm{I}{\Sigma}_{n+2}$ (independently of $n$),
due to the bounds implicit in the proof of Thm. 20. Furthermore, if we are
willing to give up a few more exponentials in complexity, one may even bound
the size of $\mathrm{I}{\Sigma}_{1}$ proofs arising from Prop. 21 by an
appropriate elementary function (though this analysis is beyond the scope of
this paper).

However, we must be conscious of the ‘robustness’ of the definition of
$\mathrm{C}{\Sigma}_{n}$ proofs in terms of complexity. The one we gave, which
essentially requires cyclic proofs to contain only ${\Sigma}_{n}$-formulae, is
more similar to ‘free-cut free’ $\mathrm{I}{\Sigma}_{n}$ proofs than general
ones, cf. Thm. 3, so it seems unfair to compare these notions of proof in
terms of proof complexity. In fact we may define a more natural notion of a
$\mathrm{C}{\Sigma}_{n}$ proof from the point of view of complexity, while
inducing the same theory.

First, let us recall some notions from, e.g., [Bro06, BS11]. Any cyclic proof
can be written in ‘cycle normal form’, where any ‘backpointer’ (e.g., the
conclusions of upper sequents marked $\bullet$ until now) points only to a
sequent that has occurred below it in the proof. Referring to the terminology
of [Bro06, BS11] etc., we say that a sequent is a _bud_ in a cyclic proof if
it has a backpointer pointing to an identical sequent (called the
_companion_).

######  Proposition 24.

If $\varphi$ has a $\mathsf{CA}$ proof whose buds and companions contain only
${\Sigma}_{n}$ formulae then $\mathrm{C}{\Sigma}_{n}\vdash\varphi$.

######  Proof 7.3 (Proof idea).

Once again, we simply apply free-cut elimination, Thm. 3, treating any
backpointers as ‘initial sequents’ for a proof in cycle normal form.

This result again shows the robustness of the definition of
$\mathrm{C}{\Sigma}_{n}$ as a theory, and we would further argue that, from
the point of view of proof complexity, the backpointer-condition induced by
Prop. 24 above constitutes a better notion of ‘proof’ for
$\mathrm{C}{\Sigma}_{n}$. One could go yet further and argue that an even
better notion of ‘proof’ would allow pointers to any other identical sequent
in the proof (not just those below it), which could potentially make for an
exponential improvement in proof complexity.

At the same time we see that it is not easy to compare the proof complexity of
such systems for $\mathrm{C}{\Sigma}_{n}$ with those for
$\mathrm{I}{\Sigma}_{n+1}$, due to the fact that we have used a free-cut
elimination result for the simulations in both directions, inducing a possibly
non-elementary blowup in proof size. It would be interesting if a more fine-
grained result regarding the relative proof complexity of
$\mathrm{I}{\Sigma}_{n+1}$ and $\mathrm{C}{\Sigma}_{n}$ could be established,
but this is beyond the scope of the current work.

##  8\. Some metamathematical results

In this section we make some further observations on various properties of the
cyclic theories in this work, which are later applied in Sect. 9. The
exposition we give is brief, since we follow standard methods, but we provide
appropriate references for the reader.

###  8.1. Provably recursive functions of $\mathrm{C}{\Delta}_{0}$

As a corollary of the Thms. 8 and 23 we have that, for $n\geq 1$, the provably
recursive functions of $\mathrm{C}{\Sigma}_{n}$ coincide with those of
$\mathrm{I}{\Sigma}_{n+1}$. Such functions were characterised by Parsons in
[Par72] as certain fragments of Gödel’s system $\mathsf{T}$ or, equivalently,
by recursion up to suitably bounded towers of $\omega$, e.g. in [Bus95]. This
apparently leaves open a gap for the case of $\mathrm{C}{\Delta}_{0}$ (a.k.a.
$\mathrm{C}{\Sigma}_{0}$). However notice that from the definition of
$\mathrm{C}{\Sigma}_{n}$ and Thm. 8 we have:

######  Corollary 25 (of Thm. 8).

$\mathrm{C}{\Sigma}_{n}$ is axiomatised by the ${\Pi}_{n+1}$-consequences of
$\mathrm{I}{\Sigma}_{n+1}$, for $n\geq 0$.

In particular, since $\mathrm{I}{\Delta}_{0}$ is known to be
${\Pi}_{1}$-axiomatised (see, e.g., Thm. 1.27 in [HP93]), we have that in fact
$\mathrm{C}{\Delta}_{0}\supseteq\mathrm{I}{\Delta}_{0}$ (i.e. over _all_
theorems). Thus $\mathrm{C}{\Delta}_{0}$ can prove recursive _at least_ the
functions (bitwise computable) in the linear-time hierarchy, from the
analogous result for $\mathrm{I}{\Delta}_{0}$ (see, e.g., Theorem III.4.8 in
[CN10]). Conversely, since $\mathrm{C}{\Delta}_{0}$ is also
${\Pi}_{1}$-axiomatised by the above observation, it has no more
‘computational content’ than $\mathrm{I}{\Delta}_{0}$, as we will now see.

Recall that the linear-time hierarchy ($\mathbf{LTH}$) is the class of
predicates expressible by a ${\Delta}_{0}$ formula in the language of
arithmetic.777Equivalently it is the class of predicates recognised by an
alternating Turing machine with random access in a linear number of steps with
only boundedly many alternations. See, e.g., [CK02] for more details. A
function is said to be in $\mathbf{FLTH}$ just if it has linear growth rate
(in terms of the bit string representation) and is bitwise computable in
$\mathbf{LTH}$.

######  Proposition 26.

If $\mathrm{C}{\Delta}_{0}\vdash\forall\vec{x}.\exists!y.\varphi(\vec{x},y)$
for a ${\Sigma}_{1}$-formula $\varphi$, then $\varphi$ computes the graph of a
function in $\mathbf{FLTH}$.

######  Proof 8.1 (Proof sketch).

Suppose $\varphi$ is $\exists\vec{y}.\varphi_{0}$ with
$\varphi_{0}\in{\Delta}_{0}$. By ‘Parikh’s theorem’ for
${\Pi}_{1}$-axiomatised theories (see, e.g., Thm. III.2.3 in [CN10]) we
moreover have
$\mathrm{C}{\Delta}_{0}\vdash\forall\vec{x}.\exists!y<t.\exists\vec{y}<\vec{t}.\varphi_{0}$
for some terms $t,\vec{t}$. This means we may simply search for a witness
$y<t$ of linear size verifying $\exists\vec{y}<\vec{t}.\varphi_{0}$, an
$\mathbf{LTH}$ property, and thus $\exists\vec{y}<\vec{t}.\varphi_{0}$
computes the graph of a function in $\mathbf{FLTH}$.

Interestingly, we cannot strengthen the above proposition to
“$\mathrm{C}{\Delta}_{0}$ and $\mathrm{I}{\Delta}_{0}$ prove the same
${\Pi}_{2}$ theorems”. This is because $\mathrm{I}{\Sigma}_{1}$ proves the
_consistency_ of $\mathrm{I}{\Delta}_{0}$, a ${\Pi}_{1}$ sentence, so
$\mathrm{C}{\Delta}_{0}$ does too by Thm. 8. Thus the aforementioned stronger
statement would contradict Gödel’s second incompleteness theorem for
$\mathrm{I}{\Delta}_{0}$.

See, e.g., [Bus98, CN10] for further discussions on the provably recursive
functions of fragments of (bounded) arithmetic, and see, e.g., [CK02] for more
details on relationships between the language of arithmetic and recursive
function classes.

###  8.2. Failure of cut-admissibility

As a corollary of our results, we may formally conclude that the cut rule is
not admissible in $\mathsf{CA}$, or indeed any of its fragments
$\mathrm{C}{\Sigma}_{n}$.888This observation was pointed out to me by Stefano
Berardi. In fact the situation is rather worse than that:

######  Corollary 27 (of Thms. 8 and 23).

Let $n\geq 1$. The class of $\mathsf{CA}$ proofs with only ${\Sigma}_{n-1}$
cuts is not complete for even the ${\Pi}_{1}$ theorems of
$\mathrm{C}{\Sigma}_{n}$.

######  Proof 8.2.

For a recursively axiomatised theory $T$, let $\mathsf{Con}({T})$ be an
appropriate ${\Pi}_{1}$ sentence expressing that “$T$ does not prove $0=1$”.
It is well-known that
$\mathrm{I}{\Sigma}_{n+1}\vdash\mathsf{Con}({\mathrm{I}{\Sigma}_{n}})$ (see,
e.g., [Kay91, Bus98, HP93]), so also
$\mathrm{C}{\Sigma}_{n}\vdash\mathsf{Con}({\mathrm{I}{\Sigma}_{n}})$ by Thm.
8. For contradiction, suppose $\mathsf{Con}({\mathrm{I}{\Sigma}_{n}})$
concludes some $\mathsf{CA}$ proof with only ${\Sigma}_{n-1}$ cuts; then in
fact $\mathrm{C}{\Sigma}_{n-1}\vdash\mathsf{Con}({\mathrm{I}{\Sigma}_{n}})$ by
degeneralising (for the case $n=1$) and the subformula property. However this
implies $\mathrm{I}{\Sigma}_{n}\vdash\mathsf{Con}({\mathrm{I}{\Sigma}_{n}})$
by Thm. 23, which is impossible by Gödel’s second incompleteness theorem for
$\mathrm{I}{\Sigma}_{n}$.

See, e.g., [Bus98, Kay91, HP93] for further discussions on the provability of
consistency principles for fragments of arithmetic.

###  8.3. Reflection and consistency

Thanks to the uniformity of the results from Sect. 6, we can give some
fundamental metalogical properties regarding provable soundness and
consistency of cyclic proofs. First we will fix our formalisation of
$\mathrm{C}{\Sigma}_{n}$-provability (of arbitrary sequents, not just
${\Sigma}_{n}$) in the language of arithmetic.

Let $n\geq 0$. We will fix some appropriate formula
$\mathsf{Prf}_{n}(\pi,\varphi)$ expressing that $\pi$ is a
$\mathrm{C}{\Sigma}_{n}$ proof of $\varphi$. We suppose that proofs are
written as usual derivations (finite trees or dags) whose leaves are either
axiom instances from $\mathsf{Q}$, or otherwise some (possibly open)
${\Sigma}_{n}$ sequent labelled by an associated cyclic proof that derives it
(containing only ${\Sigma}_{n}$ formulae). Descriptively,
$\mathsf{Prf}_{n}(x,y)$ checks that $\pi$ is a proof of $\varphi$ by first
checking that it is a well-formed derivation, then checking that each premiss
is either an axiom instance from $\mathsf{Q}$ or is labelled by a correct
cyclic proof deriving it. In the latter case it must search for a certificate
verifying that the cyclic proof satisfies the automaton-inclusion condition,
i.e. that $\mathcal{A}_{b}\sqsubseteq\mathcal{A}_{t}$.

While $\mathsf{Prf}_{n}(\pi,\varphi)$ is recursive in $\pi$ and $\varphi$,
this may not be provably the case in weak theories such as
$\mathrm{I}{\Delta}_{0}$. Thus we fix $\mathsf{Prf}_{n}$ to be an appropriate
${\Sigma}_{1}$ formula, as described above, and we write $\square_{n}\varphi$
for $\exists\pi.\mathsf{Prf}_{n}(\pi,{{\varphi}})$. We write
${\Pi}_{k}\text{-}\mathsf{Rfn}({\mathrm{C}{\Sigma}_{n}})$ for the (local)
_${\Pi}_{k}$ -reflection principle_ of $\mathrm{C}{\Sigma}_{n}$. I.e.

${\Pi}_{k}\text{-}\mathsf{Rfn}({\mathrm{C}{\Sigma}_{n}})\ :=\
\\{\square_{n}\varphi\supset\varphi:\varphi\in{\Pi}_{k}\\}$

######  Corollary 28 (of Thm. 19).

For $n\geq 0$, we have
$\mathrm{I}{\Sigma}_{n+2}\vdash{\Pi}_{n+1}\text{-}\mathsf{Rfn}({\mathrm{C}{\Sigma}_{n}})$.

######  Proof 8.3.

Let $\varphi(\vec{x})$ be a ${\Sigma}_{n}$ formula. Working in
$\mathrm{I}{\Sigma}_{n+2}$, suppose that $\square_{n}\forall\vec{x}.\varphi$
(so that $\mathrm{C}{\Sigma}_{n}\vdash\forall\vec{x}.\varphi(\vec{x})$). We
may assume that every formula occurring in a $\mathrm{C}{\Sigma}_{n}$ proof of
the sequent $\Rightarrow\varphi(\vec{x})$ is ${\Sigma}_{n}$, thanks to free-
cut elimination, Thm. 3 (recall that this result is provable already in
$\mathrm{I}{\Sigma}_{1}$). Thus we have
$\mathbb{N},\varnothing\vDash_{n+1}\forall\vec{x}.\varphi(\vec{x})$ by Thm. 19
and Prop. 16.5, whence the result follows by the reflection property, Prop.
17.

Notice that, while the statement of Cor. 28 above is peculiar to the current
formulation of a $\mathrm{C}{\Sigma}_{n}$ proof, $\mathsf{Prf}_{n}$, it holds
also under any other notion of proof that is provably equivalent in
$\mathrm{I}{\Sigma}_{n+2}$. In particular, in Sect. 7.1 we discussed another
notion of proof for $\mathrm{C}{\Sigma}_{n}$ which, morally, allowed “free
cuts” to occur inside cycles. Since the equivalence of the two formulations,
Prop. 24, is proved using only free-cut elimination and basic reasoning, all
formalisable in $\mathrm{I}{\Sigma}_{1}$, the version of Cor. 28 for that more
liberal notion of a $\mathrm{C}{\Sigma}_{n}$ proof holds too.

As usual, we may see ${\Pi}_{1}$-reflection as another formulation of
‘consistency’. Let us write $\mathsf{Con}({\mathrm{C}{\Sigma}_{n}})$ for the
sentence $\neg\square_{n}0=1$ (notice that this is a ${\Pi}_{1}$ sentence).

######  Corollary 29 (of Thm. 19).

For $n\geq 0$, we have
$\mathrm{I}{\Sigma}_{n+2}\vdash\mathsf{Con}({\mathrm{C}{\Sigma}_{n}})$

######  Proof 8.4.

Follows immediately from Cor. 28 above by substituting $0=1$ for $\varphi$.

We will see in the next subsection that this result is, in fact, optimal with
respect to logical complexity.

###  8.4. Incompleteness

Unsurprisingly, all the theories $\mathrm{C}{\Sigma}_{n}$ suffer from Gödel’s
incompleteness theorems. Even though $\mathrm{C}{\Sigma}_{n}$ is not
explicitly defined axiomatically, it does have a recursively enumerable notion
of provability, namely $\square_{n}$, and so must be incomplete with respect
to this notion (see, e.g., Thm. 2.21 in [HP93]):

######  Theorem 30 (Gödel’s second incompleteness theorem, for cyclic
theories).

For $n\geq 0$, as long as $\mathrm{C}{\Sigma}_{n}$ is consistent (i.e.
$\mathrm{C}{\Sigma}_{n}\nvdash 0=1$), we have
$\mathrm{C}{\Sigma}_{n}\nvdash\mathsf{Con}({\mathrm{C}{\Sigma}_{n}})$.

Consequently we have that Cor. 29 is, in fact, optimal in terms of logical
complexity:

######  Corollary 31.

For $n\geq 0$, we have
$\mathrm{I}{\Sigma}_{n+1}\nvdash\mathsf{Con}({\mathrm{C}{\Sigma}_{n}})$.

######  Proof 8.5.

Suppose otherwise. Then also
$\mathrm{C}{\Sigma}_{n}\vdash\mathsf{Con}({\mathrm{C}{\Sigma}_{n}})$ by
${\Pi}_{1}$-conservativity, cf. Thm. 8, which contradicts Gödel’s second
incompleteness above, Thm. 30.

We will see in the next section that this has a curious consequence for the
reverse mathematics of results in $\omega$-automaton theory.

##  9\. On the logical strength of McNaughton’s theorem

In this section we show how the results of this work yield an unexpected
corollary: certain formulations of _McNaugton’s theorem_ , that every NBA has
an equivalent deterministic ‘parity’ or ‘Muller’ automaton, are not provable
in $\mathsf{RCA}_{0}$. The general question of the logical strength of
McNaughton’s theorem was notably left open in the recent work [KMPS19].

Our result is non-uniform in the sense that unprovability holds for any
_explicit_ primitive recursive determinisation construction. As far as the
author is aware this accounts for all known proofs of McNaughton’s theorem,
suggesting that it is unlikely to be provable at all, in its usual uniform
version, in $\mathsf{RCA}_{0}$. That said, we point out that the statement of
McNaughton’s theorem itself is arguably not so well-defined in the context of
reverse mathematics: it is not clear in $\mathsf{RCA}_{0}$ that different
versions of the theorem coincide, namely with respect to the choice of (a)
acceptance conditions (parity, Muller, etc.) and (b) formulation of the set of
states infinitely often hit during a run (negative, $\forall$, vs. positive,
$\exists$).

Our argument is based on an alternative route to proving the soundness of
$\mathrm{C}{\Sigma}_{n}$. Assuming that an appropriate version of McNaughton’s
theorem is indeed provable in $\mathsf{RCA}_{0}$, we are in fact able to
formalise the soundness argument for $\mathrm{C}{\Sigma}_{n}$ already in
$\mathrm{I}{\Sigma}_{n+1}$. However, consequently we have that
$\mathrm{I}{\Sigma}_{n+1}$ proves the consistency of $\mathrm{C}{\Sigma}_{n}$,
and so $\mathrm{C}{\Sigma}_{n}$ proves its own consistency by
${\Pi}_{1}$-conservativity, cf. Thm. 8, which is absurd by Gödel’s second
incompleteness theorem for $\mathrm{C}{\Sigma}_{n}$, Thm. 30.

###  9.1. Deterministic parity automata and universality

Due to space considerations, we only briefly present the details of parity
automata. The reader is encouraged to consult, e.g., [Tho97], for further
details on automaton theory for $\omega$-languages.

A (non-deterministic) Rabin or parity automaton (NRA) is a just a NBA where,
instead of a set of final states $F$, we have a function $c:Q\to\mathbb{N}$,
called a colouring. A word is accepted by a NRA if it has a run in which the
least colour of a state occurring infinitely often is even. The notion of
deterministic parity automaton (DRA) is analogous to that of a DBA, i.e.
requiring the transition relation to be deterministic and total.

[McNaughton, [McN66]] For every NBA $\mathcal{A}$, we can effectively
construct a DRA accepting the same language.

Actually, McNaughton gave this result for deterministic _Muller_ automata
rather than parity automata. The equivalence of these two models is well-known
though, as we previously mentioned, it is not clear whether $\mathsf{RCA}_{0}$
can prove their equivalence. The fact that we use parity automata here is
arbitrary; we believe a similar exposition could be carried out for Muller
automata.

As for DBA, we may naturally express language acceptance for a DRA
$\mathcal{A}=(A,Q,\delta,q_{0},c)$ by an arithmetical formula, i.e. without SO
quantifiers. For our purposes, it will be useful to take a ‘negative’
formulation of acceptance:

$X\in\mathcal{L}(\mathcal{A})\ :=\ \forall q\in
Q.\left(\left(\begin{array}[]{rl}&\forall x.\exists x^{\prime}>x.\
q_{X}(x^{\prime})=q\\\ \wedge&\exists x.\forall x^{\prime}>x.\
c(q_{X}(x^{\prime}))\geq c(q)\end{array}\right)\supset\text{``$c(q)$ is
even''}\right)$

We write $\sigma:q_{1}\underset{\delta}{\overset{*}{\rightarrow}}q_{2}$ if a
word $\sigma\in A^{*}$ determines a path along $\delta$ starting at $q_{1}$
and ending at $q_{2}$. We write $\underset{\delta}{\overset{+}{\rightarrow}}$
when the path is nonempty. A _simple loop_ about a state $q\in Q$ is a
nonempty path along $\delta$ beginning and ending at $q$ that visits no
intermediate state more than once.

Recall that we call an $\omega$-automaton _universal_ if it accepts all
$\omega$-words over its alphabet. We write $\mathrm{Univ}(\mathcal{A})$ for a
standard recursive procedure testing universality of a DRA $\mathcal{A}$: “for
every odd-coloured state $q$ reachable from $q_{0}$, any simple loop about $q$
contains a state coloured by an even number $<c(q)$”. More formally, writing
$\sigma^{\prime}\leq\sigma$ if $\sigma^{\prime}$ is a prefix of $\sigma$:

$\mathrm{Univ}(\mathcal{A})\ :=\ \begin{array}[]{l}\ \ \forall
q\underset{\delta}{\overset{*}{\leftarrow}}q_{0}.\
\forall\sigma:q\underset{\delta}{\overset{+}{\rightarrow}}q.\\\
\left(\begin{array}[]{rl}&\text{``$\sigma$ is a simple
loop''}\wedge\text{``$c(q)$ is odd''}\\\
\supset&\exists\sigma^{\prime}\leq\sigma.\ \exists q^{\prime}\in Q.\
(\sigma^{\prime}:q\underset{\delta}{\overset{+}{\rightarrow}}q^{\prime}\
\wedge\text{``$c(q^{\prime})$ even''}\wedge
c(q^{\prime})<c(q))\end{array}\right)\end{array}$

Clearly this formula is provably ${\Delta}^{0}_{1}$ in $\mathsf{RCA}_{0}$.
Furthermore:

######  Proposition 32.

$\mathsf{RCA}_{0}\vdash\forall\text{ DRA }\mathcal{A}.\
(\mathrm{Univ}(\mathcal{A})\equiv\forall X\in
A^{\omega}.X\in\mathcal{L}(\mathcal{A}))$.

######  Proof 9.1.

Working in $\mathsf{RCA}_{0}$, let $\mathcal{A}=(A,Q,\delta,q_{0},c)$ be a
DRA. For the left-right implication, suppose there is some $X\in A^{\omega}$
such that $X\notin\mathcal{L}(\mathcal{A})$. Thus we have some $q\in Q$ such
that $c(q)$ is odd and the following hold:

$\forall x.\exists x^{\prime}>x.\ q_{X}(x^{\prime})=q$ (16) $\exists x.\forall
x^{\prime}>x.\ c(q_{X}(x^{\prime}))\geq c(q)$ (17)

Let $x_{0}$ be a witness to (17), and let $x_{0}<x_{1}<x_{2}$ such that
$q_{X}(x_{1})=q_{X}(x_{2})=q$, by two applications of (16). We will need the
following intermediate (arithmetical) result,

If $\sigma:q\underset{\delta}{\overset{+}{\rightarrow}}q$, there is a
subsequence $\sigma^{\prime}$ of $\sigma$ that is a simple loop on $q$.

which follows directly by induction on $|\sigma|$, eliminating intermediate
loops at each inductive step in the case of non-simplicity. Now we apply this
result to the sequence $(X(x))^{x_{2}}_{x=x_{1}}$ to obtain a simple loop
about $q$; moreover since this will be a subsequence of
$(X(x))^{x_{2}}_{x=x_{1}}$, we have that any even-coloured state occurring in
it is coloured $>c(q)$, since $x_{0}$ witnesses (17) and $x_{0}<x_{1}<x_{2}$,
so $\neg\mathrm{Univ}(\mathcal{A})$.

For the right-left implication, we proceed again by contraposition. Suppose
$\neg\mathrm{Univ}(\mathcal{A})$, and let
$\sigma:q_{0}\underset{\delta}{\overset{*}{\rightarrow}}q$ and
$\tau:q\underset{\delta}{\overset{+}{\rightarrow}}q$ such that $c(q)$ is odd,
and $\tau$ is a simple loop containing no states coloured $<c(q)$. We may now
set $X=\sigma\tau^{\omega}$ (which is easily defined by comprehension) and
show that $X\notin\mathcal{L}(\mathcal{A})$. For this it suffices to show (16)
and (17) above. For the former, given $x$ we set
$x^{\prime}=|\sigma|+m|\tau|>x$, for some sufficiently large $m$. For the
latter, we set $x=|\sigma|$ as the witness to the outer existential, whence
(17) follows by construction of $\tau$.

###  9.2. Reducing soundness of $\mathrm{C}{\Delta}_{0}$ to a version of
McNaughton’s theorem

Henceforth we may write $\mathcal{L}(\mathcal{A})=\mathcal{L}(\mathcal{B})$ as
shorthand for $\forall X.(X\in\mathcal{L}(\mathcal{A})\equiv
X\in\mathcal{L}(\mathcal{B}))$, where $\mathcal{A}$ and $\mathcal{B}$ may be
any type of automaton thus far encountered with respect to their associated
notions of membership. Based on our ‘negative’ formulation of DRA acceptance,
we define for a (definable) function $d$:

$\mathsf{McNaughton}^{-}_{d}\ :=\ \forall\text{ NBA
}\mathcal{A}.(\text{``$d(\mathcal{A})$ is a
DRA''}\wedge\mathcal{L}(\mathcal{A})=\mathcal{L}(d(\mathcal{A}))$

Assuming this is provable in $\mathsf{RCA}_{0}$ for some primitive recursive
function $d$, we will reproduce a version of Thm. 14 in
$\mathrm{I}{\Sigma}_{n+1}$. The idea is that, rather than expressing the fact
that $\mathcal{L}(\mathcal{A}_{1})\subseteq\mathcal{L}(\mathcal{A}_{2})$ by
saying “$(\mathcal{A}_{1}^{c}\sqcup\mathcal{A}_{2})^{c}$ is empty”, as we did
in Sects. 6 and 7, we may rather express it as
“$\mathcal{A}_{1}^{c}\sqcup\mathcal{A}_{2}$ is universal”, relying on
$\mathsf{McNaughton}^{-}_{d}$ and Prop. 32 above.

For a DBA $\mathcal{A}_{1}$ and a NBA $\mathcal{A}_{2}$ we define
$\mathcal{A}_{1}\sqsubseteq_{d}\mathcal{A}_{2}$ as
$\mathrm{Univ}(d(\mathcal{A}_{1}^{c}\sqcup\mathcal{A}_{2})))$. Let us write
$(\ref*{eqn:arith-form-prog-traces}_{d})$ for the equation (11) with
$\sqsubseteq$ replaced by $\sqsubseteq_{d}$, i.e.:

$\forall\ \text{DBA}\ \mathcal{A}_{1},\forall\ \text{NBA}\ \mathcal{A}_{2}.\
\left((\mathcal{A}_{1}\sqsubseteq_{d}\mathcal{A}_{2}\wedge
X\in\mathcal{L}(\mathcal{A}_{1}))\supset\mathrm{ArAcc}(X,\mathcal{A}_{2})\right)$
($\ref*{eqn:arith-form-prog-traces}_{d}$)

We have the following analogue to Thm. 14:

######  Proposition 33.

$\mathsf{RCA}_{0}+\mathsf{McNaughton}^{-}_{d}\vdash\eqref{eqn:arith-form-prog-
traces'}$.

######  Proof 9.2.

Mimicking the proof of Thm. 14, we work in $\mathsf{RCA}_{0}$ and suppose
$X\in\mathcal{L}(\mathcal{A}_{1})$ and
$\mathcal{A}_{1}\sqsubseteq_{d}\mathcal{A}_{2}$. We have:

$\begin{array}[]{rll}&\mathrm{Univ}(d(\mathcal{A}_{1}^{c}\sqcup\mathcal{A}_{2}))&\text{since
$\mathcal{A}_{1}\sqsubseteq_{d}\mathcal{A}_{2}$}\\\ \implies&\forall Y\in
A^{\omega}.Y\in\mathcal{L}(\mathcal{A}_{1}^{c}\sqcup\mathcal{A}_{2})&\text{by
Prop.~{}\ref{prop:rca-prov-corr-univ-dra} and
$\mathsf{McNaughton}^{-}_{d}$}\\\ \implies&\forall Y\in
A^{\omega}.(Y\in\mathcal{L}(\mathcal{A}^{c}_{1})\vee
Y\in\mathcal{L}(\mathcal{A}_{2}))&\text{by Lemma~{}\ref{lem:aut-clos-props-in-
so-arith}.\ref{item:union-rca} }\\\ \implies&\forall Y\in
A^{\omega}.(Y\in\mathcal{L}(\mathcal{A}_{1})\supset
Y\in\mathcal{L}(\mathcal{A}_{2}))&\text{by Lemma~{}\ref{lem:aut-clos-props-in-
so-arith}.\ref{item:compl-dba-rca}}\\\
\implies&X\in\mathcal{L}(\mathcal{A}_{2})&\text{since
$X\in\mathcal{L}(\mathcal{A}_{1})$}\\\
\implies&\mathrm{ArAcc}(X,\mathcal{A}_{2})&\text{by Prop.~{}\ref{prop:arith-
acc}.}\end{array}$

We may use this result to reconstruct the entire formalised soundness argument
for $\mathrm{C}{\Sigma}_{n}$ of Sect. 6 in $\mathrm{I}{\Sigma}_{n+1}$ instead
of $\mathrm{I}{\Sigma}_{n+2}$, assuming $\mathsf{McNaughton}^{-}_{d}$. In
particular, using Prop. 33 above instead of Thm. 14, we may recover versions
of Cor. 15, Thm. 19 and Cor. 28 for $\mathrm{I}{\Sigma}_{n+1}$ instead of
$\mathrm{I}{\Sigma}_{n+2}$, with respect to ($\ref*{eqn:arith-form-prog-
traces}_{d}$) instead of (11). Formally, let
${\Pi}_{k}\text{-}\mathsf{Rfn}_{d}({\mathrm{C}{\Sigma}_{n}})$ denote the
formulation of the ${\Pi}_{k}$-reflection principle for
$\mathrm{C}{\Sigma}_{n}$ induced by using $\sqsubseteq_{d}$ instead of
$\sqsubseteq$ throughout Sect. 8.3, with respect to the definitions of
$\mathsf{Prf}_{n}$ and $\square_{n}$. Similarly, let
$\mathsf{Con}_{d}({\mathrm{C}{\Sigma}_{n}})$ be the induced consistency
principle.

######  Proposition 34.

For $n\geq 0$, if $\mathsf{RCA}_{0}\vdash\mathsf{McNaughton}^{-}_{d}$ for some
primitive recursive function $d$, then
$\mathrm{I}{\Sigma}_{n+1}\vdash{\Pi}_{n+1}\text{-}\mathsf{Rfn}_{d}({\mathrm{C}{\Sigma}_{n}})$,
so in particular
$\mathrm{I}{\Sigma}_{n+1}\vdash\mathsf{Con}_{d}({\mathrm{C}{\Sigma}_{n}})$.

######  Proof 9.3 (Proof sketch).

The argument goes through just like that of Cors. 28 and 29 of Thm. 19, except
that we use Prop. 33 instead of Thm. 14. Appealing to the assumption that
$\mathsf{RCA}_{0}\vdash\mathsf{McNaughton}^{-}_{d}$, this version of the
argument requires only ${\Sigma}^{0}_{1}\text{-}\mathsf{IND}$ instead of
${\Sigma}^{0}_{2}\text{-}\mathsf{IND}$, thus yielding
$\mathrm{I}{\Sigma}_{n+1}$ proofs overall once we substitute the appropriate
formulae for $X$.

######  Theorem 35.

$\mathsf{RCA}_{0}\nvdash\mathsf{McNaughton}^{-}_{d}$, for any primitive
recursive function $d$.

######  Proof 9.4 (Proof sketch).

The same argument as Cor. 31 holds for our revised notion of consistency; in
particular we have that
$\mathrm{I}{\Sigma}_{1}\nvdash\mathsf{Con}_{d}({\mathrm{C}{\Delta}_{0}})$. The
result now follows immediately by the contraposition of Prop. 34 above, for
$n=0$.

##  10\. Conclusions and further remarks

In this work we developed the theory of cyclic arithmetic by studying the
logical complexity of its proofs. We showed that inductive and cyclic proofs
of the same theorems require similar logical complexity, and obtained tight
quantifier complexity bounds in both directions. We further showed that the
proof complexity of the two frameworks differs only elementarily, although it
remains unclear how to properly measure proof complexity for the fragments
$\mathrm{C}{\Sigma}_{n}$, even if the theory itself seems well-defined and
robust. Many of these issues constitute avenues for further work.

###  10.1. Comparison to the proofs of [BT17b] and [Sim17]

One reason for our improved quantifier complexity compared to [Sim17], is that
Simpson rather relies on _Weak König’s Lemma_ ($\mathsf{WKL}$) to obtain an
infinite branch when formalising the soundness argument for cyclic proofs.
This, _a priori_ , increases quantifier complexity of the argument, since
$\mathsf{WKL}$ is known to be unprovable in $\mathsf{RCA}_{0}$ even in the
presence of ${\Sigma}^{0}_{2}\text{-}\mathsf{IND}$; in fact, it is
incomparable to ${\Sigma}^{0}_{2}\text{-}\mathsf{IND}$ (see, e.g., [KMPS19]).
That said, we believe that the ‘bounded-width $\mathsf{WKL}$’
($\mathsf{bwWKL}$) of [KMPS19] should suffice to carry out Simpson’s proof,
and this principle is provable already in
$\mathsf{RCA}_{0}+{\Sigma}^{0}_{2}\text{-}\mathsf{IND}$. Applying this
strategy to his proof yields only that
$\mathrm{C}{\Sigma}_{n}\subseteq\mathrm{I}{\Sigma}_{n+3}$, since
$\mathsf{bwWKL}$ is applied to a ${\Pi}^{0}_{n+1}$ set, though this should
improve to a $\mathrm{I}{\Sigma}_{n+2}$ bound by using the non-uniform version
of NBA complementation implicit in [KMPS19], cf. Prop. 21. We reiterate that
the main improvement here is in giving a uniform formulation of those results;
not only does this lead to a better proof complexity result, cf. Thm. 20, but
we also recover a metamathematical account of the theories
$\mathrm{C}{\Sigma}_{n}$, cf. 8.

Berardi and Tatsuta’s approach, [BT17b], is rather interesting since it is
arguably more ‘structural’ in nature, relying on proof-level manipulations
rather than reflection principles. That said there are still crucial sources
of logical complexity blowup, namely in an ‘arithmetical’ version of _Ramsey’s
theorem_ (Thm. 5.2) and the consequent _Podelski-Rybalchenko termination
theorem_ (Thm. 6.1). Both of these apparently increase quantifier complexity
by several levels, and so their approach does not seem to yield comparable
logical bounds to this work. Since proof complexity is not a primary
consideration of their work, it is not simple to track the precise bounds in
[BT17b]. There are some apparent sources of exponential blowups,999For
instance, Lemma 8.4 in that work yields a set of apparently exponential size
in the worst case, and this bounds from below the size of the overall
translation, e.g. as in Lemma 8.7. though it seems that the global simulation
is elementary. As before, we reiterate that the major improvement in the
present work is in the uniformity of our exposition: the approach of [BT17b]
is fundamentally non-uniform so does not yield any metamathematical account of
cyclic arithmetic.

###  10.2. On the correctness criteria for cyclic proofs

Since the algorithms used to check correctness of a cyclic preproof reduce to
the inclusion of Büchi automata, the exponential simulation of $\mathsf{CA}$
by $\mathsf{PA}$ is optimal, unless there is a nondeterministic
subexponential-time algorithm for $\mathbf{PSPACE}$ or, more interestingly,
there is an easier way to check cyclic proof correctness. (In fact,
technically, it would suffice to have an easier criterion for a _larger_ class
of preproofs that were, nonetheless, sound.) As far as we know,
$\mathbf{PSPACE}$ remains the best known upper bound for checking the
correctness of general cyclic preproofs, although efficient algorithms have
recently been proposed for less general correctness criteria, cf. [Str17,
NST18]. Thus, it would be interesting to prove a corresponding lower bound or
otherwise improve the upper bound. Conditional such results could be obtained
via, say, certain polynomial upper bounds on proof complexity in
$\mathsf{CA}$: for instance, if $\mathsf{CA}$ were to have polynomial-size
proofs of each correct Büchi inclusion then cyclic proof correctness would not
be polynomial-time checkable, unless $\mathbf{NP}=\mathbf{PSPACE}$.
Unfortunately naïve attempts at this approach fail, but the general question
of whether $\mathsf{PA}$ and $\mathsf{CA}$ are exponentially separated seems
pertinent.

On the other hand, the translation of Lemma 9 from inductive proofs to cyclic
proofs is rather structured. In light of the converse result in Sect. 6 it
might make sense in further work, from the point of view of logical
complexity, to consider only cyclic proofs accepted by some weaker more
efficiently verified criterion, such as [Str17, NST18].

###  10.3. Interpreting ordinary inductive definitions in arithmetic

In earlier work by Brotherston and Simpson, cyclic proofs were rather
considered over a system of FO logic extended by ‘ordinary’ _Martin-Löf_
inductive definitions [ML71], known as $\mathrm{FOL}_{\mathit{ID}}$ [Bro06,
BS07, BS11]. Berardi and Tatsuta showed in [BT17b] that the cyclic system
$\mathsf{CLKID}^{\omega}$ for $\mathrm{FOL}_{\mathit{ID}}$ is equivalent to
the inductive system $\mathsf{LKID}$, when at least arithmetic is present,
somewhat generalising Simpson’s result [Sim17]. We point out that ordinary
Martin-Löf inductive definitions can be _interpreted_ in arithmetic in the
usual way by a ${\Sigma}_{1}$ inductive construction of ‘approximants’, and a
proof of $\mathsf{CLKID}^{\omega}$ may be similarly interpreted line-by-line
in $\mathsf{CA}$. (This is similar to the role of the ‘stage number
predicates’ in [BT17b].) In particular, this means that
$\mathsf{CLKID}^{\omega}(+\mathsf{PA})$ is _conservative_ over $\mathsf{CA}$.
We reiterate that the interest behind the results of [BT17b] is rather the
structural nature of the transformations, but this observation also
exemplifies why $\mathsf{CA}$ is a natural and canonical object of study, as
argued in [Sim17].

###  10.4. Cyclic propositional proof complexity

One perspective gained from this work comes in the setting of _propositional
proof complexity_ (see, e.g., [CN10, Kra95]). Thm. 8 of Sect. 4 should
relativise to theories with oracles too. For instance, we may formalise in
$\mathrm{C}{\Delta}_{0}(f)$, where $f$ is a fresh (uninterpreted) function
symbol, a proof of the relativised version of the (finitary) pigeonhole
principle (see App. A). This formula is known to be unprovable in
$\mathrm{I}{\Delta}_{0}(f)$ due to lower bounds on propositional proofs of
bounded depth [KPW95, PBI93].

At the same time the ‘Paris-Wilkie’ translation [PW81], which fundamentally
links $\mathrm{I}{\Delta}_{0}(f)$ to bounded-depth propositional proofs, works
locally on an arithmetic proof, at the level of formulae. Consequently one may
still apply the translation to the lines of a $\mathrm{C}{\Delta}_{0}(f)$
proof to obtain small ‘proof-like’ objects containing only formulae of bounded
depth, and a cyclic proof structure. One would expect that this corresponds to
some strong form of ‘extension’, since it is known that adding usual extension
to bounded systems already yields full ‘extended Frege’ proofs. However at the
same time, some of this power has been devolved to the proof structure rather
than simply at the level of the formula, and so could yield insights into how
to prove simulations between fragments of Hilbert-Frege systems with
extension.

We point out that recent work, [AL18], relating cyclic proof structures to
proof complexity has already appeared, albeit with a different correctness
criterion.

## Acknowledgments

I am indebted to Alex Simpson for encouraging me to pursue this work and for
his valuable feedback. Similarly, I would like to thank Stefano Berardi for
several illuminating discussions on metalogical matters regarding cyclic
proofs. Finally, I would like to thank James Brotherston, Guilhem Jaber,
Alexis Saurin and the anonymous reviewers for this and previous versions of
this work for all their helpful comments and insights.

## References

  * [AL17] Bahareh Afshari and Graham E. Leigh.  Cut-free completeness for modal $\mu$-calculus.  In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017, pages 1–12, 2017\.