Circular and non-wellfounded proofs have become an increasingly popular tool for metalogical treatments of systems with forms of induction and/or recursion. In this work we investigate the expressivity of a variant $\C$ of Gödel's system $\T$ where programs are circularly typed, rather than including an explicit recursion combinator.
In particular, we examine the abstraction complexity (i.e. type level) of $\C$, and show that the Gödel primitive recursive functionals may be typed more succinctly with circular derivations, using types precisely one level lower than in $\T$.
In fact we give a logical correspondence between the two settings, interpreting the quantifier-free type 1 theory of level $n+1$ $\T$ into that of level $n$ $\C$ and vice-versa.

We also obtain some further results and perspectives on circular `derivations', namely strong normalisation and confluence, models based on hereditary computable functionals, continuity at type 2, and a translation to terms of $\T$ computing the same functional, at all types.

§ INTRODUCTION

In recent years non-wellfounded proofs have attracted increasing attention.
The modern inception of the area arguably lies with the celebrated work [51] of Niwinski and Walukiewicz, where a circular analytic tableau system was proved sound and complete for Kozen's modal $\mu$-calculus [39].
Since then several distinct lines of research have emerged, in particular pivoting towards proof theoretical aspects of non-wellfounded reasoning:

* Modal logic. Niwinski and Walukiewicz's system has been recast as more traditional sequent based systems in, e.g., the works [21] for the linear time fragment, and [60] for the general fragment, both offering alternative cut-free completeness proofs. Recently more `constructive' proofs have emerged of both these results, namely [23] and [2]. Similar results may be readily recovered for many other fixed point modal logics.

* Predicate logic. Brotherston and Simpson initiated a program for non-wellfounded proof theory based on predicate logic [9, 10]. Here, syntactic correctness criteria from modal logic, themselves inspired by automaton theory, were adapted to provide a sound circular proof theory for forms of inductive definitions. This approach has found applications in automated theorem proving  [8, 6, 54], and more recently variations of these systems in the setting of first-order arithmetic have been investigated [59, 12, 19, 18].

* Type systems. Recently, formulations of cyclic proofs through the lens of the Curry-Howard correspondence have garnered attention in the French school of proof theory. Fortier and Santocanale, also inspired by [51], seem to have been the first of the modern era to give a cut-elimination result for circular proofs with the aforementioned correctness conditions,[Of course, in this regard, one must also mention Mints' famous `continuous cut-elimination' [50]; while his approach indeed seems to apply, the main difficulty herein seems to be the preservation of syntactic correctness at the limit.] namely for additive linear logic with least and greatest fixed points [28]. This was generalised in later work to the logic including multiplicatives too (for closed formulas) in [7], and with more expressive correctness conditions recently in [5]. Deepening this Curry-Howard viewpoint, presentations of `proof nets' have recently appeared [26], yielding a form of Natural Deduction for circular proofs.

* Algebras. Inspired by the aforementioned work on type systems, there have been many recent applications to classes of algebras based on fixed points, in particular the Kleene star. [24] has presented a cut-free complete system for Kleene algebra, and established a cut-elimination result for it and the extension by residuals and meets (i.e. Lambek calculus + Kleene star) in [25].
These have been used directly to obtain alternative completeness results, e.g. [20], and have inspired recent undecidability results, e.g. for the logic of action lattices [46], which solved a longstanding open problem.

A key motivation in all these areas is the so-called `Brotherston-Simpson conjecture': are cyclic proofs and inductive ones equally powerful? Naturally, the answer depends on how one interprets `equally powerful', e.g. as provability, proof complexity, logical complexity etc., as well as on the logic at hand. One example of this nuance is readily found in the setting of first-order logic:

* Berardi and Tatsuta have shown that first-order proofs with induction, over particular inductive definitions, do not prove the same theorems as cyclic ones [11].

* Simpson in [59] and Berardi and Tatsuta in [12] have independently shown that inductive and cyclic proofs are equally powerful in the presence of Peano Arithmetic.

* Both these results were refined in [19] where it was shown that provability by cyclic proofs containing only $\Sigma_n$ formulas ($C\Sigma_n$) coincides with provability by $\Sigma_{n+1}$-induction ($I\Sigma_{n+1}$), over $\Pi_{n+1}$ theorems.

The current work is somewhat inspired by the line of work just mentioned, in the sense that it attempts to understand the Brotherston-Simpson question for type systems and their corresponding equational theories at the level of abstraction complexity (or type level).
In particular, motivated by the results for arithmetic mentioned above, our natural starting point is Gödel's `system $\T$' [30].

$\T$ is a multi-sorted classical quantifier-free theory over a simply typed programming language based on primitive recursion at all finite types.
Gödel's celebrated Dialectica functional interpretation [30] allows all of first-order arithmetic to be interpreted by this simple theory,[In fact, Gödel's interpretation was only for the intuitionistic theory Heyting Arithmetic. Peano Arithmetic may be duly interpreted upon composition with a suitable double negation translation.] essentially trading off logical complexity of quantifiers for abstraction complexity in functional programs.
This tradeoff was made precise by Parsons in [52]: the fragment $I\Sigma_{n+1}$ of Peano Arithmetic is $\mathit{ND}$-interpreted into the fragment of $\T$ admitting only type $n$ recursion ($\nT n$).
Naturally, a converse result holds too, in the sense that
$\nT n$ may be interpreted into appropriate fragments of arithmetic where the interpretation of types is relativised to classes of hereditarily computable functionals.

In this work we present a circular (or cyclic) version $\C$ of Gödel's $\T$, where typing derivations may be non-wellfounded, but remain finitely presentable.
At the level of the type system, we simply adapt the correctness conditions of many of the previously mentioned works to the language of simple types.
At the level of the theory we admit the same axioms as $\T$, in particular quantifier-free induction, and include a form of extensional equality.
Our main result is that, similar to the arithmetic setting, $\C$ and $\T$ are mutually interpretable.
In fact, we obtain a similar refinement: the type $n$ restriction of $\C$ ($\nC n$) is interpretable in $\nT{n+1}$ and vice versa, over at least the type 1 quantifier-free theory.
Intuitively this means that cyclic typing derivations, and their induced theory, are more succinct than ones in $\T$, by precisely 1 type level.

Our arguments, however, are more subtle and technical than the analogous ones from [19], since we are working simultaneously with systems for typing and systems for reasoning within a theory.
We take a proof mining approach to interpreting $\C$ in $\T$, formalising a totality argument in suitable fragments of `second-order'[As for simple type theory, the allusion to `second' or `higher' order is only suggestive: formally speaking these are multi-sorted first-order settings and not bona fide second or higher order.] arithmetic.
Extraction of witnessing functionals and corresponding specifications in fragments of $\T$ follow by the aforementioned results of Parsons, under well-known conservation results over fragments of first-order arithmetic.
Notably, since we are unable to formalise the standard set theoretic model of higher order functionals, we take a detour through the model theory of $\T$, in particular presenting `coterm' models that play the roles of the hereditarily recursive (and hereditarily effective) operations.
We give a rewriting theoretic implementation of program execution, and establish a confluence result within $\RCA$, yielding determinism of normalising programs.
The interpretation of $\C$ in $\T$ is then a consequence of the fact that these type structures indeed constitute models of $\C$.
For the refinement at each type level, we take advantage of recent results on the reverse mathematics of cyclic proof checking from [19], inspired by [37, 36].

Our ultimate motivation is to establish a correspondence between two of the proof theoretic worlds mentioned at the start: predicate logic and type systems.
In future work we would like to establish a `circular Dialectica' functional interpretation, thereby completing the picture and formally associating the two settings.

§.§ Related work

Kuperberg, Pinault and Pous have notably also studied non-wellfounded typing derivations inspired by $\T$ in [40], in particular investigating affinity.
Their types are closed under a `Kleene star' operation for list formation, inspired by previous works such as [25], and are equivalent to the usual notion of simple (or finite) types. They show that the affine fragment of this type system, where contraction is omitted, computes precisely the primitive recursive functions in the standard set-theoretic model, generalising a similar result by Dal Lago for affine $\T$ [47].
They also show that, in the presence of contraction, their type 1 fragment computes just the type 1 primitive recursive functionals (à la Gödel), i.e. those computed by type 1 terms of $\T$ in the standard model.

This latter result is subsumed by and, in particular, refined in the current work in terms of type level  (we discuss this further in Section <ref>).
Moreover, the point of this work is to establish a logical correspondence between fragments of $\C$ and $\T$, i.e. at the level of their equational/quantifier-free theories, not only at the level of interpretation of their terms in the standard model.

§.§ Outline and prerequisites

The remainder of this paper is structured as follows.
In Section <ref> we give some preliminaries on Church's simple type theory and we recall system $\T$ in Section <ref>, in particular giving a sequent-style presentation of typing derivations.

In Section <ref> we present non-wellfounded typing derivations (`coderivations'), in particular giving semantic results with respect to the standard model such as extensional completeness at type 1, Turing completeness for the regular fragment and, of course, well-definedness of the induced functionals. This section concludes with the definition of $\C$ and its type-level-restricted fragments $\nC n$.

In Section <ref> we give a simulation of $\nT{n+1} $ within $\nC n$, over the type $n+1$ theory, in the presence of extensionality.

The techniques of this section are entirely proof-theoretic.

In Section <ref> we turn to the model theory of $\C$. We recast traditional type structures of hereditarily recursive and hereditarily effective operations into `coterm' models, in light of the aforementioned Turing-completeness result. At the base level, program execution is implemented as a rewrite system induced from the equational axioms in the usual way; in particular we prove a confluence result, yielding determinism of computation.

In Section <ref> we formalise the aforementioned type structures within fragments of second-order arithmetic, in particular proving (within these fragments) that they constitute models of $\C$ (with extensionality).
By applying standard proof mining results, we obtain an interpretation of $\nC n$ into $\nT{n+1}$, over the type 1 equational theory, a converse result to that of Section <ref>.

Finally, in Section <ref> we give some further results and perspectives on $\C$ coterms, in particular obtaining type 2 continuity, weak and strong normalisation, and a translation to $\T$ terms computing the same functional.
We also discuss proof theoretic strength, cut-elimination and the incorporation of fixed point operators.

It would not be pertinent to give a purely self-contained presentation of the content herein, since we rely on a number of established disciplines.
That said, we aim for a level of exposition that highlights the significance and subtleties of our results and techniques for the general proof theorist.

Naturally, it is helpful to have some background with Gödel's system $\T$ and the Dialectica functional interpretation (though we shall not explicitly work with it), for which [1] is an excellent survey and [67, 38] are more comprehensive.
There are also excellent references for the technical disciplines underlining this work, namely rewriting theory (e.g. [66]), reverse mathematics (e.g.  [57, 31]) and higher-order computability theory (e.g. [48]).

Finally, we give metamathematical accounts of many of our results,[This is for two reasons: (a) for self-contained interest; while some such results are probably folklore, they have not appeared elsewhere, as far as we know; and, more importantly, (b) since we exploit these metamathematical resuls in Section <ref> in order to interpret $\C$ within $\T$.] and so assume
some familiarity with
metamathematics of first- and second-order arithmetic (e.g. [33], also [35] for a recursion-theoretic viewpoint and [67] for a constructive viewpoint).

§ PRELIMINARIES ON CHURCH'S SIMPLE TYPE THEORY

At the heart of Gödel's $\T$ is a rudimentary version of Church's Simple Type Theory [16].
Since we later consider a rather non-standard `circular' calculus $\C$, we will here give a presentation of simple type theory that underlies both $\T$ and $\C$.

§.§ Simple types

Throughout this work we will deal with terms that are simply typed. (Simple) types, written $\sigma, \tau $ etc., are defined as follows:

* $\nat$ is a type.

* If $\sigma $ and $\tau$ are types, then so is $(\sigma \to \tau)$.

We typically omit parentheses on types when they are associated to the right. E.g., we may write $\rho \to \sigma \to \tau$ instead of $\rho \to (\sigma \to \tau)$ and so on.

We define the level of a type $\sigma$, written $\level (\sigma)$, inductively as follows:

* $\level (\nat) = 0$

* $\level (\sigma \to \tau) = \max (1 + \level (\sigma), \level (\tau))$.

Every type $\sigma$ can be uniquely written as $\sigma_1 \to \cdots \to \sigma_n \to \nat$, for some $n \in \Nat$.
In this case we sometimes write $\vec \sigma$ for $(\sigma_1, \dots, \sigma_n)$ and, as an abuse of notation, we also sometimes write $\vec \sigma \to \nat$ for $\sigma$.

We call $n$ here the arity of $\sigma$ (in reference to the type isomorphism $\rho \to \sigma \to \tau \equiv (\rho \times \sigma) \to \tau$).
Note that, in this case, $\level (\sigma) = 1 + \max\limits_{i=1}^n (\level (\sigma_i))$.

§.§ Simply typed theories (STTs)

A simply typed language is a multi-sorted first-order language,

whose sorts are just the simple types.

The simply typed languages considered in this work will consist of some basic set of constants of simple type, called combinators, as well as infinitely many variables, written $x,y,z$ etc., of each simple type.
We may sometimes indicate the type of a variable (or term) as superscript to aid parsing, e.g. writing $x^\sigma$ for a variable $x$ of type $\sigma$.

Terms are formed from constants (and variables) by typed application:

* Any constant or variable of type $\sigma$ is a term of type $\sigma$.

* if $s$ and $t$ are terms of types $\sigma$ and $\sigma \to \tau$, respectively, then $(t \comp s)$ is a term of type $\tau$.

We usually just omit the application symbol $\comp$, e.g. writing $t\, s$ instead of $t \comp s$, and omit parentheses for long applications when they are associated to the left, e.g. writing $r\, s\, t$ for $(r\, s)\, t$ and so on.
We do not include a $\lambda$-abstraction operation as primitive, instead requiring that it is coded by constants and composition for combinatory completeness (see, e.g., Fact <ref>).

Formally speaking, being in a multi-sorted first-order framework, `application' itself comprises a family of operations, one for each pair of types $(\sigma \to \tau, \sigma)$.
We shall gloss over this formality in what follows, unless we need to distinguish application operations of differing types.

Simply typed languages, for us, always include a binary relation symbol $=_\sigma$ `equality at type $\sigma$', on each type $\sigma$.
Atomic formulas have the form $s=_\sigma t$, where $s$ and $t$ are terms of type $\sigma$, although we shall suppress the subscript $\sigma$ when it does not cause confusion.

Formulas are built from atomic ones in the usual way, using $\cnot$ (negation), $\cor$ (disjunction), $\cand$ (conjunction), $\cimp$ (implication), $\ciff$ (if and only if), $\exists$ (existential quantifier), and $\forall$ (universal quantifier).

Simply typed theories (or STTs) are (first-order, classical) theories over a (simply typed) language, typically specified by a set of quantifier-free axioms and rules.

We always assume that STTs include the axioms for equality from Figure <ref>.

*  $ t=_\sigma t$, for any term $t$ of type $\sigma$. (Reflexivity)

$(s =_\sigma t \cand  \phi(s))  \cimp \phi(t)$, for terms $s,t$ of type $\sigma$.

Axiom schemata for (intensional) equality.

We will also include a form of extensionality for equality given by the extensionality rule ($\extensionality$) in Figure <ref>.

If $\proves s \, \vec x \, = \, t\, \vec x\, $ then $\proves s=t$.

Extensionality rule.

Our inclusion of an equality symbol in all finite types coupled with a rule for extensionality is non-standard, but it eases some of the technical development.
Let us note, however, that our version has been previously considered in the literature, e.g. in [52] where $\extensionality$ is called `SI' and facilitates the translation from $I\Sigma_{n+1}$ into $\nT n$ (cf. Section <ref> later).

Our axiomatisation of equality thus sits somewhere between intensional or weakly extensional variants and the fully extensional variant.
Since our principal concern in this work is in comparing STTs by their type 1 theories, the precise variant of equality is not so important, vis a vis known extensionality-elimination techniques at lower types, cf. [49].
Weaker formulations, in particular weak extensionality, seem to suffice for certain results, but the appropriate proof adaptations seem to introduce technicalities that detract from our main purpose.
Thus such considerations are beyond the scope of this work, but they will naturally be of greater importance for related directions, in particular for proof interpretations.

§.§ Structures and the standard model

We consider usual Henkin structures for simply typed languages, called type structures. Note that we do not, a priori, require $=_\sigma$ to be interpreted as true equality on the interpretation of $\sigma$.

One particular structure, the `standard' or `full set-theoretic' model $\nmod$, is given by the following interpretation of types:

* $\nat^\nmod$ is $\Nat$.

* $(\sigma \to \tau )^\nmod$ is the set of functions $\sigma^\nmod \to \tau^\nmod$.

* $\comp^\nmod$ is just function application, i.e. given $f \in \sigma^\nmod$ and $g \in (\sigma \to \tau)^\nmod$, $g \comp^\nmod f \in \tau^\nmod$ is defined as $g(f)$.

* For each type $\sigma$, we have an extensional equality relation $=_\sigma^\nmod$:

* $=_\nat^\nmod$ is just equality of natural numbers;

* for $f,g \in (\sigma \to \tau )^\nmod$, we have $f=_{\sigma \to \tau}^\nmod g$ just if $ \forall x \in \sigma^\nmod .  f(x) =_\tau^\nmod g(x)$.

As a notational convention, for a function $f : X\to {Z^Y}$ and $x \in X$, $y\in Y$, we may write $f(x,y)$ for $f(x)(y)$, and so on, in reference to the usual `Currying' isomorphism $(Z^Y)^X \cong Z^{X \times Y}$.

This structure also has standard extensions to the STTs considered later in this work, which will be presented at the appropriate moments.

§.§ Example: Combinatory Algebra

The language of combinatory algebra consists of the following constants:

* $\Kcomb \sigma \tau$, for each pair $(\sigma, \tau)$, of type $\sigma \to \tau \to \sigma$.

* $\Scomb \rho \sigma \tau$, for each triple $(\rho, \sigma, \tau)$, of type $(\rho \to \sigma \to \tau) \to (\rho \to \sigma) \to \rho \to \tau$.

We will typically omit the type subscripts of the combinators in what follows when it is unambiguous.
Combinatory Algebra is a theory over this language that includes all axioms of the form:

\begin{equation}
\label{eqn:ks-comb-axioms}
\begin{array}{rcl}
\Kcomb{}{} \, x\, y & = &   x \\
\Scomb{}{}{} \, x\, y\, z & = &  x\, z\, (y\, z)
\end{array}
\end{equation}

The standard model $\nmod$ may be extended to a model of Combinatory Algebra by taking the equations above as definitions (oriented from left to right).

It is well-known that Combinatory Algebra is complete:

For each term $t$ of type $\tau$ and variable $x$ of type $\sigma$, there is a term $\lambda x t$ of type $\sigma \to \tau$ s.t. $\eqref{eqn:ks-comb-axioms} \proves\ (\lambda x t) \, y\ = \ t[y/x]$.

§.§ Sequent style type system

Sequent calculi give us a way to write typed terms that are more succinct with respect to type level, and also enjoy nice proof theoretic properties, e.g. cut-elimination.
From the point of view of the Curry-Howard correspondence, they associate sequent proofs of minimal logic to simply typed terms.
Importantly, the sequent presentation and its induced relations between type occurrences makes it easier to define our notion of progressing non-wellfounded derivation later.

Sequents are expressions $\vec \sigma \seqar \tau$, where $\vec \sigma$ is a list of types and $\tau $ is a type.
The rules for minimal logic are given in Figure <ref>.

\[
\vlinf{\exch}{}{\red{\vec \rho}, \blue{\rho}, \orange{\sigma}, \purple{\vec \sigma }\seqar \tau}{\red{\vec \rho},  \orange{\sigma}, \blue{\rho}, \purple{\vec \sigma }\seqar \tau}
\qquad
\vlinf{\wk}{}{\purple{\vec \sigma}, \blue{\sigma} \seqar \tau}{\purple{\vec \sigma }\seqar \tau}
\qquad
\vlinf{\cntr}{}{\purple{\vec \sigma}, \blue{\sigma} \seqar \tau}{\purple{\vec \sigma}, \blue{\sigma}, \blue{\sigma }\seqar \tau}
\qquad
\vliinf{\cut}{}{\purple{\vec \sigma }\seqar \tau}{\purple{\vec \sigma} \seqar  \sigma }{\purple{\vec \sigma}, \sigma \seqar \tau}
\]

\[
\vlinf{\id}{}{\purple{\sigma} \seqar \sigma}{}
\qquad
\vliinf{\leftimp}{}{\purple{\vec \sigma }, \blue{\rho \to \sigma} \seqar \tau}{\purple{\vec \sigma} \seqar \rho}{\purple{\vec \sigma}, {\sigma }\seqar \tau}
\qquad
\vlinf{\rightimp}{}{\purple{\vec \sigma }\seqar \sigma \to \tau}{\purple{\vec \sigma}, \sigma \seqar \tau}
\]

Sequent style typing rules from minimal logic.

Here, and throughout this section, colours of each type occurrence in typing rules may be ignored for now and will become relevant later in Section <ref>. That said, it may be illustrative for the reader to imagine that, once we give interpretations of these rules, type occurrences of the same colour will correspond to identical inputs for the corresponding functionals.
In this way, the colour assigned to a type on the LHS of a sequent is a sort of variable annotation for that occurrence.

Recall that, for a list of types $\vec \sigma = (\sigma_1, \dots, \sigma_n)$, we sometimes write $\vec \sigma \to \sigma$ for the type $\sigma_1 \to \cdots \to \sigma_n \to \sigma$.
Each rule instance (or step) determines a constant of the appropriate type:

* A step $\vlinf{}{}{\vec \tau \seqar \tau}{}$ is a constant of type $\vec \tau \to \tau$.

* A step $\vlinf{}{}{\vec \tau \seqar \tau}{\vec \sigma \seqar \sigma}$ is a constant of type
\(
(\vec \sigma \to \sigma) \to \vec \tau \to \tau
\).

* A step $\vliinf{}{}{\vec \tau \seqar \tau}{\vec \rho\seqar \rho}{\vec \sigma \seqar \sigma}$ is a constant of type
$(\vec \rho \to \rho) \to (\vec \sigma \to \sigma) \to \vec \tau \to \tau$.

We will usually refer to steps only by their labels, e.g. $\exch$, $\cntr$, $\rightimp$ etc., rather than explicitly indicating their types in the premisses and conclusions; unless otherwise clear from context, the associated typing should be assumed to be as given in the original specification of the rule, e.g. in Figure <ref>.

A sequent calculus derivation of $\vec \sigma \seqar \tau$ determines a term of type $\vec \sigma \to \tau$ in the expected way, by applying all the inference steps according to its structure.
Formally, derivations are construed as terms by inductively setting:

* $\vlderivation{
\vlin{\mathsf r}{}{\vec \tau \seqar \tau}{
\vltr{s}{\vec \sigma \seqar \sigma}{\vlhy{ \ }}{\vlhy{}}{\vlhy{\ }}
}$ is the term $\mathsf r\, s$; and,

* $\vlderivation{
\vliin{\mathsf r}{}{\vec \tau \seqar \tau}{
\vltr{r}{\vec \rho \seqar \rho}{\vlhy{\ }}{\vlhy{ }}{\vlhy{\ }}
\vltr{s}{\vec \sigma \seqar \sigma}{\vlhy{\ }}{\vlhy{ }}{\vlhy{\ }}
}$ is the term $\mathsf r\ r\, s$.

We write $t: \vec \sigma \seqar \tau$ if $t$ is a derivation of the sequent $\vec \sigma \seqar \tau$ (and so also a term of type $\vec \sigma \to \tau$).

Note that, strictly speaking, derivations form a strict subset of all closed terms, since they are not formally closed under application.
I.e., for $s:\ \seqar \sigma$ and $t:\sigma \seqar \tau$, we have that $t\, s $ is a term of type $\tau$, but $t\, s $ is not, in general, a derivation.[E.g., if $t$ concludes with a binary step, then the only way to write $t\, s $ in the form $\mathsf r\, r_1 \cdots r_n$, with $\mathsf r$ an inference step, requires $n>2$, which is not possible since all rules are at most binary.]
In what follows, we will see that we can interpret the term $t\, s$ as the derivation $\cut\, t\, s$ (with appropriate types), but it will nonetheless be convenient to distinguish these two terms.
In particular this interpretation does not admit the same notion of `thread' for non-wellfounded derivations we consider later.

While it may seem strange to adopt a sequent style type system but construe inference steps as combinators rather than meta-level operations on, say,  $\lambda$-terms, we adopt this approach to facilitate our later notions of non-wellfounded derivations and coterms.
This combinatory approach ensures that the `term associated to a derivation' is actually a continuous construction, so that when we later consider non-wellfounded derivations, the corresponding notion of `coterm' is well-defined.

On the other hand, why do we use the sequent calculus at all? This is due to the particular termination criterion we will adopt for non-wellfounded derivations later, exploiting  well-known notions of formula ancestry available in the sequent calculus.
This is why the sequent calculus is the standard formalism in circular proof theory.

We define the axiomatisation in Figure <ref>, where the types corresponding to each rule label are as indicated in the corresponding rule instance in Figure <ref>.

\[
\begin{array}{rcl}
\id \ x & = & x \\
\exch \ t \ \vec x\  x \ y\ \vec y & = & t \ \vec x \ y \ x \ \vec y \\
\wk \ t  \ \vec x \ x & = & t \ \vec x \\
\cntr \ t\ \vec x \ x & = & t \ \vec x \ x \ x \\
\cut \ s\ t\ \vec x & = & t \ \vec x \ (s \ \vec x ) \\
\leftimp \ s\ t\ \vec x\ y & = & t \ \vec x\ (y\ (r\ \vec x) ) \\
\rightimp \ t \ \vec x \ x & = & t\ \vec x\ x
\end{array}
\]

Equational axiomatisation of sequent calculus rules.

Note that, here and elsewhere, there is no formal reason why we distinguish the arguments corresponding to subderivations by term meta-variables, $s,t$ etc., and other arguments by variables $x,y$ etc. It is purely in order to facilitate the identification of the corresponding arguments. All axioms are closed under substitution of terms for variables.

The sequent calculus in Figure <ref>, under the axiomatisation in Figure <ref>, is equivalent to Combinatory Algebra (from Section <ref>).
In particular there are derivations for $\Kcomb \sigma \tau$ and $\Scomb \rho \sigma \tau$ that satisfy the corresponding equational axioms.
As a consequence, our sequent calculus is also combinatory complete.

The structure $\nmod$ from Section <ref> may be extended to one for Figures <ref> and <ref> by taking the equations of Figure <ref> as definitions, oriented left-to-right.

[Rules modulo exchange]

In the rest of this work, it will often be convenient to omit instances of exchange, $\exch$, in typing derivations and their corresponding notation as terms.
For example, we may freely write a `rule instance',

\begin{equation}
\label{eqn:cut-with-exchange}
\vliinf{\cut}{}{\purple{\vec \rho}, \blue{\vec \sigma} \seqar \tau}{\purple{\vec \rho}, \blue{\vec \sigma} \seqar \sigma}{\purple{\vec \rho}, \sigma , \blue{\vec \sigma }\seqar \tau}
\end{equation}

instead of the corresponding derivation with exchanges, and an `axiom',

\[
\cut\, s\, t\, \vec x\, \vec y \ = \ t\, \vec x\, (s\, \vec x\, \vec y)\, \vec y
\]

instead of the corresponding equation derived using the $\exch$ and $\cut $ axioms.
Again, we may omit typing of rule labels when it is unambiguous.

§ PRELIMINARIES ON GÖDEL'S SYSTEM $\T$

So far we have not imposed any restrictions on our base type $\nat$, despite the fact that the standard model $\nmod$ interprets $\nat$ as $\Nat$.
System $\T$ is a simple type theory that extends Combinatory Algebra by including new constants, axioms and rules that constrain the interpretation of $\nat$ to this effect.
Its definition is borne out over the following subsections.

§.§ Constants for natural numbers and recursion

The language of $\T$ extends the sequent system from Figure <ref> by the typing rules in Figure <ref>.
Again, we may omit the subscript (and other typing information) of an instance of $\rec_\tau$ when it is unambiguous.

\[
\vlinf{0}{}{\seqar \nat}{}
\qquad
\vlinf{\succ}{}{\purple{\nat} \seqar \nat}{}
\qquad
\vliinf{\rec_\tau}{}{ \purple{\vec \sigma}, \blue{\nat }\seqar \tau}{\purple{\vec \sigma }\seqar \tau}{ \purple{\vec \sigma}, \blue{\nat}, \sigma \seqar \tau}
\]

Typing rules for $0$, $\succ$ and $\rec_\tau$ combinators.

When writing terms, we assume $\succ$ binds stronger than application. This is usually visually signified since the symbol $\succ$ will appear in closer proximity to the term it is bound to. E.g. We write $s\ \succ t$ for $s \comp (\succ \comp t)$.

A numeral is a term of the form $\underbrace{\succ \cdots \succ}_n 0$, which we more succinctly write as $\numeral n$.

§.§ Recursion axioms

$\T$ includes as axioms the equations from Figure <ref>.

\[
\begin{array}{rcl}
\rec\ s\ t\ \vec x\  0 &=& s\, \vec x \\
\rec\ s\ t\ \vec x\ \succ y &=& t\ \vec x\ y \ (\rec\ s\ t\ \vec x \ y)
\end{array}
\]

Equational axioms for recursion combinators, where $y$ is a variable of type $\nat$.

Before concluding our definition of $\T$, let us note that the equational axioms thus far presented are enough to expose well-behaved computational content:[Note that this result also applies to alternative combinatorial bases such as ours, e.g. as noted in [15], Chapter B.]

Orienting the axioms of Figures <ref> and <ref> left-to-right yields a terminating and confluent rewriting system on closed terms of $\T$.

We will not elaborate now on the rewriting theoretic aspects of $\T$ since we will revisit it in more detail later in Section <ref>.
However, let us note that Tait's result above induces a well-behaved term model of $\T$, with equality simply comparing (unique) normal forms.
The point of Section <ref> is to establish similar models for the non-wellfounded type system we will introduce in Section <ref>, formalised in the setting of second-order arithmetic.

§.§ Number-theoretic axioms

Finally, $\T$ includes the axioms from Figure <ref>, indicating that $(0,\succ)$ generates a free and inductive structure.

*  $\cnot\,  \succ x = 0 $

*  $\succ x = \succ y\,  \cimp \, x=y$

If $\proves \phi(0)$ and $\proves \phi(x) \cimp \phi(\succ x)$ then $\proves \phi(t)$, for $\phi$ quantifier-free.

Number-theoretic axioms for $\T$, where $x$ and $y$ are variables of type $\nat$, and $t$ is a term of type $\nat$.

This concludes the definition of $\T$, i.e.:

$\T$ is the simple type theory over the language given by Figures <ref> and Figures <ref>,
axiomatised by the formulas and rules from Figures <ref>, <ref>, <ref>, <ref> and <ref>.

Going back to Fact <ref> and the succeeding discussion, one crucial property of $\T$ is that the only (closed) normal forms of type $\nat$ are numerals.
For the aforementioned term model induced by unique normal forms of closed terms,
this property allows the verification of the induction schema (<ref>) in Figure <ref> to be reduced to induction at the meta-level.
this property fails for the non-wellfounded calculus we will present in Section <ref> (see Remark <ref>), necessitating a somewhat specialised construction of corresponding models in Section <ref>.

§.§ The standard model and primitive recursive functionals

The standard model $\nmod$ from Section <ref> may be extended to one of $\T$ by setting,

* $0^\nmod:= 0 \in \Nat$.

* $\succ^\nmod (n) := n+1$.

and taking the axioms for $\rec$ from Figure <ref> as definitions, oriented left-to-right.
Note that the interpretation of $\rec$ is indeed well-defined by these axioms, provable by induction on $\Nat$.

The interpretations of terms in this model, i.e. the functionals $t^\nmod$, form a higher-order function algebra known as the (Gödel) primitive recursive functionals of finite type, written $\PRF{}$.
It is well-known by a result of Kreisel that its type 1 functions coincide with those definable by effective transfinite recursion up to $\epsilon_0$ [41, 42], and moreover that ordinal complexity (height of an $\omega$-tower) can be effectively traded off for abstraction complexity (type level) and vice-versa (cf., e.g., [63, 56]).

§.§ Restricting the level of recursors

The main subject of study in this work will be fragments of $\T$ induced by restricting the type level of recursors.

$\nT n$ is the restriction of $\T$ to the language containing only recursors $\rec_\sigma$ where $\level (\sigma) \leq n$.

The significance of these fragments was investigated in the seminal work of Parsons [52].
In particular we have:

If $\ISn{n+1} \proves \forall \vec x \exists  y A(\vec x,y)$, where $A$ is $\Delta_0$, then there is a $\nT n$ term $t$ with $\nT n \proves A(\vec x, t\, \vec x)$.[We assume here some standard encoding of $\Delta_0$ formulas into quantifier-free formulas of $\nT 0$. Alternatively we could admit bounded quantifiers into the language of $\T$, on which induction is allowed, without affecting expressivity. We shall gloss over this technicality here.]

In fact, this result is a direct consequence of Gödel's famous `Dialectica' functional interpretation [30], composed with a suitable negative translation.
The converse, that $\ISn{n+1}$ proves the totality of all type 1 terms of $\nT n$, is obtained by formalising models of hereditarily computable functionals similar to those in Section <ref>.
Both directions may be alternatively obtained via the aforementioned transfinite recursion theoretical characterisations of $\T$, using purely structural proof theoretic methods, cf.  [13].

Both results naturally extend to the conservative extension $\RCA + \CIND{\Sigma^0_{n+1}}$.

If $\RCA+ \ISn{n+1} \proves \forall \vec x \exists  y A(\vec x,y)$, where $A$ is $\Delta^0_0$, then there is a $\nT n$ term $t$ with $\nT n \proves A(\vec x, t\, \vec x)$.

For the results of Section <ref>, it will be useful to have the following normal form of typing derivations:

Let $t: \vec \sigma \seqar \tau$ be a $\nT n$ derivation, where $\tau$ and each $\sigma_i$ have level $\leq n$. Then there is a $\nT n$-derivation $t':\vec \sigma \seqar \tau$ such that $t^\nmod=t'^\nmod$.

Moreover, $\nT n \proves t = t' $.

Since we could not easily find an explicit statement of this in the literature, a self-contained proof is given in Appendix <ref>.

§.§ Example: typing the Ackermann-Péter function

Let us take a moment to see an example of typing and reasoning within $\T$.
The Ackermann-Péter function $A: \Nat \times \Nat \to \Nat$ is defined by the following equations:

\begin{equation}
\label{eqn:ackermann-equations}
\begin{array}{rcl}
A(0,y) & := & y+1\\
A(x+1,0) &:=& A(x,1)\\
A(x+1,y+1) &:=& A(x,A(x+1,y))
\end{array}
\end{equation}

Formally, we may see $A$ as being defined by induction on a lexicographical product order on $\Nat\times \Nat$.
This function may duly be computed by a term of $\T$ by appealing to primitive recursion at type level $1$.
We first define a functional $\mathrm I$ by primitive recursion (at type $\nat$) satisfying:

\begin{equation}
\label{eqn:iterator-eqns}
\begin{array}{rcl}
\mathrm I\, f \, 0 & = & f\, \numeral 1 \\
\mathrm I\, f \, \succ y & = & f\, (\mathrm I\, f\, y)
\end{array}
\end{equation}

Formally, $\mathrm I$ may be typed by the following derivation,

\[
\vlderivation{
\vliin{\rec_\nat}{}{\nat \to \nat , \underline{{\nat}} \seqar \nat}{
\vliin{\leftimp}{}{\underline{\nat \to \nat} \seqar \nat}{
\vltr{1}{\seqar \nat}{\vlhy{\ }}{\vlhy{}}{\vlhy{\ }}
\vlin{\id}{}{\nat \seqar \nat}{\vlhy{}}
\vliin{\leftimp}{}{\underline{\nat \to \nat}, \red{\nat} \seqar \nat}{
\vlin{\id}{}{\red{\nat} \seqar \nat}{\vlhy{}}
\vlin{\wk}{}{\nat, \underline{\red{\nat}} \seqar \nat}{
\vlin{\id}{}{\nat \seqar \nat}{\vlhy{}}
\]

where principal types are underlined and red occurrences of $\red \nat$ correspond to the same input (morally $y$ in (<ref>)).
$\T$ proves the defining equations from (<ref>) for $\mathrm I$:

\[
\begin{array}{rcll}
\mathrm I\, f\, 0 & = & \leftimp \, \numeral 1\, \id\, f & \text{by $\rec$ axioms}\\
& = & \id\, (f\, \numeral 1) & \text{by $\leftimp$ axiom} \\
&= & f\, \numeral 1 & \text{by $\id$ axiom}
\\
\noalign{\medskip}
\mathrm I\, f\, \succ y & = & \leftimp\, \id\, (\wk\, \id) \, f \, (\mathrm I\, f\, y) & \text{by $\rec$ axioms}\\
& = & \wk\, \id\, (f\, (\id\, (\mathrm I\, f\, y)))\, (\mathrm I \, f\, y) & \text{by $\leftimp$ axiom}\\
&=& \id\, (f\, (\id\, (\mathrm I\, f\, y))) & \text{by $\wk$ axiom}\\
& = & f\, (\id\, (\mathrm I\, f\, y)) & \text{by $\id$ axiom}\\
& = & f\, (\mathrm I\, f\, y) &\text{by $\id$ axiom}
\end{array}
\]

From here $\mathrm A $ is obtained by primitive recursion at type $\nat \to \nat$, satisfying:

\begin{equation}
\label{eqn:ackermann-abstracted-eqns}
\begin{array}{rcl}
\mathrm A\, 0 & = & \succ \\
\mathrm A\, \succ x & =& \mathrm I\, (\mathrm A\, x)
\end{array}
\end{equation}

Formally, such $\mathrm A$ may be typed by the following derivation,

\[
\vlderivation{
\vliin{\rec_{\nat \to \nat}}{}{\underline{\nat} \seqar \nat \to \nat}{
\vlin{\rightimp}{}{\seqar \underline{\nat \to \nat}}{
\vlin{\succ}{}{\nat \seqar \nat}{\vlhy{}}
\vlin{\wk}{}{\underline{\nat}, \nat \to \nat \seqar \nat \to \nat}{
\vlin{\rightimp}{}{\nat \to \nat \seqar \underline{\nat \to \nat}}{
\vltr{\mathrm I}{\nat \to \nat, \nat \seqar \nat}{\vlhy{\ }}{\vlhy{}}{\vlhy{\ }}
\]

where principal types are underlined.

$\nT 1$ proves the following equations:

\[
\begin{array}{rcl}
\mathrm A\, 0\, y & = & \succ y \\
\mathrm A\, \succ x \, 0 & = & \mathrm A\, x\, \numeral 1 \\
\mathrm A\, \succ x\, \succ y & = &  \mathrm A\, x\, (\mathrm A\, \succ x \, y)
\end{array}
\]

We have,

\[
\begin{array}{rcll}
\mathrm A\, 0 \, y & = & \rightimp \, \succ \, y & \text{by $\rec $ axioms}\\
& = & \succ y \, & \text{by $\rightimp$ axiom}
\\
\noalign{\medskip}
\mathrm A\, \succ x \, y & = & \wk\, (\rightimp \, \mathrm I)\, x\, (\mathrm A\, x)\, y & \text{by $\rec$ axioms} \\
& = & \rightimp \, \mathrm I\, (\mathrm A\, x)\, y & \text{by $\wk$ axiom} \\
& =& \mathrm I\, (\mathrm A\, x)\, y & \text{by $\rightimp$ axiom} \quad (*)
\end{array}
\]

whence we have immediately $\mathrm A\, \succ x\, 0 \ = \ \mathrm A\, x\, \numeral 1$ by (<ref>).
For $y$ non-zero, we have:

\[
\begin{array}{rcll}
\mathrm A\, \succ x\, \succ y & = & \mathrm I\, (\mathrm A\, x)\, \succ y & \text{by $(*)$ above} \\
& = & \mathrm A\, x\, (\mathrm I\, (\mathrm A\, x)\, y) & \text{by \eqref{eqn:iterator-eqns}}\\
& = & \mathrm A\, x\, (\mathrm A\, \succ x\, y) & \text{by $(*)$ above} \qedhere
\end{array}
\]

The recursors used to type $\mathrm A$ have level $1$.
This is not a coincidence, since primitive recursion at level $0$ (i.e. on only natural numbers) computes just the primitive recursive functions:

If $t:\nat^k \to \nat$ is a term of $\nT 0$ then $t^\nmod : \Nat^k \to \Nat$ is primitive recursive.

Note that, together with Proposition <ref>, this constitutes a proof that $\ISn 1 $ (or $\RCA$) well-defines just the primitive recursive functions.

§ A CIRCULAR VERSION OF $\T$

We will now move on to the main subject of study in this work: typing `derivations' that are non-wellfounded and their corresponding notion of term.
Let us henceforth write $\T^-$ for the restriction of $\T$ to the language without recursion combinators $\rec_\tau$.

We introduce a new typing rule $\cond$ for derivations, as well as corresponding axioms, in Figure <ref>.

As before, the colouring of type occurrences above will become apparent soon.

\[
\vliinf{\cond}{}{ \purple{\vec \sigma  }, \blue{\nat }\seqar \tau}{\purple{\vec \sigma }\seqar \tau}{ \purple{\vec \sigma  }, \blue{\nat }\seqar \tau}
\qquad\qquad
\begin{array}{rcl}
\cond\ s\ t\ \vec x \  0 & = &  s \ \vec x \\
\cond \ s\ t\ \vec x \ \succ y  & = & t \ \vec x \  y
\end{array}
\]

Typing rule and axioms for $\cond$ combinators.

Again, the interpretation of $\cond$ in the standard model $\nmod$ is uniquely determined by the defining axioms of Figure <ref>.

Throughout this section, we will work in the language of $\T^- + \cond$, unless otherwise specified.

§.§ Non-wellfounded `terms' and `derivations'

Coterms are generated coinductively from constants and variables under typed application.
Formally, we may construe a coterm as a possibly infinite binary tree (of height $\leq \omega$) where each leaf (if any) is labelled by a typed variable or constant and each interior node is labelled by a typed application operation, having type consistent with the types of its children. I.e., an interior node with children of types $\sigma$ and $\sigma \to \tau$, respectively, must have type $\tau$.

At the risk of confusion, we expand the range of the metavariables $s,t,$ etc. to include coterms as well as terms, clarifying further only in the case of ambiguity.
We adopt the same writing and bracketing conventions as for terms, where it is meaningful, e.g. writing $r\, s\, t$ for $(r \comp s)\comp t$.

We will not dwell much on arbitrary coterms, since we will only deal with those induced by our sequent style type system.

A coderivation is some possibly non-wellfounded `derivation' built from the typing rules of $\T^- + \cond$, in a locally correct manner.
Formally, a coderivation is a possibly infinite labelled binary tree (of height $\leq \omega$) whose nodes are labelled by rule instances s.t. the premisses of a node (if any) match the conclusions of the node's respective children (if any).

We construe coderivations as coterms in the same way as we construed derivations as terms.
Namely, we coinductively set:

* $\vlderivation{
\vlin{\mathsf r}{}{\vec \tau \seqar \tau}{
\vltr{s}{\vec \sigma \seqar \sigma}{\vlhy{ \ }}{\vlhy{}}{\vlhy{\ }}
}$ is the coterm $\mathsf r\, s$; and,

* $\vlderivation{
\vliin{\mathsf r}{}{\vec \tau \seqar \tau}{
\vltr{r}{\vec \rho \seqar \rho}{\vlhy{\ }}{\vlhy{ }}{\vlhy{\ }}
\vltr{s}{\vec \sigma \seqar \sigma}{\vlhy{\ }}{\vlhy{ }}{\vlhy{\ }}
}$ is the coterm $\mathsf r\ r\, s$.

Note that this association is continuous at the level of the underlying trees, so it is indeed well-defined.

Again overloading notation, we will write $t:\vec \sigma \seqar \tau$ if $t$ is a coderivation of the sequent $\vec \sigma \seqar \tau$, and $t:\sigma$ if $t$ is a coterm of type $\tau$.
If we need to distinguish $t$ as a term then we will say so explicitly.

Note that the equational theory induced by Figures <ref>, <ref> and <ref> form a Kleene-Herbrand-Gödel
style equational specification for coterms (cf., e.g., [35]), now understanding the metavariables $s,t$ etc. there to range over coterms.
We may thus view coterms as partial recursive functionals in the standard model $\nmod$ of the appropriate type.  More formally:

We define a type structure $\nmod_\bot$ by interpretations $\cdot^\nmod_\bot$ and corresponding `totally undefined functionals' $\bot_\sigma$ as follows:

* $\bot_\nat$ is just some fresh element $\bot$.

* $\nat^\nmod_\bot$ is $\Nat \cup \{\bot \}$.

* $\bot_{\sigma \to \tau} : \sigma^\nmod_\bot \to \tau^\nmod_\bot$ by $a\mapsto \bot_\tau$, for any $a \in \sigma^\nmod_\bot$.

* $(\sigma \to \tau)^\nmod_\bot$ is the set of functions $f:\sigma^\nmod_\bot \to \tau^\nmod_\bot$ s.t. $f(\bot_\sigma) = \bot_\tau$.

* $=^\nmod_\bot$ is just extensional equality (for each type).

A partial functional of type $\sigma$ is just a function in $\sigma^\nmod_\bot$.
A (total) functional of type $\sigma$ is just a partial functional $f$ of type $\sigma$ with $f(x) = \bot $ if and only if $x = \bot$.

We now define the interpretation of coterms in $\nmod_\bot$ as follows:

* If $t: \nat$ then $t^\nmod_\bot = n \in \Nat$ just if $n$ is the unique interpretation of $t$ (under the equations of Figures <ref> and <ref>) in $\nmod_\bot$. Otherwise $t^\nmod_\bot$ is $\bot$.

* If $t : \sigma \to \tau$ and $a \in \sigma^\nmod_\bot$ then $t^\nmod_\bot (a) := (t\, a)^\nmod_\bot$.[Here we are implicitly using parameters from the model.]

Note that total functionals of type $\sigma$ are just elements of $\sigma^\nmod$, when restricted to non-$\bot$ arguments.
Moreover, for any (finite) term $t$ we have immediately that $t^\nmod_\bot = t^\nmod$, when restricted to non-$\bot$ arguments.
In light of this, we shall henceforth unambiguously write $t^\nmod$ rather than $t^\nmod_\bot$, and simply write $\nmod$ instead of $\nmod_\bot$.

We shall omit here the finer details of this interpretation of coterms as partial functionals, since we will give a more formal (and, indeed, formalised) treatment of `regular' coterms and their computational interpretations in Section <ref>.
We point the reader to the excellent book [48] for further details on models of (partial) (recursive) function(al)s.

Let us now consider some relevant examples of coderivations and coterms, at the same time establishing some foundational results. As before, the reader may safely ignore the colouring of type occurrences in what follows.
That will become meaningful later in the section.

[Extensional completeness at type 1]

For any $f : \Nat^k \to \Nat$, there is a coderivation $t:\nat^k \seqar \nat$ s.t. $t^\nmod = f$.

To demonstrate this, we proceed by induction on $k$.[While we may assume $k=1$ WLoG by the availability of sequence (de)coding, the current argument is both more direct and avoids the use of cuts (on non-numerals).]
If $k=0$ then the numerals clearly suffice.
Otherwise, suppose $f: \Nat \times \Nat^k \to \Nat$ and write $f_n$ for the projection $\Nat^k \to \Nat$ by $f_n (\vec x) = f(n,\vec x)$.

We define the coderivation for $f$ as follows:

\begin{equation}
\label{eqn:ext-comp}
\vlderivation{
\vliin{\cond}{}{\red{\nat}, \vec \nat \seqar \nat}{
\vltr{f_0}{\vec \nat \seqar \nat}{\vlhy{\quad }}{\vlhy{}}{\vlhy{\quad }}
\vliin{\cond}{}{\red{\nat}, \vec \nat \seqar \nat}{
\vltr{f_1}{\vec \nat \seqar \nat}{\vlhy{\quad}}{\vlhy{}}{\vlhy{\quad}}
\vliin{\cond}{}{\red{\nat}, \vec \nat \seqar \nat}{
\vltr{f_2}{\vec \nat \seqar \nat}{\vlhy{\quad}}{\vlhy{}}{\vlhy{\quad}}
\vlin{\cond}{}{\red{\nat}, \vec \nat \seqar \nat}{\vlhy{\vdots}}
\end{equation}

where the derivations for each $f_n$ are obtained by the inductive hypothesis.
It is not difficult to see that the interpretation of this coderivation in the standard model indeed coincides with $f$.

Notice that, while we have extensional completeness at type 1, we cannot possibly have such a result for higher types by a cardinality argument: there are only continuum many coderivations.

[Naïve simulation of primitive recursion]

Terms of $\T$ may be interpreted as coterms in a straightforward manner.
The only difficulty is the simulation of the $\rec$ combinators, which may be interpreted by coderivations as follows:

\begin{equation}
\label{eqn:sim-rec-naively-in-ct}
\vlderivation{
\vliin{\rec}{}{\vec \sigma, \nat \seqar \sigma}{
\vlhy{\vec \sigma \seqar \sigma}
\vlhy{\vec \sigma, \nat, \sigma \seqar \sigma}
\quad \leadsto \quad
\vlderivation{
\vliin{\cond}{\bullet}{\vec \sigma, \blue{\nat} \seqar \sigma}{
\vlhy{\vec \sigma \seqar \sigma}
\vliin{\cut}{}{\vec \sigma , \blue{\nat} \seqar \sigma}{
\vlin{\cond}{\bullet}{\vec \sigma , \blue{\nat} \seqar \sigma}{\vlhy{\vdots}}
\vlhy{\vec \sigma, \nat , \sigma \seqar \sigma}
\end{equation}

where the occurrences of $\bullet $ indicate roots of identical derivations.

Denoting the RHS of (<ref>) above as $\rec'$, we can check that the two sides of (<ref>) are indeed equivalent.
Formally, we show $\rec\, s\, t\, \vec x\, y \ = \ \rec \, s\, t\, \vec x\, y$ by induction on $y$:

\[
\begin{array}{rcll}
\rec' s\, t\, \vec x\, 0 & = & \cond\, s\, (\cut\, (\rec' s\, t) \, t) \,   \vec x\, 0 & \text{by definition of $\rec'$ above} \\
& = & s\, \vec x & \text{by $\cond$ axioms} \\
& = & \rec\, s\, t\, \vec x\, 0 & \text{by $\rec$ axioms}
\\ \noalign{\medskip}
\rec'  s\, t\, \vec x\, \succ y &=& \cond\, s\, (\cut\, (\rec' s\, t) \, t)\, \vec x\, \succ y & \text{by definition of $\rec'$ above}\\
& = & \cut\, (\rec' s\, t) \, t\, \vec x\, y  & \text{by $\cond$ axioms} \\
& = & t\, \vec x\, y\, (\rec'\, s\, t\, \vec x\, y ) & \text{by $\cut$ axiom} \\
& = & t\, \vec x\, y\, (\rec\, s\, t\, \vec x\, y) & \text{by inductive hypothesis}\\
& = & \rec\, s\, t\, \vec x\, \succ y & \text{by $\rec$ axioms}
\end{array}
\]

Note that our reasoning here was completely syntactic, indeed only using axioms and rules from Figures <ref>, <ref> and <ref>, (understanding metavariables $s,t$ etc. in those figures to now range over coterms as well as terms).
This is no coincidence, and the argument above will actually turn out to be a formal proof in our theory defined later, thus inducing equivalence of $\rec$ and $\rec'$ in all models.

§.§ Regularity

Until now, our coderivations and coterms were potentially non-uniform in structure and, as exemplified in Example <ref>, comprise a computational model of extreme expressivity.
Naturally, within formal theories, we would prefer to manipulate only finitely presentable objects. To this end we will study a natural fragment in non-wellfounded proof theory:

A coderivation $t$ is regular (or circular) if it has only finitely many distinct sub-coderivations.
A regular coterm is similarly just one with finitely many distinct sub-coterms.

Note that a regular coderivation or coterm is indeed finitely presentable, e.g. as a finite directed graph, possibly with cycles, or a finite binary tree with `backpointers'.
When dealing with recursion-theoretic matters, we will implicitly assume such a finitary representation.
Further details on such a formalised representation are given in Section <ref>.

Once again we have that regular coderivations are regular coterms, and conversely that closed regular coterms may be interpreted as regular coderivations (under $\cut$-as-composition).

One example we have already seen of a regular coderivation is the RHS of (<ref>).
In fact, it turns out that the regular coterms constitute a sufficiently expressive programming language:

The set of regular coderivations of type level 1 is Turing-complete,[For a model of program execution, we may simply take the aforementioned Kleene-Herbrand-Gödel model with equational derivability, cf. [35]. Note that this coincides with derivability by the axioms thus far presented.]
i.e. $\{t^\nmod\  |\  \text{$t: \nat^k \seqar \nat$ regular}\}$ includes all partial recursive functions on $\Nat$.

We have already seen in Example <ref> that we can encode the primitive recursive functions, so it remains to simulate minimisation, i.e. the operation $\mu x (fx=0)$, for a given function $f$.
For this, we observe that $\mu x (fx =0)$ is equivalent to $H\, 0$ where

\begin{equation}
\label{eqn:blind-search-equation}
H\, x \  =\  \cond \ (f\, x)\ x\ (H\, \succ x)
\end{equation}

Note that $H$ may be interpreted by the following coderivation:

\begin{equation}
\label{eqn:blind-search-derivation}
\vlderivation{
\vliin{\cut}{\bullet}{\blue\nat \seqar \nat}{
\vltr{f}{\blue\nat \seqar \red \nat}{\vlhy{}}{\vlhy{\quad}}{\vlhy{}}
\vliin{\cond}{}{\underline{\red\nat}, \blue \nat \seqar \nat}{
\vlin{\id}{}{\blue \nat\seqar \nat}{\vlhy{}}
\vlin{\wk}{}{\underline{\red\nat} , \blue\nat \seqar \nat}{
\vliin{\cut}{}{\blue \nat \seqar \nat}{
\vlin{\succ}{}{\blue \nat \seqar \purple \nat}{\vlhy{}}
\vlin{\cut}{\bullet}{\purple \nat \seqar \nat}{\vlhy{\vdots}}
\end{equation}

It is intuitive here to think of the blue $\blue \nat$ standing for $x$, the red $\red\nat$ standing for $f(x)$, and the purple $\purple \nat$ standing for $\succ x$.

Working in the standard model $\nmod$,  may show that $H$ indeed satisfies (<ref>) as follows.
We have that:

\[
\begin{array}{rcll}
H\, x & = & \cut \, f\, (\cond\, \id\, (\wk\, (\cut\, \succ \, H)))\, x & \text{by definition of $H$}\\
& = & \cond\, \id\, (\wk\, (\cut\, \succ \, H))\, (f\, x)\, x & \text{by $\cut$ axiom}\\
\end{array}
\]

Now, we conduct a case analysis on the value of $f(x)$:

* If $f(x) = 0$, then we have $H\, x \ = \ \id\, x\ =\ x$, by the $\cond$ and $\id$ axioms, thus satisfying (<ref>).

* If $f(x) = \succ y$, for some $y$, then,

\[
\begin{array}{rcll}
H\, x & = & \wk\, (\cut\, \succ\, H)\, y\, x & \text{by $\cond$ axioms}\\
& = & \cut\, \succ\, H\, x  &\text{by $\wk$ axiom}\\
& = & H\, \succ x & \text{by $\cut $ axiom}
\end{array}
\]

again satisfying (<ref>).

Note, again, that the reasoning above was entirely syntactic, using only axioms thus far presented in Figures <ref>, <ref>,  <ref> and <ref>.
While the coderivation in (<ref>) will not formally be a symbol of our eventual theory $\C$,
the reasoning above hints at well-behaved extensions accommodating partially defined coterms.

Note that the argument above required coderivations including only occurrences of $\nat$.
This means that the set of type 0 regular coderivations are already a Turing-complete programming language, under derivability via Figures <ref>, <ref>,  <ref> and <ref>.

§.§ The progressing criterion

Despite regular coderivations being finitely presentable, they do not necessarily denote totally defined functionals in the standard model $\nmod$, cf. Proposition <ref>, contrary to the norm for terms in formal theories.
In this work we will consider coderivations satisfying a standard `termination criterion' in non-wellfounded proof theory.
First, let us recall some standard structural proof theoretic concepts about (co)derivations.

Let $t $ be a (co)derivation. A type occurrence $\sigma^1$ is an immediate ancestor[This terminology is standard in proof theory, e.g. as in [14].] of a type occurrence $\sigma^2$ in $t$ if $\sigma^1$ and $\sigma^2$ appear in the LHSs of a premiss and conclusion, respectively, of a rule instance and have the same colour in the corresponding rule typeset in Figure <ref>, <ref> or <ref>. If $\sigma^1$ and $\sigma^2$ are elements of an indicated list, say $\vec \sigma$, we also require that they are at the same position of the list in the premiss and the conclusion.
Note that, if $\sigma^1$ is an immediate ancestor of $\sigma^2$, they are necessarily occurrences of the same type.

The notion of immediate ancestor thus defined, being a binary relation, induces a directed graph whose paths will form the basis of our termination criterion.

A thread is a maximal path in the graph of immediate ancestry.
A $\sigma$-thread is a thread whose elements are occurrences of the type $\sigma$.
We say that a $\nat$-thread progresses when it is principal for a $\cond$ step (i.e. it is the indicated blue $\blue \nat$ in the $\cond$ rule typeset in Figure <ref>).

A (infinitely) progressing thread is a $\nat$-thread that progresses infinitely often (i.e. it is infinitely often the indicated blue $\blue \nat$ in the $\cond$ rule typeset in Figure <ref>.)

A coderivation is progressing if every infinite branch has a progressing thread.

Note that progressing threads do not necessarily begin at the root of a coderivation, they may begin arbitrarily far into a branch.
In this way, the progressing coderivations are closed under all typing rules.
Note also that arbitrary coderivations may be progressing, not only the regular ones.

[Extensional completeness at type $1$, revisited]

Recalling Example <ref>, note that the infinite branch marked $\cdots$ in (<ref>) has a progressing thread along the red $\red \nat$s.
Other infinite branches, say through $f_0,f_1, $ etc., will have progressing threads along their infinite branches by an appropriate inductive hypothesis, though these may progress for the first time arbitraryily far from the root of (<ref>).

As previously mentioned, we shall focus our attention in this work on the regular coderivations.
Let us take a moment to appreciate some previous (non-)examples of regular coderivations with respect to the progressing criterion.

[Primitive recursion, revisited]

Recalling Example <ref>, notice that the RHS of (<ref>) is a progressing coderivation: there is precisely one infinite branch (that loops on $\bullet$) and it has a progressing thread on the blue $\blue \nat$ indicated there.

[Turing completeness, revisited]

Recalling the proof of Proposition <ref>, notice that the coderivation given for $H$ in (<ref>) is not progressing: the only infinite branch loops on $\bullet$ and immediate ancestry, as indicated by the colouring, admits no thread along the $\bullet$-loop.
This is no coincidence, as it turns out that the progressing criterion suffices for coderivations to denote total functionals in the standard model $\nmod$, as we will show in the next subsection.

One of the most appealing features of the progressing criterion is that, while being rather expressive and admitting many natural programs, e.g. as we will see in Section <ref>, it remains effective (for regular coderivations) thanks to well known arguments in automaton theory:

It is decidable whether a regular coderivation is progressing.

This well-known result (see, e.g., [22] for an exposition for a similar circular system) follows from the fact that the progressing criterion is equivalent to the universality of a Büchi automaton of size determined by the (finite) representation of the input coderivation.
This problem is decidable in polynomial space, though the correctness of this algorithm requires nontrivial infinitary combinatorics, as formally demonstrated in [37].
Nonetheless, a non-uniform version of this problem is formalisable in the weakest of the big-five theories of reverse mathematics:

For any regular progressing coderivation $t$, $\RCA$ proves that $t$ is progressing.

As noted in that work, the above result cannot be strengthened to a uniform one unless $\RCA$ (and so PRA) is inconsistent, by a reduction to Gödel-incompletness.

§.§ Progressing coterms denote total functionals

As outlined in Definition <ref>, coderivations denote partial functionals in the standard model $\nmod$.
In fact, the partial functionals induced by progressing coderivations are indeed totally defined, by adapting well-known infinite descent arguments in non-wellfounded proof theory:

If $t:\vec \sigma \seqar \tau$ is a progressing coderivation, then $t^\nmod$ is a well-defined total functional in $(\vec \sigma\to \tau)^\nmod$.

The idea behind this result is to, by contradiction, assume a non-terminating `run' of a progressing coderivation, and thence extract an infintely decreasing sequence of natural numbers from a progressing thread, contradicting the well-ordering property.
We stop short of giving an explicit `operational semantics' here, being beyond the scope of this work. Rather, let us simply note that the totally defined functionals are closed under composition by typing rules (since typing rules are constants interpreted as totally defined functionals themselves). Contrapositively this means that if a coderivation is interpreted by a non-total functional, then so is one of its immediate sub-coderivations.

[Proof of Proposition <ref>]
Suppose otherwise and let $\vec a \in \vec \sigma^\nmod$ be inputs on which $t^\nmod$ is not well-defined, i.e. $t^\nmod(\vec a) = \bot$.
We may thus inductively construct an infinite branch $(t_i:\vec \sigma_i \seqar \tau_i)_{i \in \omega}$ and associated inputs $(\vec a_i \in \vec \sigma_i^\nmod)$ s.t. $t_i^\nmod (\vec a_i) = \bot$ as follows:

* $t_0 = t$ and $\vec a_0 = \vec a$.

* If $t_i$ concludes with a $\wk$, $\exch$ or $\cntr$ step then $t_{i+1}$ is the only immediate sub-coderivation and $\vec a_{i+1}$ is just $\vec a_i$ with the appropriate deletion, switch or duplication of arguments.

* ($t_i$ cannot conclude with a nullary step $\id$, $0$ or $\succ$, by assumption that $t_i$ is non-total.)

* If $t_i$ concludes with a $\cut $ step, as typeset in Figure <ref>, then $t_{i+1}$ is the left sub-coderivation if it is not totally defined on inputs $\vec a_i$; otherwise $t_{i+1}$ is the right sub-coderivation and $\vec a_{i+1} = (\vec a, a)$, for some $a\in \sigma^\nmod$ s.t. $t_{i+1}^\nmod (\vec a_i,a) = \bot$.

* If $t_i$ concludes with a $\leftimp $ step, as typeset in Figure <ref>, then $t_{i+1}$ is the left sub-coderivation if it is not totally defined on inputs $\vec a_i$; otherwise $t_{i+1}$ is the right sub-coderivation and $\vec a_{i+1} = (\vec a_i, a)$, for some $a \in \sigma^\nmod$ s.t. $t_{i+1}^\nmod (\vec a_i,a) = \bot$.

* If $t_i$ concludes with a $\rightimp $ step, as typeset in Figure <ref>, then $t_{i+1}$ is the only immediate sub-coderivation and $\vec a_{i+1} = (\vec a_i , a)$, for some $a \in \sigma^\nmod$ s.t. $t_{i+1}^\nmod (\vec a_i, a) = \bot$.

* If $t_i$ concludes with a $\cond$ step and $\vec a_i = (\vec a_i', n)$, then $t_{i+1}$ is the left sub-coderivation if $n=0$ and $\vec a_{i+1} = \vec a_i'$; otherwise, if $n=m+1$, $t_{i+1}$ is the right sub-coderivation and $\vec a_{i+1} = (\vec a_i', m)$.

Now, notice that, since $t$ is progressing, we must have some progressing thread $(\nat^i)_{i\geq k}$ along some tail $(t_i)_{i\geq k}$.
Writing $n_i$ for the input in $\vec a_i$ corresponding to $N^i$, notice that $(n_i)_{i\geq k}$ is a non-increasing sequence of natural numbers, by construction of $t_i$ and $\vec a_i$.
Moreover, we have that $n_{i+1}<n_i$ whenever $\nat^i$ is principal for a $\cond$ step, so for infinitely many $i\geq k$ by definition of a progressing thread.
Thus $(n_i)_{i\geq k}$ has no least element, contradicting the well-ordering property.

§.§ The simply typed theory $\C$ and its fragments

We are finally ready to give the definition of our circular version of System $\T$.

The language of
$\C$ extends contains every regular progressing coderivation of $\T^- + \cond$ as a symbol.

We identify `terms' of this language with coterms in the obvious way, and call them (regular) progressing coterms.
$\C$ itself is a STT axiomatised by
the schemata from
Figures <ref>, <ref> and <ref>, now interpreting the metavariables $s,t$ etc. there as ranging over coterms.

The aim of this work is to compare fragments of $\C$ and fragments of $\T$ delineated by type level.
In light of Proposition <ref>, the following definition gives natural circular counterparts of the fragments $\nT n$ of $\T$:

$\nC n$ is the fragment of $\C$ restricted to the language containing only coderivations where all types occurring have level $\leq n$.
$\nC n$ still has constant symbols for each individual constant of $\T^- + \cond$.

Notice that, despite the fact that coderivations of $\nC n$ may type only level $n+1$ functionals, progressing coterms are closed under application and so, by definition of a STT, $\nC n$ admits `terms' of arbitrary type by composing with the constants and variables of $\T^- + \cond$.
In particular we still have combinatory completeness, as usual.
In what follows, however, it will usually suffice to only consider the coderivations when proving properties of $\nC n$, the generalisation to progressing coterms following by closure under application.

§.§ Example: Ackermann-Péter, revisited

Let us revisit the example of the Ackermann-Péter function from Section <ref>.
Despite the fact that type level 1 recursion is required to type it in $\T$ (cf. Fact <ref>), $A$ may be circularly typed in $\C$ by a coderivation $\mathrm A$ using only the base type $\nat$:[For convenience we have implemented some branching rules as context-splitting, namely the $\cut$ steps. Formally, there are implicit $\wk$ steps that are not indicated, a convention that we will henceforth adopt for the sake of easing legibility.]

\begin{equation}
\label{eqn:ack-cyc-der}
\vlderivation{
\vlin{\cntr}{\bullet}{\underline{\purple \nat}, \nat \seqar \nat}{
\vliin{\cond}{}{\underline{\red \nat} , \blue \nat , \orange \nat \seqar \nat}{
\vlin{\wk}{}{\underline \nat , \nat \seqar \nat}{
\vlin{\succ}{}{\nat \seqar \nat}{\vlhy{}}
\vliin{\cond}{}{\red \nat, \blue \nat , \underline{ \orange{\nat}} \seqar \nat}{
\vlin{\wk}{}{\red{\nat}, \underline \nat \seqar \nat}{
\vliin{\cut}{}{\red \nat \seqar \nat}{
\vliq{1}{}{\seqar \nat}{\vlhy{}}
\vlin{}{\bullet}{\red{\nat}, \nat \seqar \nat}{\vlhy{\vdots (1)}}
\vliin{\cut}{}{\red \nat, \blue \nat , \orange \nat \seqar \nat}{
\vlin{}{\bullet}{\blue \nat,  \orange \nat \seqar \nat}{\vlhy{\vdots (2)}}
\vlin{}{\bullet}{\red \nat, \nat \seqar \nat}{\vlhy{\vdots (3)}}
\end{equation}

As usual, the occurrences of $\bullet$ above indicate roots of identical coderivations, and we have indicated three distinct threads, coloured red, blue and orange. Note that the purple $\purple \nat$ prefixes both the red and the blue thread.
Finally note that the red $\red \nat$ thread progresses on every visit to (1) and (3), while the orange $\orange \nat$ thread progresses on every visit to (2).

$\mathrm A$ is progressing and regular, and so is a symbol of $\nC 0$.

To show that $\mathrm A$ is progressing, we conduct a case analysis on an infinite branch $B$, based on which of the simple loops $(1),(2)$ and $(3)$ are traversed infinitely often:

* $B$ hits only $(1)$ infinitely often. Then there is a progressing thread along the red $\red \nat$.

* $B$ hits only $(2)$ infinitely often. Then eventually there is a progressing thread along the orange $\orange \nat$.

* $B$ hits only $(3)$ infinitely often. Then eventually there is a progressing thread along the red $\red \nat$.

* $B$ hits only (1) and (2) infinitely often. Then eventually there is a progressing thread along the red $\red \nat$ on iterations of (1) (on which it progresses) and along the blue $\blue \nat$ on iterations of (2) (on which it is constant).

* $B$ hits only (1) and (3) infinitely often. Then eventually there is a progressing thread along the red $\red \nat$, which progresses on any iteration of (1) or (3).

* $B$ hits only (2) and (3) infinitely often. Then eventually there is a progressing thread along the blue $\blue \nat$ on iterations of (2) (on which it is constant) and along the red $\red \nat$ on iterations of (3) (on which it progresses).

* $B$ hits all of (1), (2) and (3) infinitely often. Then there is a progressing thread along the red $\red \nat$ on iterations of (1) and (3) (on which it progresses) and the blue $\blue \nat $ on iterations of (2) (on which it is constant).

Clearly $\mathrm A$ is regular and contains only occurrences of $\nat$, so $\mathrm A$ is indeed a symbol of $\nC 0$.

In fact, we may also show that $\nC 0 $ proves the defining equations of $A$ from (<ref>):

$\nC 0 $ proves the following equations:

\[
\begin{array}{rcl}
\mathrm A\, 0\, y & = & \succ y \\
\mathrm A\, \succ x \, 0 & = & \mathrm A\, x\, \numeral 1 \\
\mathrm A\, \succ x\, \succ y & = &  \mathrm A\, x\, (\mathrm A\, \succ x \, y)
\end{array}
\]

Writing $\mathrm A_0$ and $\mathrm A_1$ for the left and right coderivations, respectively, composed by the lowermost $\cond$ step in (<ref>), we have:

\begin{equation}
\label{eqn:ackxy-to-cond}
\begin{array}{rcll}
\mathrm A \, x\, y & = & \cntr\, (\cond\, \mathrm A_0 \, \mathrm A_1)\, x \, y & \text{by definition of $\mathrm A$}\\
& = & \cond\, \mathrm A_0\, \mathrm A_1\, x\, x\, y & \text{by $\cond$ axioms}
\end{array}
\end{equation}

From here we obtain the first equation of (<ref>), in $\nC 0$:

\[
\begin{array}{rcll}
\mathrm A\, 0 \, y & = & \mathrm A_0 \, x\, y & \text{by \eqref{eqn:ackxy-to-cond} above and $\cond$ axioms}\\
& = & \wk \, \succ\, x\, y & \text{by definition of $\mathrm A_0$}\\
& = & \succ y & \text{by $\wk$ axiom}
\end{array}
\]

Now writing $\mathrm A_{10}$ and $\mathrm A_{11}$ for the left and right coderivations, respectively, composed by the uppermost $\cond$ step typeset in (<ref>), we have:

\begin{equation}
\label{eqn:acksxy-to-cond}
\begin{array}{rcll}
\mathrm A\, \succ x\, y & = & \mathrm A_1 \, x\, \succ x\, y & \text{by \eqref{eqn:ackxy-to-cond} above and $\cond$ axioms}\\
& = & \cond\, \mathrm A_{10} \, \mathrm A_{11}\, x\, \succ x\, y & \text{by definition of $\mathrm A_1$}
\end{array}
\end{equation}

From here we obtain the second and third equations of (<ref>), in $\nC 0$:

\[
\begin{array}{rcll}
\mathrm A\, \succ x\, 0 & = & \mathrm A_{10}\, x\, \succ x & \text{by \eqref{eqn:acksxy-to-cond} above and $\cond$ axioms}\\
& = & \wk\, (\cut\, (1\, \mathrm A))\, x\, \succ x & \text{by definition of $\mathrm A_{10}$}\\
& = & \cut\, (1\, \mathrm A)\, x & \text{by $\wk$ axiom}\\
& = & \mathrm A\, x\, \numeral 1 & \text{by $\cut$ axiom}\\
\noalign{\medskip}
\mathrm A\, \succ x\, \succ y & = & \mathrm A_{11}\, x\, \succ x\, y & \text{by \eqref{eqn:acksxy-to-cond} above and $\cond$ axioms}\\
& = & \cut\, (\mathrm A\, \mathrm A)\, x\, \succ x\, y & \text{by definition of $\mathrm A_{11}$}\\
& = & \mathrm A\, x\, (\mathrm A\, \succ x\, y) & \text{by $\cut $ axiom} \qedhere
\end{array}
\]

Now, let us revisit Section <ref>, where we gave a $\T$ term for the Ackermann-Péter function based on type 1 recursion.
Calling that term $\mathrm A'$, temporarily, we now have that $\mathrm A'$ and $\mathrm A$ satisfy the same defining equations from (<ref>).
Working in a combined theory, we may thus deduce their equivalence via a nested induction.

$\nC 0 , \rec_1 \proves\,  \mathrm A\, x\, y \, = \, \mathrm A'x\, y$.

Working inside $\nC 0 + \rec_1$, we show $\mathrm A\, x\, = \, \mathrm A' x$ by induction on $x$. We have,

\[
\begin{array}{rcll}
\mathrm A\, 0 \, y & = & \succ y & \text{by Proposition~\ref{prop:ct0-proves-ack-eqns}}\\
& = & \mathrm A' 0\, y & \text{by Proposition~\ref{prop:t1-proves-ack-eqns}}
\end{array}
\]

so $\mathrm A\, 0 = \mathrm A' 0$ by $\extensionality$.
For the inductive step, we show that $\mathrm A\, \succ x\, y = \mathrm A' \succ x\, y$ by a sub-induction on $y$:

\[
\begin{array}{rcll}
\mathrm A\, \succ x\, 0 & = & \mathrm  A\, x\, \numeral 1 & \text{by Proposition~\ref{prop:ct0-proves-ack-eqns}}\\
& = & \mathrm A'x\, \numeral 1 & \text{by main inductive hypothesis}\\
& = & \mathrm A'\succ x\, 0 & \text{by Proposition~\ref{prop:t1-proves-ack-eqns}}\\
\noalign{\medskip}
\mathrm A\, \succ x\, \succ y & = & \mathrm A\, x\, (\mathrm A\, \succ x\, y) & \text{by Proposition~\ref{prop:ct0-proves-ack-eqns}}\\
& = & \mathrm A' x\, (\mathrm A\, \succ x\, y) & \text{by main induction hypothesis}\\
& = & \mathrm A'x\, (\mathrm A' \succ x\, y) & \text{by sub-induction hypothesis}\\
& = & \mathrm A' \succ x\, \succ y & \text{by Proposition~\ref{prop:t1-proves-ack-eqns}}
\end{array}
\]

Thus we have $\mathrm A\, \succ x\, = \, \mathrm A' \succ x$ by $\extensionality$, proving the main inductive step as required.

As we mentioned before, general extensionality is not strictly necessary for many of our results, and this is in particular the case for the result above.
We could have also proceeded under weak extensionality by an instance of $\Pi_1$-induction ($\forall y (\mathrm A\, x\, y \, = \, \mathrm A' x\, y)$). Standard witnessing theorems then reduce this to an instance of quantifier-free induction, but such a development is beyond the scope of this work.

§ $\C$ SIMULATES $\T$, MORE SUCCINCTLY

In this section we give a simulation of $\nT{n+1}$ terms of level $\leq n+1$ into $\nC n$, provably satisfying the same equational theory, thus improving on the naive simulation of primitive recursion from Examples <ref> and <ref>.
This matches similar results from the setting of arithmetic, [19], and the exposition is entirely proof theoretic.

The main goal is to show the following result:

If $t:\sigma$ is a term of $\nT{n+1}$ with $\level(\sigma)\leq n+1$ then there is a $\nC n$ coderivation $t' : \sigma$ s.t.:

\begin{equation}
\label{eqn:prov-eq-t-ct-terms-with-ext}
\nC n, \rec_{n+1} \proves t=t'
\end{equation}

The idea is to rely on the partial normalisation result, Proposition <ref>, to work with a normal form of $\T$ derivations, and then translate into $\C$ coderivations under a constructive realisation of the deduction theorem (for typing derivations).

§.§ Derivations with `oracles'

We consider (co)derivations with fresh intial sequents of the form $\vlinf{f}{}{\sigma_1, \dots, \sigma_n \seqar \tau}{}$, denoting a functional $f$ of type $\sigma_1 \to \cdots \to \sigma_n \to \tau$, as expected.
We write,

\[
\toks0={0.7}
\vlderivation{
\vltrf{t}{\vec \sigma \seqar \tau}{\vlhy{}}{
\vlin{f_i}{i}{\vec \sigma_i \seqar \tau_i}{\vlhy{}}
\]

for a (co)derivation $t$ of $\vec \sigma \seqar \tau$ with initial sequents among $\vlinf{f_i}{i}{\vec \sigma_i \seqar \tau_i}{}$, with $i$ varying over some fixed range.
We distinguish $f_i$ from variable symbols, since coderivations until now are closed coterms; instead it is more pertinent to think of them as some fresh constant `oracle' symbols.
We thus use metavariables $f,g,$ etc. for these new initial sequents.
The interpretation of such (co)derivations into the standard model $\nmod$ is as expected, with (co)derivations now computing (partial) functionals with respect to oracles for each $f_i$.

§.§ Constructive realisation of the deduction theorem

We describe how to `realise' a version of the deduction theorem for typing derivations in order to lower type level.
The key feature of this translation is that recursion is simulated by a cyclic derivation in a succinct way, in terms of abstration complexity.

As notation throughout this section, if $\vec f = f_1, \dots, f_n$ then we may simply write $(\vec f\, \vec x)$ for $(f_1\, \vec x)\, (f_2\, \vec x)\, \dots\, (f_n\, \vec x)$, to lighten the syntax.
Our key intermediate result is the following lemma:

Let $t:\vec \sigma , \vec \nat \seqar \tau$ be  a $\nT{n+1}$ derivation, i.e.,

\[
\vltreeder{t}{\vec \sigma, \vec \nat \seqar \tau}{\ }{\quad }{\ }
\]

with all $\nat$s indicated, s.t. all types occurring in $t$ have level $\leq n+1$.

Write $\tau = \vec \tau \to \nat$ and $\sigma_i = \vec \sigma_i \to \nat$. For each $\vec \rho$ of levels $\leq n$ there is a $\nC n$ coderivation $\rhotrans t {\vec\rho} (\vec f) : \vec \rho, \vec \nat , \vec \tau \seqar \nat$ using initial sequents $\vlinf{f_i}{i}{\vec \rho, \vec \sigma_i \seqar \nat}{}$, i.e.,

\[
\toks0={0.7}
\vlderivation{
\vltrf{ \rhotrans{ t }{\vec \rho}   (\vec f) }{\vec \rho, \vec \nat , \vec \tau \seqar \nat}{\vlhy{}}{
\vlin{f_i}{i}{\vec \rho,\vec \sigma_i \seqar \nat}{\vlhy{}}
\]

such that,

\begin{equation}
\label{eqn:ded-thm-invariant}
\nC n, \rec_{n+1} \proves \rhotrans t {\vec \rho}(\vec f)\, \vec x\, \vec y\, \vec z \  = \ t\, (\vec f\, \vec x)\, \vec y\, \vec z
\end{equation}

Moreover, for any $j$, there is a $\rho_j$-thread from the $\rho_j$ in the conclusion of $\rhotrans t {\vec \rho} (\vec f)$ to the $\rho_j$ in any occurrence of the initial sequent $f_i$.

Before giving the proof let us set up some further notation to lighten the exposition as much as possible.

* We shall sometimes suppress the initial sequent arguments of a coderivation when it is unambiguous, e.g. writing $\rhotrans t {\vec \rho}$ instead of $\rhotrans t{\vec \rho}(\vec f)$ etc. We will only do this when the initial sequents, or approrpriate substituted (co)derivations, are explicitly typeset.

* We shall write $\mathsf r^*$ for the reflexive transitive closure of a rule $\mathsf r$.

* As in the statement of the lemma, we shall typically assume that a type, say, $\tau$ has the form $\vec \tau \to \nat$ and so on.

* Variables $\vec x,x$ will typically correspond to types $\vec \rho, \rho$, variables $\vec y, y$ to $\vec \nat, \nat$, and $\vec z\, z$ to $\vec \tau, \tau$.

We proceed by induction on the structure of $t$, and refer to an inductive hypothesis for a smaller derivation $s$ by $\IH(s)$.

If $t$ is the initial sequent $\vlinf{\id}{}{\sigma \seqar \sigma}{}$ then:

* If $\sigma = \nat$, then $\rhotrans t{\vec \rho} $ is:

\[
\vlderivation{
\vliq{\wk}{}{\vec \rho, \nat \seqar \nat}{
\vlin{\id}{}{\nat \seqar \nat}{\vlhy{}}
\]

There are no new initial sequents so also no thread condition to check.
To verify (<ref>), we have:

\[
\begin{array}{rcll}
\rhotrans t {\vec \rho}\, \vec x\, y & = & \wk^*\, \id\, \vec x\, y & \text{by definition of $\rhotrans t{\vec \rho}$}\\
& = & \id\, y & \text{by $\wk$ axioms}\\
& = & t\, y & \text{by definition of $t$}
\end{array}
\]

* Otherwise $\rhotrans t {\vec \rho}$ is just:

\[
\vlinf{f}{}{\vec \rho , \vec \sigma \seqar \nat }{}
\]

The required threading property is immediate, and to verify (<ref>) we have:

\[
\begin{array}{rcll}
\rhotrans t{\vec \rho}(f)\, \vec x\, \vec y & = & f\, \vec x\, \vec y & \text{by definition of $\rhotrans t{\vec \rho}$. }\\
& = & \id\, (f\, \vec x)\, \vec y & \text{by $\id$ axiom} \\
& = & t\, (f\, \vec x)\, \vec y & \text{by definition of $t$}
\end{array}
\]

If $t$ is the initial sequent $\vlinf{0}{}{\seqar \nat}{}$, then $\rhotrans t{\vec \rho}$ is:

\[
\vlderivation{
\vliq{\wk}{}{\vec \rho \seqar \nat}{
\vlin{0}{}{\seqar \nat}{}
\]

There are no new initial sequents, so no threading property to check.
To verify (<ref>) we have:

\[
\begin{array}{rcll}
\rhotrans t{\vec \rho}\, \vec x & = & \wk^*\, 0\, \vec x &\text{by definition of $\rhotrans t{\vec \rho}$}\\
& = & 0 & \text{by $\wk$ axioms}\\
& = & t & \text{by definition of $t$}
\end{array}
\]

If $t$ is the initial sequent $\vlinf{\succ}{}{\nat \seqar \nat}{}$ then $\rhotrans t{\vec \rho}$ is:

\[
\vlderivation{
\vliq{\wk}{}{\vec \rho, \nat \seqar \nat}{
\vlin{\succ}{}{\nat \seqar \nat}{}
\]

There are no new initial sequents, so no threading property to check.
To verify (<ref>) we have:

\[
\begin{array}{rcll}
\rhotrans t{\vec \rho}\, \vec x\, y & = & \wk^*\, \succ \, \vec x\, y &\text{by definition of $\rhotrans t{\vec \rho}$}\\
& = & \succ\, y & \text{by $\wk$ axioms}\\
& = & t\, y & \text{by definition of $t$}
\end{array}
\]

If $t $ concludes with a weakening step,

\[
\vlderivation{
\vlin{\wk}{}{\vec \sigma , \pi, \vec \nat\seqar \tau}{
\vltr{s}{\vec \sigma, \vec \nat \seqar \tau}{\vlhy{\  }}{\vlhy{\ }}{\vlhy{\ }}
\]

* If $\pi = \nat$ then we define $\rhotrans t{\vec \rho} (\vec f)$ by just commuting with the weakening step:

\[
\toks0={.8}
\vlderivation{
\vlin{\wk}{}{\vec \rho, \vec \sigma, \nat , \vec \nat , \vec \tau \seqar \nat}{
\vltrf{\rhotrans s{\vec \rho}(\vec f)}{\vec \rho, \vec \sigma, \vec \nat, \vec \tau \seqar \nat}{\vlhy{\quad }}{\vlhy{\quad}}{\vlhy{\quad}}{\the\toks0}
\]

The threading property is readily obtained from the inductive hypothesis, and we verify (<ref>) as follows:

\[
\begin{array}{rcll}
\rhotrans t {\vec \rho} (\vec f)\, \vec x\, y\, \vec y\, \vec z & = & \wk\, \rhotrans s {\vec \rho} (\vec f)\, \vec x\, y\, \vec y\, \vec z & \text{by definition of $\rhotrans t{\vec \rho}$}\\
& = & \rhotrans s{\vec \rho}(\vec f)\, \vec x\, \vec y\, \vec z & \text{by $\wk$ axiom} \\
& = & s\, (\vec f\, \vec x)\, \vec y\, \vec z & \text{by $\IH(s)$}\\
& = & \wk\, s\, (\vec f\, \vec x)\, y\, \vec y\, \vec z & \text{by $\wk$ axiom}\\
& = & t\, (\vec f\, \vec x)\, y \, \vec y \, \vec z & \text{by definition of $t$}
\end{array}
\]

* Otherwise, $\rhotrans t{\vec \rho} (\vec f,g)$ is simply just $\rhotrans s{\vec \rho} (\vec f)$ (the initial sequents $f:\vec \pi\seqar \nat$ are never used), and the required properties are inherited directly from the inductive hypothesis.

If $t$ concludes with a contraction step,

\[
\vlderivation{
\vlin{\cntr}{}{\vec \sigma, \pi, \vec \nat \seqar \tau}{
\vltr{s}{\vec \sigma, \pi, \pi, \vec \nat \seqar \tau}{\vlhy{\  }}{\vlhy{\ }}{\vlhy{\ }}
\]

* If $\pi = \nat$ then we define $\rhotrans t{\vec \rho}(\vec f)$ by just commuting with the contraction step:

\[
\toks0={.8}
\vlderivation{
\vlin{\cntr}{}{\vec \rho, \vec \sigma, \nat , \vec \nat , \vec \tau \seqar \nat}{
\vltrf{\rhotrans s{\vec \rho}(\vec f)}{\vec \rho, \vec \sigma, \nat, \nat , \vec \nat, \vec \tau \seqar \nat}{\vlhy{\quad }}{\vlhy{\quad}}{\vlhy{\quad}}{\the\toks0}
\]

The threading property is readily obtained from the inductive hypothesis, and we verify (<ref>) as follows:

\[
\begin{array}{rcll}
\rhotrans t {\vec \rho} (\vec f)\, \vec x\, y\, \vec y\, \vec z & = & \cntr\, \rhotrans s {\vec \rho} (\vec f)\, \vec x\, y\, \vec y\, \vec z & \text{by definition of $\rhotrans t{\vec \rho}$}\\
& = & \rhotrans s{\vec \rho}(\vec f)\, \vec x\, y\, y\, \vec y\, \vec z & \text{by $\cntr$ axiom} \\
& = & s\, (\vec f\, \vec x)\, y\, y\, \vec y\, \vec z & \text{by $\IH(s)$}\\
& = & \cntr\, s\, (\vec f\, \vec x)\, y\, \vec y\, \vec z & \text{by $\cntr$ axiom}\\
& = & t\, (\vec f\, \vec x)\, y \, \vec y \, \vec z & \text{by definition of $t$}
\end{array}
\]

* Otherwise, $\rhotrans t{\vec \rho} (\vec f, g)$ is just $\rhotrans{s}{\vec \rho}(\vec f, g,g)$ and the threading property is immediate from the inductive hypothesis.
(<ref>) is also easily verified:

\[
\begin{array}{rcll}
\rhotrans t{\vec \rho} (\vec f, g)\, \vec x\, \vec y\, \vec z & = & \rhotrans s{\vec \rho}(\vec f, g, g)\, \vec x\, \vec y \, \vec z & \text{by definition of $t$}\\
& = & s\, (\vec f\, \vec x)\, (g\, \vec x)\, (g\, \vec x)\, \vec y\, \vec z & \text{by $\IH(s)$}\\
& = & \cntr\, s\, (\vec f\, \vec x)\,  (g\, \vec x)\, \vec y\, \vec z & \text{by $\cntr$ axiom}\\
& = & t\, (\vec f\, \vec x)\,  (g\, \vec x)\, \vec y\, \vec z & \text{by definition of $t$}
\end{array}
\]

If $t$ concludes with a cut step,

\[
\vlderivation{
\vliin{\cut}{}{\vec \sigma, \vec \nat \seqar \tau}{
\vltr{r}{\vec \sigma, \vec \nat \seqar \pi}{\vlhy{\ }}{\vlhy{\ }}{\vlhy{\ }}
\vltr{s}{\vec \sigma, \pi, \vec \nat \seqar \tau}{\vlhy{\ }}{\vlhy{\ }}{\vlhy{\ }}
\]

* If $\pi = \nat$ then we define $\rhotrans t{\vec \rho}(\vec f)$ by just commuting with the cut step:

\[
\toks0={.8}
\toks1={.8}
\vlderivation{
\vliin{\cut_\nat}{}{\vec \rho, \vec \nat, \vec \tau \seqar \nat}{
\vltrf{\rhotrans r{\vec \rho}(\vec f)}{\vec \rho, \vec \nat \seqar \nat}{\vlhy{\quad}}{\vlhy{\quad}}{\vlhy{\quad}}{\the\toks0}
\vltrf{\rhotrans s{\vec \rho}(\vec f)}{\vec \rho, \nat, \vec \nat , \vec \tau \seqar \nat}{\vlhy{\quad}}{\vlhy{\quad}}{\vlhy{\quad}}{\the\toks1}
\]

The threading property is readily obtained from the inductive hypotheses and we verify (<ref>) as follows:

\[
\begin{array}{rcll}
\rhotrans t{\vec \rho} (\vec f)\, \vec x\, \vec y\, \vec z & = & \rhotrans s{\vec \rho}(\vec f)\, \vec x\, (\rhotrans r{\vec \rho}(\vec f) \, \vec x\, \vec y)\, \vec y\, \vec z & \text{by $\cut$ axiom} \\
& = & s\, (\vec f\, \vec x)\, (r\, (\vec f\, \vec x)\, \vec y)\, \vec y\, \vec z & \text{by $\IH(r)$ and $\IH(s)$} \\
& = & t\, (\vec f\, \vec x)\, \vec y\, \vec z & \text{by $\cut$ axiom}
\end{array}
\]

* Otherwise, we define $\rhotrans t{\vec \rho}(\vec f)$ as:

\[
\toks0={.4}
\toks1={.8}
\vlderivation{
\vliq{\cntr}{}{ \vec \rho, \vec \nat , \vec \tau \seqar \nat }{
\vltrf{\rhotrans s{\vec \rho, \vec \nat}}{\vec \rho, \vec \nat, \vec \nat , \vec \tau \seqar \nat}{
\vliq{\wk}{}{\vec \rho, \vec \nat, \vec \sigma_i \seqar \nat}{
\vlin{f_i}{i}{\vec \rho, \vec \sigma_i \seqar \nat}{\vlhy{}}
\vlhy{}
\vltrf{\rhotrans r{\vec \rho}(\vec f)}{\vec \rho, \vec \nat , \vec \pi \seqar \nat}{\vlhy{\quad}}{\vlhy{\quad}}{\vlhy{\quad}}{\the\toks1}
\]

The threading property is readily obtained from the inductive hypotheses, and we verify (<ref>) as follows:

\[
\begin{array}{rcll}
\rhotrans t{\vec \rho}\, \vec x\, \vec y\, \vec z & = & \rhotrans s{\vec \rho, \vec \nat} (\wk^* \vec f , \rhotrans r{\vec \rho} (\vec f))\, \vec x\, \vec y\, \vec y\, \vec z & \text{by $\cntr$ axioms}\\
& = & s\, (\wk^* \vec f\, \vec x\, \vec y)\, (\rhotrans r{\vec \rho}(\vec f)\, \vec x\, \vec y )\, \vec y\, \vec z & \text{by $\IH(s)$}\\
& = & s\, (\wk^* \vec f\, \vec x\, \vec y)\,  (r\, (\vec f\, \vec x)\, \vec y)\, \vec y\, \vec z & \text{by $\IH(r)$ and $\extensionality$}\\
& = & s\, (\vec f\, \vec x)\, (r\, (\vec f\, \vec x)\, \vec y)\, \vec y\, \vec z & \text{by $\wk$ axioms and $\extensionality$}\\
& = & t\, (\vec f\, \vec x)\, \vec y\, \vec z & \text{by definition of $t$}
\end{array}
\]

If $t$ concludes with a right-implication step,

\[
\vlderivation{
\vlin{\rightimp}{}{\vec \sigma, \vec \nat \seqar \pi \to \tau}{
\vltr{s}{\vec \sigma, \pi , \vec \nat \seqar \tau}{\vlhy{\ }}{\vlhy{\ }}{\vlhy{\ }}
\]

* If $\pi=\nat$ then $\rhotrans t{\vec \rho}(\vec f)$ is just:

\[
\toks0={.8}
\vlderivation{
\vliq{\exch}{}{\vec \rho, \vec \nat, \nat, \vec \tau \seqar \nat}{
\vltrf{\rhotrans s{\vec \rho}(\vec f)}{\vec \rho, \nat, \vec \nat , \vec \tau \seqar \nat}{\vlhy{\quad}}{\vlhy{\quad}}{\vlhy{\quad}}{\the\toks0}
\]

The threading property is readily obtained from the inductive hypothesis and (<ref>) is easily verified:

\[
\begin{array}{rcll}
\rhotrans t{\vec \rho}(\vec f)\, \vec x\, \vec y\, y\, \vec z & = & \rhotrans s{\vec \rho}(\vec f)\, \vec x\, y\, \vec y\, \vec z & \text{by $\exch$ axioms}\\
& = & s\, (\vec f\, \vec x)\, y\, \vec y\, \vec z & \text{by $\IH(s)$}\\
& = & t\, (\vec f\, \vec x)\, \vec y\, y\, \vec z & \text{by $\rightimp$ axiom}
\end{array}
\]

* Otherwise $\level (\pi)\leq n$ and we define $\rhotrans t{\vec \rho} (\vec f)$ as:

\[
\toks0={.4}
\vlderivation{
\vliq{\exch}{}{\vec \rho, \vec \nat , \pi, \vec \tau \seqar \nat}{
\vltrf{\rhotrans s{\vec \rho, \pi}}{\vec \rho, \pi, \vec \nat ,\vec \tau \seqar \nat}{
\vlin{\wk}{}{\vec \rho, \pi, \vec \sigma_i \seqar \nat}{
\vlin{f_i}{i}{\vec \rho, \vec \sigma_i \seqar \nat}{\vlhy{}}
\vlhy{}
\vliq{\wk}{}{\vec \rho, \pi, \vec \pi \seqar \nat}{
\vliq{\apply}{}{\pi, \vec \pi \seqar \nat}{\vlhy{}}
\]

where $\apply$ is a simple (finite) derivation satisfying:

\begin{equation}
\label{eqn:apply-eqn}
\apply\, z\, \vec w \ = \ z\, \vec w
\end{equation}

The threading property is readily obtained from the inductive hypothesis, and we verify (<ref>) as follows:

\[
\begin{array}{rcll}
\rhotrans t{\vec \rho}\, \vec x\, \vec y\, z\, \vec z & = & \rhotrans s{\vec \rho, \pi} (\wk\, \vec f , \wk^* \apply) \, \vec x\, z\, \vec y\, \vec z & \text{by $\exch$ axioms} \\
& = & s\, (\wk\, \vec f\, \vec x\, z)\, (\wk^*\apply\, \vec x\, z)\, \vec y\, \vec z & \text{by $\IH(s)$} \\
& = & s\, (\vec f\, \vec x) \, (\apply\, z)\, \vec y\, \vec z & \text{by $\wk$ axioms and $\extensionality$}\\
& = & s\, (\vec f\, \vec x)\, z\, \vec y\, \vec z & \text{by \eqref{eqn:apply-eqn} and $\extensionality$}\\
& = & t\, (\vec f\, \vec x)\, \vec y\, z\, \vec z & \text{by $\rightimp$ axiom}
\end{array}
\]

If $t$ concludes with a left-implication step,

\[
\vlderivation{
\vliin{\leftimp}{}{\vec \sigma, \tau' \to \pi, \vec \nat \seqar \tau}{
\vltr{r}{\vec \sigma , \vec \nat \seqar \tau'}{\vlhy{\ }}{\vlhy{\ }}{\vlhy{\ }}
\vltr{s}{\vec \sigma, \pi, \vec \nat \seqar \tau}{\vlhy{\ }}{\vlhy{\ }}{\vlhy{\ }}
\]

* If $\pi = \nat$ then we define $\rhotrans t{\vec \rho} (\vec f,g)$ as:

\[
\toks0={0.8}
\vlderivation{
\vliin{\cut}{}{\vec \rho, \vec \nat , \vec \tau \seqar \nat}{
\vliq{\rightimp}{}{\vec \rho, \vec \nat \seqar \tau'}{
\vltrf{\rhotrans r{\vec \rho}(\vec f)}{\vec \rho, \vec \nat, \vec \tau'\seqar \nat}{\vlhy{\quad}}{\vlhy{\quad}}{\vlhy{\quad}}{\the\toks0}
\vliin{\cut}{}{\vec \rho, \tau', \vec \nat , \vec \tau \seqar \nat}{
\vlin{g}{}{\vec \rho, \tau' \seqar \nat}{\vlhy{}}
\vltrf{\rhotrans s{\vec \rho}(\vec f)}{\vec \rho, \nat, \vec \nat, \vec \tau \seqar \nat}{\vlhy{\quad}}{\vlhy{\quad}}{\vlhy{\quad}}{\the\toks0}
\]

The threading property is readily obtained from the inductive hypotheses and we verify (<ref>) as follows:

\[
\begin{array}{rcll}
\rhotrans t{\vec \rho} (\vec f,g)\, \vec x\, \vec y\, \vec z &  = & \cut\, g\, \rhotrans s{\vec \rho}(\vec f)\, \vec x\, (\rightimp^*\, \rhotrans r{\vec \rho}(\vec f)\, \vec x\, \vec y)\, \vec y\, \vec z & \text{by $\cut$ axiom} \\
& = & \rhotrans s{\vec \rho}(\vec f)\, \vec x\, (g\, \vec x\, (\rightimp^*\, \rhotrans r{\vec \rho}(\vec f)\, \vec x\, \vec y))\, \vec y\, \vec z & \text{by $\cut$ axiom}\\
& =& \rhotrans s{\vec \rho}(\vec f)\, \vec x\, (g\, \vec x\, ( \rhotrans r{\vec \rho}(\vec f)\, \vec x\, \vec y))\, \vec y\, \vec z & \text{by $\rightimp$ axioms and $\extensionality$}\\
& = & s\, (\vec f\, \vec x)\, (g\, \vec x\, ( \rhotrans r{\vec \rho}(\vec f)\, \vec x\, \vec y))\, \vec y\, \vec z & \text{by $\IH(s)$}\\
& = & s\, (\vec f\, \vec x)\, (g\, \vec x\, (r\, (\vec f\, \vec x)\, \vec y))\, \vec y\, \vec z & \text{by $\IH(r)$ and $\extensionality$}\\
& = & t\, (\vec f\, \vec x)\, (\vec g\, \vec x)\, \vec y\, \vec z & \text{by $\leftimp$ axiom}
\end{array}
\]

* Otherwise we define $\rhotrans t{\vec \rho}(\vec f,g)$ as:

\[
\toks0={.3}
\toks1={.8}
\vlderivation{
\vliq{\cntr}{}{\vec \rho, \vec \nat, \vec \tau \seqar \nat}{
\vltrf{\rhotrans s{\vec \rho, \vec \nat}}{\vec \rho, \vec \nat, \vec \nat, \vec \tau \seqar \nat}{
\vliq{\wk}{}{\vec \rho, \vec \nat, \vec \sigma_i \seqar \nat}{
\vlin{f_i}{i}{\vec \rho, \vec \sigma_i \seqar \nat}{\vlhy{}}
\vlhy{}
\vliin{\cut}{}{\vec \rho, \vec \nat, \vec \pi \seqar \nat}{
\vliq{\rightimp}{}{\vec \rho, \vec \nat \seqar \tau' }{
\vltrf{\rhotrans r{\vec \rho} (\vec f)}{\vec \rho, \vec \nat, \vec \tau'\seqar \nat}{\vlhy{\quad}}{\vlhy{\quad}}{\vlhy{\quad}}{\the\toks1}
\vliq{\wk}{}{\vec \rho , \vec \nat, \tau', \vec \pi \seqar \nat}{
\vlin{g}{}{\vec \rho, \tau', \vec \pi \seqar \nat}{\vlhy{}}
\]

The threading property is readily obtained from the inductive hypotheses and we verify (<ref>) as follows:

\[
\begin{array}{rcll}
\rhotrans t{\vec \rho}(\vec f,g)\, \vec x\, \vec y\, \vec z & = & \rhotrans s{\vec \rho, \vec \nat} ( \wk^*\vec f, \cut (\rightimp^* \rhotrans r{\vec \rho}(\vec f)) (\wk^* g) )\, \vec x\, \vec y\, \vec y\, \vec z & \text{by $\cntr$ axioms}\\
& = & s\, (\wk^*\vec f\, \vec x\, \vec y)\, (\cut (\rightimp^* \rhotrans r{\vec \rho}(\vec f)) (\wk^* g) \vec x\, \vec y)\, \vec y\, \vec z & \text{by $\IH(s)$}\\
& = & s\, (\vec f\, \vec x)\, (\cut (\rightimp^* \rhotrans r{\vec \rho}(\vec f)) (\wk^* g) \vec x\, \vec y)\, \vec y\, \vec z & \text{by $\wk$ axioms and $\extensionality$}\\
& = & s\, (\vec f\, \vec x) (\wk^* g\, \vec x\, \vec y\, (\rightimp^* \rhotrans r{\vec \rho}(\vec f)\, \vec x\, \vec y))\, \vec y \, \vec z & \text{by $\cut$ axiom}\\
& = & s\, (\vec f\, \vec x) (g\, \vec x\,  (\rightimp^* \rhotrans r{\vec \rho}(\vec f)\, \vec x\, \vec y))\, \vec y \, \vec z & \text{by $\wk$ axioms and $\extensionality$} \\
& = & s\, (\vec f\, \vec x) (g\, \vec x\,  ( \rhotrans r{\vec \rho}(\vec f)\, \vec x\, \vec y))\, \vec y \, \vec z & \text{by $\rightimp$ axioms and $\extensionality$}\\
& = & s\, (\vec f\, \vec x)\, (g\, \vec x\, (r\, (\vec f\, \vec x) \, \vec y))\, \vec y \, \vec z & \text{by $\IH(r)$ and $\extensionality$}\\
& = & t\, (\vec f\, \vec x)\, (g\, \vec x)\, \vec y\, \vec z & \text{by $\leftimp $ axiom}
\end{array}
\]

Finally, if $t$ concludes with a recursion step,

\[
\vlderivation{
\vliin{\rec}{}{\vec \sigma , \vec \nat, \nat \seqar \tau}{
\vltr{r}{\vec \sigma , \vec \nat \seqar \tau}{\vlhy{\ }}{\vlhy{\ }}{\vlhy{\ }}
\vltr{s}{\vec \sigma, \tau, \vec \nat, \nat \seqar \tau}{\vlhy{\ }}{\vlhy{\ }}{\vlhy{\ }}
\]

* If $\tau = \nat$ (so $\vec \tau$ is empty) then we define $\rhotrans t{\vec \rho}$ similarly to before in Example <ref>,

\begin{equation}
\label{eqn:rec-to-cyc-low-comp}
\toks0={.8}
\vlderivation{
\vliin{\cond}{\bullet}{\vec \rho, \vec \nat, \blue{\nat} \seqar \nat}{
\vltrf{\rhotrans r{\vec \rho} (\vec f)}{\vec \rho, \vec \nat \seqar \nat}{\vlhy{\quad}}{\vlhy{\quad}}{\vlhy{\quad}}{\the\toks0}
\vliin{\cut}{}{\vec \rho, \vec \nat, \blue{\nat} \seqar \nat}{
\vlin{\cond}{\bullet}{\vec \rho, \vec \nat, \blue{\nat} \seqar \nat}{\vlhy{\vdots}}
\vltrf{\rhotrans s{\vec \rho}(\vec f)}{\vec \rho, \nat, \vec \nat, \nat \seqar \nat}{\vlhy{\quad}}{\vlhy{\quad}}{\vlhy{\quad}}{\the\toks0}
\end{equation}

where $\bullet$ marks roots of identical sub-coderivations.
The threading property is readily obtained from the inductive hypotheses.
For progressiveness, any infinite branch either just loops on $\bullet$ indefinitely, in which case there is a progressing thread along the blue $\blue \nat$, or is eventually in just $\rhotrans r{\vec \rho}(\vec f)$ or $\rhotrans s{\vec \rho}(\vec f)$, in which case there is a progressing thread by the inductive hypotheses.
To verify (<ref>) we shall show,

\begin{equation}
\label{eqn:ind-to-cyc-rec-n-ih}
\rhotrans t{\vec \rho}(\vec f)\, \vec x\, \vec y\, y \ = \ t\, (\vec f\, \vec x)\, \vec y\, y
\end{equation}

by (object-level) induction on $y$:

\[
\begin{array}{rcll}
\rhotrans t{\vec \rho}(\vec f)\, \vec x\, \vec y\, 0 & = & \rhotrans r{\vec f}(\vec f)\, \vec x\, \vec y & \text{by $\cond$ axiom}\\
& = & r\, (\vec f\, \vec x)\, \vec y& \text{by $\IH(r)$} \\
& = & t\, (\vec f\, \vec x)\, \vec y\, 0 & \text{by $\rec$ axioms}\\
\noalign{\medskip}
\rhotrans t{\vec \rho}(\vec f)\, \vec x\, \vec y\, \succ y & = & \cut\, \rhotrans t{\vec \rho}(\vec f)\, \rhotrans s{\vec \rho}(\vec f)\, \vec x\, \vec y\, y & \text{by $\cond$ axioms}\\
& = & \rhotrans s{\vec \rho}(\vec f)\, \vec x\, (\rhotrans t{\vec \rho}(\vec f)\, \vec x\, \vec y\, y)\, \vec y\, y & \text{by $\cut$ axiom}\\
& = & s\, (\vec f\, \vec x)\, (\rhotrans t{\vec \rho}(\vec f)\, \vec x\, \vec y\, y)\, \vec y\, y & \text{by $\IH(s)$}\\
& = & s\, (\vec f\, \vec x)\, (t\, (\vec f\, \vec x)\, \vec y\, y)\, \vec y\, y & \text{by inductive hypothesis \eqref{eqn:ind-to-cyc-rec-n-ih}}\\
& = & t\, (\vec f\, \vec x)\, \vec y\, \succ y & \text{by $\rec$ axioms}
\end{array}
\]

* Otherwise we define $\rhotrans t{\vec \rho}(\vec f)$ to be,

\begin{equation}
\label{eqn:rec-to-cyc-high-comp}
\toks0={.8}
\toks1={.3}
\vlderivation{
\vliin{\cond}{\bullet}{\vec \rho , \vec \nat, \blue \nat, \vec \tau \seqar \nat}{
\vltrf{\rhotrans r{\vec \rho}(\vec f)}{\vec \rho, \vec \nat, \vec \tau \seqar \nat}{\vlhy{\quad}}{\vlhy{\quad}}{\vlhy{\quad}}{\the\toks0}
\vliq{\cntr}{}{\vec \rho, \vec \nat, \blue{\nat }, \vec \tau \seqar \nat}{
\vltrf{\rhotrans s{\vec \rho, \vec \nat , \blue{\nat}}}{\vec \rho, \vec \nat , \blue{\nat }, \vec \nat , \nat, \vec \tau \seqar \nat}{
\vliq{\wk}{}{\vec \rho, \vec \nat, \blue{\nat }, \vec \sigma_i \seqar \nat}{
\vlin{f_i}{i}{\vec \rho, \vec \sigma_i \seqar \nat}{\vlhy{}}
\vlhy{}
\vlin{\cond}{\bullet}{\vec \rho, \vec \nat, \blue{\nat}, \vec \tau \seqar \nat}{\vlhy{\vdots}}
\end{equation}

where $\bullet$ marks roots of identical sub-coderivations.
The threading property is readily obtained from the inductive hypotheses.
For progressiveness, notice that any infinite branch that hits $\bullet$ infinitely often will have a progressing thread along the blue $\blue \nat$, thanks to the threading property from the inductive hypothesis for $s$.
Any other infinite branch is eventually in $\rhotrans r{\vec \rho}(\vec f)$ or $\rhotrans{s}{\vec \rho, \vec \nat, \nat}$, so progressiveness follows from the inductive hypotheses.

To verify (<ref>) we show that,

\begin{equation}
\label{eqn:ind-to-cyc-rec-ih}
\rhotrans t{\vec \rho}(\vec f)\, \vec x\, \vec y\, y\, \vec z \ = \ t\, (\vec f\, \vec x)\, \vec y\, y\, \vec z
\end{equation}

by (object-level) induction on $y$:

\[
\begin{array}{rcll}
\rhotrans t{\vec \rho}(\vec f)\, \vec x\, \vec y\, 0 \, \vec z & = & \rhotrans r{\vec \rho}(\vec f)\, \vec x\, \vec y\, \vec z & \text{by $\cond$ axioms}\\
& = & r\, (\vec f\, \vec x)\, \vec y\, \vec z & \text{by $\IH(r)$}\\
& = & t\, (\vec f\, \vec x)\, \vec y\, 0\, \vec z & \text{by $\rec$ axioms}\\
\noalign{\medskip}
\rhotrans t{\vec \rho}(\vec f)\, \vec x\, \vec y\, \succ y\, \vec z & = & \cntr^*\, \rhotrans s{\vec \rho, \vec \nat , \nat}(\wk^*\vec f, \rhotrans t{\vec \rho}(\vec f))\, \vec x\, \vec y\, y\, \vec z & \text{by $\cond$ axioms}\\
& = & \rhotrans s{\vec \rho, \vec \nat , \nat}(\wk^*\vec f, \rhotrans t{\vec \rho}(\vec f))\, \vec x\, \vec y\, y\, \vec y\, y\, \vec z & \text{by $\cntr$ axioms}\\
& = & s\, (\wk^* \vec f\, \vec x\, \vec y\, y)\, (\rhotrans t{\vec \rho}(\vec f)\, \vec x\, \vec y\, y)\, \vec y\, y\, \vec z & \text{by $\IH(s)$}\\
& = & s\, (\vec f\, \vec x)\, (\rhotrans t{\vec \rho}(\vec f)\, \vec x\, \vec y\, y)\, \vec y\, y\, \vec z & \text{by $\wk$ axioms and $\extensionality$} \\
& = & s\, (\vec f\, \vec x)\, (t\, (\vec f \, \vec x)\, \vec y\, y)\, \vec y\, y\, \vec z & \text{by inductive hypothesis \eqref{eqn:ind-to-cyc-rec-ih}}\\
& = & t\, (\vec f\, \vec x)\, \vec y\, \succ y\, \vec z & \text{by $\rec$ axioms} \qedhere
\end{array}
\]

§.§ $\nC n$ simulates $\nT{n+1}$

We are now ready to prove the main result of this section, which essentially boils down to an instance of the main Lemma in the previous subsection.

Without loss of generality assume $t$ is a derivation of $\seqar \sigma$ and apply Lemma <ref> with $\vec \rho$ empty, to obtain a coderivation $\rhotrans t \emptyset: \vec \sigma \seqar \nat$ s.t.:

\begin{equation}
\label{eqn:thm-csimt-use-of-lemma}
\nC n, \rec_{n+1} \proves \ t\, \vec x\, =\, \rhotrans t \emptyset\, \vec x
\end{equation}

Note that $\rhotrans t \emptyset$ uses no new initial sequents since the antecedent of the conclusion of $t$ is empty.
Now we define $t'$ as:

\[
\vlderivation{
\vliq{\rightimp}{}{\seqar \sigma}{
\vltr{\rhotrans t \emptyset}{\vec \sigma \seqar \nat}{\vlhy{\ }}{\vlhy{\ }}{\vlhy{\ }}
\]

We verify (<ref>) as follows, working inside the theory:

\[
\begin{array}{rll}
& t\, \vec x \, = \, \rhotrans t \emptyset\, \vec x & \text{by \eqref{eqn:thm-csimt-use-of-lemma}}\\
\therefore & t\, \vec x \, = \, \rightimp^*\rhotrans t \emptyset\, \vec x & \text{by $\rightimp$ axioms} \\
\therefore & t\, \vec x\, = \, t'\vec x & \text{by definition of $t'$}\\
\therefore & t = t' & \text{by $\extensionality$} \qedhere
\end{array}
\]

§ COTERM-BASED MODELS OF $\T$ AND $\C$

Our ultimate goal is to establish a converse to the main result of the previous section, which we shall demonstrate in the next two sections.
Before that we need to introduce some type structures arising from our formulation of $\C$.
Ultimately, we will reduce the simulation of $\nC n$ in $\nT{n+1}$ to the provability in an appropriate arithmetic theory that certain structures are models of $\C$ .

We cannot formalise the standard model $\nmod$ in arithmetic for cardinality reasons, however there are natural models of partial recursive functionals that can be formalised, namely the hereditarily recursive and the hereditarily effective operations of finite type (see, e.g., [48]).

Since regular coterms form a Turing-complete programming language (cf. Proposition <ref>), the domains of our structures will simply be classes of regular coterms.
Viewed as Kleene-Herbrand-Gödel equational specifications (see, e.g., [35]), note that the corresponding notion of computation is subsumed by provable equality of coterms by rules and axioms of $\C$.
In fact, we will distill from $\C$ a suitable fragment of provable equality, namely that induced by the respective rewriting system.
This will eventually give rise to an intensional model, whence an extensional one can be obtained by, as usual, taking the extensional collapse.

§.§ Reduction and conversion of coterms

The reduction relation $\reduces$ on coterms is defined by orienting all the equations in Figures <ref>, <ref> and <ref> left-to-right and taking closure under substitution and contexts.

$\reduces$ is the least relation on (co)terms satisfying the reductions in Figure <ref>, where the types of each rule label are as indicated in Figures <ref>, <ref> and <ref>,[Again there is no reason, other than for ease of legibility, that we write terms variables $s,t$ etc. for the premiss inputs and variables $x,y$ etc. for the antecedent inputs. Under substitution, it makes no difference.] and closed under substitution and contexts.

We write $\conv$ for the reflexive, symmetric, transitive closure of $\reduces$, and freely use standard rewriting theoretic terminology and notations for these relations.
We sometimes write $\reduces_\sigma$ for the restriction of $\reduces$ to coterms of type $\sigma$, and $\conv_\sigma$ for the restriction of $\conv$ to coterms of type $\sigma$.

\[
\begin{array}{rcl}
\id \ x & \reduces & x \\
\exch \ t \ \vec x\  x \ y\ \vec y & \reduces & t \ \vec x \ y \ x \ \vec y \\
\wk \ t  \ \vec x \ x & \reduces & t \ \vec x \\
\cntr \ t\ \vec x \ x & \reduces & t \ \vec x \ x \ x \\
\cut \ s\ t\ \vec x & \reduces & t \ \vec x \ (s \ \vec x ) \\
\leftimp \ s\ t\ \vec x\ y & \reduces & t \ \vec x\ (y\ (r\ \vec x) ) \\
\rightimp \ t \ \vec x \ x & \reduces & t\ \vec x\ x \\
\noalign{\smallskip}
\rec\ s\ t\ \vec x\ 0 & \reduces & s\ \vec x\\
\rec\ s\ t\ \vec x\ \succ y & \reduces & t\ \vec x\ (\rec\ s\ t\ \vec x \ y)\\
\noalign{\smallskip}
\cond \ s\ t\ \vec x\ 0 & \reduces & s \ \vec x \\
\cond\ s\ t\ \vec x\ \succ y & \reduces & t\ \vec x\ y
\end{array}
\]

Reduction rules for (co)terms

We shall address metamathematical matters w.r.t. formalising reduction and reduction sequences shortly, but first let us examine some basic mathematical properties of reduction.

§.§ On normality and numerality

The term model for $\T$, due to Tait [62], may be obtained by proving normalisation and confluence of the rewrite system in Figure <ref> for terms, and taking the (unique) normal forms of closed terms as the domain of the type structure.
Crucial to this approach is the property that the only closed normal forms of terms of type $\nat$ are the numerals, which allows induction in $\T$ to be reduced to induction at the meta-level.

Since regular coterms are Turing-complete, cf. Proposition <ref>,[Notice from that proof that Turing-completeness is retained under $\reduces$ as a model of execution.] one cannot hope for such a normalisation result, and so our models will be obtained by restricting to normalising coterms.
Normalisation for progressing coterms at type $\nat$ follows by showing that they are indeed elements of the type structure.

We will address confluence shortly, adapting known proofs to the non-wellfounded setting.
However, we point out that the final point, that closed normal forms of type $\nat$ are just the numerals, fails for coterms:

There are closed $\reduces$-normal coterms of type $\nat$ that are not numerals, e.g. the coterm $H$ with,

\[
H = \cond \, 0 \, 1\, H
\]

that returns $0$ or $1$, depending on whether it itself is $0$ or non-zero. Clearly $H$ is undefined in the standard model, though may be consistently interpreted by $0$ or $1$ in extensions of it.
Note that $H$ is even a regular counterexample to numerality of closed $\reduces$-normal coterms, and so the $\reduces$-normal regular coterms will be too large a domain for the type structures we later define.
For this reason, our type structures will restrict the interpretation of $\nat$ to (classes of) coterms that normalise to a numeral.

§.§ Formalising reduction sequences of regular coterms

Before continuing, let us make some comments about our arithmetisation of reduction sequences.
First and foremost, to avoid unnecessary technicalities, all the coterms we consider later will be regular, and so can be coded by natural numbers.
Thus all quantification over them is strictly first-order.
In fact, many of our results go through in a more general setting since finite reduction sequences may be coded by finite data, but such a treatment is beyond the scope of this work.
In what follows we shall be rather brief, outlining only the main ideas and proof methods behind the results we need.

While equality for arbitrary coterms is $\Pi^0_1$, we should justify that it is recursive for regular coterms.
Namely, we should argue that we may decide if two presentations of regular coterms (as finite labelled graphs) represent the same coterm (as an infinite labelled tree), i.e. are bisimilar.

For $v \in \{0,1\}^*$ and a coterm $t$, construed as a labelled binary tree, let us temporarily write $t_v$ for the sub-coterm of $t$ rooted at position $v$, and $t[v]$ for the rule instance at position $v$.
For a regular presentation $G$ of a coterm, a finite rooted labelled graph, write $G(v)$ for the node of $G$ reached by following the word $v$ along its edge relation.
Note that all of these notions are provably computable in $t$, $G$ and $v$ in $\RCA$.

Bisimilarity of rooted finite labelled directed graphs is provably recursive in $\RCA$.

For recursivity, just blindly search for a bisimulation relation between the two vertex sets (in exponential time).
Now we need to show that two finite graphs $G$ and $H$ are bisimilar if and only if there is a bisimulation between them:

* Suppose $R$ is a bisimulation between $G$ and $H$. We prove by induction on node position $v\in \{0,1\}^*$ that $(G(v),H(v)) \in R$. From here, by definition of a bisimulation, any two nodes related by $R$ have the same label, and so the unfoldings of $G$ and $H$ are equal.

* Suppose $G$ and $H$ have the same unfolding. We inductively construct a bisimulation $R$ from the root by continually adding $(G(v),H(v))$ to $R$. We terminate when we hit a pair that is already in $R$, which will happen in at most $|G||H|+1$ steps, by the finite pigeonhole principle.[Note that, while the usual infinite pigeonhole principle is not provable in $\RCA$, it is easy to see that the finite one is provable in $\RCA$ (and even weaker theories), by a straightforward $\Sigma^0_1$ induction.]

Equality for regular coterms is provably $\Delta^0_1$ in $\RCA$.

Now, we better show that reduction preserves certain properties of coterms, not least regularity.
More generally, since we will work with a certain class of regular coterms, we should make sure that this class is closed under reduction.

If $s\reduces t$ then $t$ is finitely composed of sub-coterms of $s$:

\begin{equation}
\label{eqn:red-cont}
\exists \text{ a finite term } r(x_1,\dots,x_n).\, \exists \langle v_1,\dots, v_n\rangle .\,  t = {r(s_{v_1}, \dots, s_{v_n})}
\end{equation}

This result holds for arbitrary coterms and, indeed, the existential quantifiers may be explicitly witnessed by primitive recursive functions in terms of $s$ and $t$.
We can take $s_{v_1},\dots ,s_{v_n}$ to include the coderivations indicated in the contractum of a reduction in Figure <ref>, as well as the `comb' of the redex of the reduction in $s$, i.e. the siblings of all the nodes in the path leading to the redex.
$r(\vec x)$ is now the finite term induced by the contracta and this comb.[Note that there is no need for weak König's lemma here, since combs may be explicitly proved to induce finite trees in $\RCA$. In any case, $\WKL$ is arithmetically conservative over $\RCA$.]

As an immediate consequence of the above proposition we have, for arbitrary coterms:

Suppose $s \reduces t$.

*  If $s$ has only finitely many variable occurrences then so does $t$.

*  If $s$ has only finitely many redexes then so does $t$.

*  If $s$ is regular then so is $t$.

*  If $s$ is progressing then so is $t$.

Restricting now to regular coterms, we obtain the analogue of Proposition <ref> for reduction sequences by $\Sigma^0_1$-induction:

If $s$ is regular and $s\reduces^*t$, then (<ref>).

Again, we could also deduce a similar result for arbitrary coterms, specifying reduction sequences as finite lists of redex positions, but formally developing this is beyond the scope of this work.
As expected, we obtain the same properties of Corollary <ref> for regular reduction sequences:

Suppose $s$ is regular and $s\reduces^*t$. Then the conditions (<ref>), (<ref>), (<ref>) and (<ref>) from Corollary <ref> hold.

§.§ Confluence of reduction

In order to obtain basic metamathematical properties of the coterm models we later consider, we need to know that our model of computation is deterministic, so that coterms have unique interpretations.
There are various ways to prove this in arithmetic, but we will approach it in terms of confluence in rewriting theory.

We will need to formalise our argument within $\RCA$ for later results,
comprising an additional contribution to the literature,
bounding the logical strength of confluence for finitary and certain infinitary rewrite systems operating with regular coterms.
To facilitate this formalisation, all the coterms we consider in this section will be finite applications of regular coderivations to variables and constants (`s' for short) which, by Proposition <ref>, are closed under reduction sequences, provably in $\RCA$.
s are not necessarily progressing but, since coderivations are closed and have no redexes or variables, s have at most finitely many variables or redexes, provably in $\RCA$ (each application operation can add at most one variable and redex).

The main goal of this subsection is to prove the following:

Let $t:\sigma$ be a .
If $t_0 \unreducess t \reduces^* t_1$ then there is $t':\sigma$ such that $t_0 \reduces^* t'\unreducess t_1$.

To some extent, we follow a standard approach to proving this result.
In particular we aim to find a relation $\vartriangleright$ such that:

* $s\reduces t $ $\implies$ $s\vartriangleright t$ $\implies$ $s\reduces^*t$ ; and,

* $\vartriangleright$ satisfies the `diamond' property: if $t_0 \vartriangleleft t \vartriangleright t_1$ then there is $t'$ such that $t_0 \vartriangleright t' \vartriangleleft t_1$.

The first property ensures that the reflexive transitive closure of $\reduces $ and $\vartriangleright$ coincide, i.e. $\reduces^* = \vartriangleright^*$. The second property then ensures confluence of $\reduces^*$

Since coterms are infinite (and, moreover, non-wellfounded), we must carry out our argument without appeal to induction on term structure, ruling out standard arguments due to Tait and Martin-Löf (cf., e.g., [34]).
Approaches of Takahashi in [65] and others that rely on complete developments could potentially be adapted, since we are working with s which have only finitely many redexes.

However, instead, we perform
an argument by induction on reduction length, as in, e.g., [53], which also seems to require less machinery from rewriting theory.

We define the relation $\parred$ on s as follows:

*  $t\parred t$ for any  $t$.

*  For a reduction step $\mathsf r \, \vec t \reduces r(\vec t)$, if each $t_i \parred t_i' $ then we have $\mathsf r\, \vec t \parred r(\vec t' )$.

*  For a reduction step $\mathsf r\, \vec t\, \succ s\, \reduces\, r(\vec t,s)$ (i.e. a $\rec$ or $\cond$ successor step), if each $t_i \parred t_i' $ and $s \parred s'$ then we have $\mathsf r\, \vec t\, \succ s\, \parred\, r(\vec t',s')$.

*  If $s\, \parred s' $ and $t \parred t' $ then $s\,t \parred s'\, t'$.

Note that we really do seem to require clause (<ref>), $t \parred t$, for arbitrary s $t$, not just variables and constants, since we cannot finitely derive the former from the latter.

$s\reduces t\ \implies \ s\parred t\ \implies \ s\reduces^* t $.

The proof of this result is not difficult, but before giving an argument let us point out a particular consequence that we will need, obtained by $\Sigma^0_1$-induction on the length of reduction sequences:

$s\reduces^* t \ \iff \ s\parred^* t$

Even though it is not necessary to prove the proposition above, we shall first prove the following useful lemma since we will use it later:

Suppose $t\parred t'$. If $s\parred s'$ then $s[t/x] \parred s'[t'/x]$, for a variable $x$ of the same type as $t$ and $t'$.

In what follows, we may write $d:s \reduces^* t$ or $d:s\parred t$ or even $d:s\parred^* t$ to indicate that $d$ is a (finite) derivation witnessing the respective relation.

We show $d: s\parred s' \, \implies \,  s[t/x] \parred s'[t'/x]$ by $\Sigma^0_1$-induction on the structure of the derivation $d:s \parred s'$.

If $d$ is obtained by just (<ref>), i.e. $s' = s$, then we show $s[t/x] \parred s[t'/x]$ by a subinduction on the maximum depth of an $x$-occurrence in $s$.
(Recall that s have only finitely many variable occurrences.)

* if $s$ is just the variable $x$ then $s[t/x] \parred s'[t'/x]$ by assumption of $t\parred t'$.

* if $s$ is just a variable $y \neq x$ then $s[t/x] = y \parred y = s'[t'/x]$ by (<ref>).

* if $s$ is just a constant symbol $\mathsf r$ then $s[t/x] = \mathsf r \parred \mathsf r = s'[t'/x]$ by (<ref>).

* if $s = s_0s_1$ then all the (finitely many) occurrences of $x$ in $s_0$ and $s_1$ have lower depth, so we have $s_0[t/x]\parred s_0[t'/x]$ and $s_1[t/x] \parred s_1[t'/x]$ by the inductive hypothesis, whence $s[t/x] \parred s[t'/x]$ by (<ref>).

If $d$ ends by (<ref>) we can write $s =\, \mathsf r\, \vec s$ and $s'= \, r(\vec s')$ s.t. $\mathsf r\, \vec s \reduces r(\vec s)$ is a $\mathsf r$-reduction and each $s_i \parred s_i'$.
By the inductive hypothesis we have that $s_i[t/x]\parred s_i' [t'/x]$.
We also have that $ \mathsf r\, \vec s[t/x] \reduces r(\vec s[t/x]) $ is an $\mathsf r$-reduction, where $r$ is variable-free (by inspection of the reduction rules).

Thus we have $s[t/x] = \, \mathsf r\, \vec s[t/x]\,  \parred \, r( \vec s'[t/x])\, = s'[t/x]$ by (<ref>).

(The argument when $d$ ends by (<ref>) is similar to that of (<ref>).)

If $d$ ends by (<ref>) we can write $s = s_0s_1$ and $s'=s_0's_1'$ s.t. $s_0 \parred s_0'$ and $s_1\parred s_1'$.
By the inductive hypothesis we have $s_0[t/x] \parred s_0'[t/x]$ and $s_1[t/x] \parred s_1'[t/x]$, whence $s[t/x] \parred s'[t/x]$ by (<ref>).

Notice that Proposition <ref> now follows immediately, by simply instantiating the Lemma above with $s = s'$ to deduce context-closure of $\parred$.

We can now turn to proving the required `diamond property' for $\parred$:

Suppose $t_0 \parder s \parred t_1$. Then there is some $u $ with $t_0 \parred u \parder t_1$.

Before giving the proof, it will be useful to have the following intermediate result:

Suppose $d: \, \mathsf r\, \vec s\, \parred \, t$, and there is no redex in $\mathsf r\, \vec s$ involving $\mathsf r$.
There are some $\vec t$ s.t. $t = \mathsf r\, \vec t$ and, for each $i$, some $d_i: \, s_i \parred t_i$ for some $d_i<d$.

We proceed by $\Sigma^0_1$-induction on the length of $\vec s$.
If $\vec s$ is empty, then only clause (<ref>) applies to $\mathsf r\, \vec s$, so we may set $\vec t$ empty too.

Suppose $\mathsf r\, \vec s\, s\, \parred t$, and there is no redex involving $\mathsf r$. Then only clause (<ref>) applies to $\mathsf r\, \vec s\, s$, so we have $t=t_0t_1$ and some $d_0 :\,  \mathsf r\, \vec s\, \parred t_0$ and $d_1: s \parred t_1$ with $d_0,d_1 < d$.
By inductive hypothesis there are $\vec t_0$ s.t. $t_0 \, =\,  \mathsf r\, \vec t_0$ and some $d_{0i} : s_i \parred t_{0i}$ with $d_{0i} < d_0$.
Thus we have $t\, = \, \mathsf r\, \vec t_0\, t_1$ and $d_{0i} : s_i \parred t_{0i}$ and $d_1: s \parred t_1$ with $d_{0i},d_1 < d$, as required.

We are now ready to prove the diamond property for $\parred$:

We proceed by simultaneous induction on the structure of the reductions $t \parred t_0$ and $t \parred t_1$.
Formally we show,

\[
\exists s' .\, ((d_0 : s\parred t_0\ \text{ and } \ d_1:s\parred t_1) \implies (t_0 \parred s' \text{ and } t_1 \parred s' ))
\]

by $\Sigma^0_1$-induction on $\min(|d_0|,  |d_1|)$.

* If $t_0 = s$ (i.e. $d_0$ is just (<ref>)) then we have $t_0 \parred t_1 \parder t_1$, by assumption and reflexivity, and we are done.

* Similarly if $t_1 = s$ (i.e. $d_1$ is just (<ref>)), so we may henceforth assume that $t_0 \neq t \neq t_1$, and $d_0$ and $d_1$ conclude with one of the clauses (<ref>),(<ref>) or (<ref>).

* If $d_0$ and $d_1$ both end by clause (<ref>), then we have $s = \mathsf r\, \vec s$ and $t_0 = r(\vec s_0)$ and $t_1 = r(\vec s_1)$, for some reduction step $\mathsf r\, \vec s \, \reduces\, r(\vec s)$ and some $\vec s_0 , \vec s_1$ s.t. $s_i \parred s_{0i}$ and $ s_i \parred s_{1i}$.
By the inductive hypothesis we have $\vec s'$ s.t. $s_{0i} \parred s_i'$ and $s_{1i} \parred s_i'$.
Thus by repeatedly applying Lemma <ref> we have $t_0 = r(\vec s_0) \parred r(\vec s')$ and $t_1 = r(\vec s_1)\parred r(\vec s')$, so we may set $s' = r(\vec s')$.

* (similarly if $d_0$ and $d_1$ end with clause (<ref>))

* (it is not possible for one to end with clause (<ref>) and the other to end by (<ref>), since in all cases precisely one reduction step applies at the head.)

* If $d_0$ ends by clause (<ref>) and $d_1$ ends by clause (<ref>), then from $d_0$ we have $\mathsf r, r$ s.t. $s\, = \, \mathsf r\, \vec s\, u \, \reduces r(\vec s, u)$ and some $\vec s_0,u_0$ with $s_i \parred s_{0i}$ and $u \parred u_0$ with $t_0 = r(\vec s_0,u_0)$.
From $d_1$ we further have some $t', u_1$ s.t. $t_1 = t'u_1$ and $\mathsf r\, \vec s\, \parred t'$ and $u \parred u_1$.
By Proposition <ref> we have some $\vec s_1$ s.t. $t'= \mathsf r\, \vec s_1$ and smaller derivations of $s_i \parred s_{1i}$.
By the inductive hypothesis we have $\vec s', u'$ s.t. $s_{0i} \parred s_i'\parder s_{1i}$ and $u_0 \parred u'\parder u_1$.
Thus, by repeatedly applying Lemma <ref> we have that $t_0 = r(\vec s_0, u_0) \parred r(\vec s',u')$, and by (<ref>) we have $t_1 = \mathsf r\, \vec s_1\, u_1\, \parred \, r(\vec s', u')$, so it suffices to set $t' = r(\vec s',u')$.

* (the case when $d_0$ ends by clause (<ref>) and $d_1$ ends by clause (<ref>) is symmetric to the one above)

* If both $d_0$ and $d_1$ end by clause (<ref>), then we have $s = s_0s_1$, $t_0 = r_0 r_1$, $t_1 = u_0u_1$ s.t. $r_0 \parder s_0 \parred u_0$ and $r_1 \parder s_1 \parred u_1$.
By inductive hypothesis we have $s_0'$ and $s_1'$ s.t. $r_0\parred s_0' \parder u_0$ and $r_1 \parred s_1'\parder u_1$.
Thus we have that $t_0 = r_0r_1 \parred s_0's_1'\parder u_0u_1$ by (<ref>), so we may set $s'= s_0's_1'$.

If $t_0 \parder^m t \parred^n t_1$ then there is some $t'$ with $t_0 \parred^n t' \parder^m t_1$.

We show,

\[
(d_0 : t \parred^m  t_0  \text{ and } d_1 : t\parred^n t_1) \, \implies \, \exists t'  ( t_0 \parred^n t' \, \text{ and } \, d_1': t_1 \parred^m t' )
\]

by $\Sigma^0_1$-induction on $ m = |d_0|$.

* If $m = 0$ then $t_0 =t$ and we may simply set $t' = t_1$, whence we have that $t_0 = t \parred^n t'$ by assumption and $t' = t_1\parder^0 t_1$.

* Now, suppose $t_0 \parder t_0' \parder^m t \parred^n t_1$. By the inductive hypothesis we have that

$$t_0' \parred^n t'' \parder^m t_1$$
for some $t_1'$. This means in particular that $t_0 \parder t_0' \parred^n t_1'$, so we have again from the inductive hypothesis a $t' $ with

$$t_0 \parred^n t' \parder t_1'$$

Putting these together we indeed have $t_0 \parred^n t' \parder^{m+1} t_1$, as required.

The following corollary is immediate:

If $t_0 \parder^* t \parred^* t_1$ then there is $t'$ s.t. $t_0 \parred^* t' \parder^* t_1$.

We may finally conclude CR for $\reduces$:

Suppose $t_0 \unreduces^* s \reduces^* t_1$. Then, by Corollary <ref> we have $t_0 \parder^* s \parred^* t_1$.
By Corollary <ref> above, we have some $s' $ with $t_0 \parred^* s' \parder^* t_1$, whence $t_0\reduces^* s' \unreduces t_1$ by Corollary <ref> again.

From here we derive other properties:

We have the following:

*  (Peaks and valleys) $s\conv t $ if and only if $  \exists r.\, s\reduces^* r \unreduces^* t$.

*  (UN for $\reduces$) If $s_0 $ and $s_1$ are normal with $s_0 \unreduces^* t \reduces^* s_1$, then $s_0 = s_1$.

*  (UN for $\conv$) If $s_0 $ and $s_1$ are normal with $s_0 \conv t \conv s_1$, then $s_0= s_1$.

For (<ref>), the right-to-left implication is obvious, so we prove

the left-to-right implication by induction on the length of a derivation $s\conv t$.

The critical case is when we have $s\conv t' \reduces t$ (or equivalently $s \unreduces s' \conv t$).
By the inductive hypothesis we have some $r'$ s.t. $s \reduces^* r' \unreduces^* t'$.
This means that we have $r' \unreduces^* t' \reduces t$ so by confluence, Theorem <ref>, we have some $r $ s.t. $r' \reduces^* r \unreduces^* t$.

(<ref>) is immediate from Theorem <ref> and the definition of normal form.

(<ref>) is immediate from (<ref>), the definition of normal form and (<ref>).

§.§ Structure of finitely applied coderivations, constants and variables

Before presenting the main type structures of this section, let us take a moment to note that we have now proven enough to show that the set of s, under conversion, forms a model of $\T$ without induction and extensionality, even provably within $\RCA$.

We write $\FARC$ for the type structure of s, defined as follows:

* $\sigma^\FARC := \{ t: \sigma \ |\  \text{$t$ is a farc} \}$.

* $\mathsf r^\FARC$ is just $\mathsf r$, for each constant $\mathsf r$.

* $t \comp^\FARC s$ is just $ts$.

* $=^\FARC_\sigma$ is just $\conv_\sigma$.

All the structures we consider in this section will be substructures of $\FARC$ that are moreover closed under conversion.
Thus they will inherit the (quantifier-free) theory of $\FARC$, to which end the following result is naturally indispensable:

$\FARC$ is a model of $\T \setminus \{ \extensionality,\induction \}$.
I.e. each $\T$ term $t$ of type $\sigma $ is in $\sigma^\FARC$, and moreover $\FARC$ satisfies the axioms of Figures <ref>, <ref>, <ref>, <ref> and the axioms (<ref>) and (<ref>) of Figure <ref>.

For each $\T$ term $t$ of type $\sigma$ we have $t \in \sigma^\FARC$ simply by definition of a , so we continue to verify the axioms.

The axioms governing the constants,
i.e. those from Figures <ref>, <ref> and <ref>, follow immediately from the definitions of $\reduces$ and $\conv$, cf. Figure <ref>.

For the equality axioms from Figure <ref>:

* Reflexivity of $\conv$ follows by definition.

* For the Leibniz property, suppose that $t \conv t'$ and $r(t) \conv s(t)$.

Then we have $r(t)\conv r(t')$ and $s(t) \conv s(t')$ by closure of $\conv$ under contexts, and the fact that s have only finitely many redexes, so there are only finitely many occurrences of $t$ in $r(t)$ and $s(t)$ (cf. Corollary <ref>). Thus we have $r(t')\conv s(t') $ by transitivity of $\conv$.
By symmetry, we also have that if $r(t')\conv s(t') $ then $ r(t) \conv s(t) $, and so in general $\phi(t) \equiv \phi(t')$ for any formula $\phi$.

For the first two number-theoretic axioms from Figure <ref>:

* $\cnot \succ 0 \conv 0$ follows from confluence, in particular unique normal forms cf. Corollary <ref>: both $\succ 0 $ and $0$ are normal but are not identical.

* Suppose $\succ s \conv \succ t$, so $\succ s \reduces^* u\unreduces^* \succ t$, by Corollary <ref>.
Notice that no reduction rule has $\succ$ at the head, so by $\Sigma^0_1$ induction we can extract reduction sequences $s \reduces^* u' \unreduces^* t $ for some $u' $ with $u = \succ u'$. Thus indeed $s \conv t$.

§.§ Hereditarily total coterms under conversion

We are now ready to present the type structures that will allow us to obtain a simulation of $\nC n$ within $\nT{n+1}$.
The structure that we present in this subsection is essentially the hereditrarily recursive operations of finite type, but where we adopt s under conversion as the underlying model of computation, cf. Proposition <ref>.

We define the following sets of s:

* $\hr\nat := \{ t:\nat \  |\  \exists n \in \Nat. \ t \conv \numeral n \}$

* $\hr{\sigma \to \tau} := \{ t: \sigma \to \tau \ | \ \forall s \in \hr\sigma . \ t\, s\, \in \hr \tau \}$

We write $\hr n$ for the union of all $\hr{\sigma}$ with $\level (\sigma) \leq n$.

Note that it is immediate from the definition that each $\hr\sigma$ contains only closed s of type $\sigma$.

Notice that, by the confluence result of the previous subsection, namely by Corollary <ref>, if $t\conv \numeral n$ then $n\in \Nat $ is unique and in fact $t \reduces^* \numeral n$ (provably in $\RCA$).
In this way we can view every element of $\hr \nat$ as computing a unique natural number by means of reduction.

$\hr \nat$ is $\Sigma^0_1$, and
if $\level(\sigma) = n>0$ then $\hr\sigma$ is $\Pi^0_{n+1}$.

$\hr\nat$ is $\Sigma^0_{1}$ just since $\conv$ is $\Sigma^0_1$. Furthermore, expanding out the definition:

$$\hro{\sigma \to \tau}(t) \iff \forall s . (s \in \hro \sigma  \implies  t s \in \hro \tau)$$

We proceed by the induction on the structure of $\sigma$.

In the base case, when $\sigma = \tau = \nat$, we have that $\hro\sigma $ and $\hro\tau$ are $\Sigma^0_1$, and so $\hro{\sigma \to \tau}$ is indeed $\Pi^0_2$, as required.

For the inductive hypothesis, we have that $\hro\sigma$ and $\hro\tau$ are $\Pi_n$ and $\Pi_{n+1}$ respectively, and so again $\hro{\sigma\to \tau}$ is indeed $\Pi_{n+1}$.

Suppose $\level(\sigma)<n$ and $\level (\tau)\leq n$.
Then we have the following, provably in $\RCA$:

*  If $s \in \hr \sigma$ and $t \in \hr{\sigma \to \tau}$ then $ts \in \hr \tau$. ($\hr{}$ closed under application)

*  If $t \in \hr \tau$ and $t\conv t'$ then $t'\in \hr\tau$. ($\hr{}$ closed under conversion)

Note that provability within $\RCA$ above is non-uniform in $\sigma$ and $\tau$, i.e. $ \RCA$ proves the statements for each particular $\sigma$ and $\tau$.

(<ref>) is immediate from the definition of the sets $\hr{\sigma}$.
(<ref>) follows by (meta-level) induction on the structure of $\tau$:

* The base case, when $\tau = \nat$, follows from symmetry and transitivity of $\conv$.[Note here that it was important to take conversion, $\conv$, which is symmetric, rather than reduction, $\reduces^*$, for the definition of $\hr\nat$.]

* Suppose $\tau = \sigma \to \tau'$ and let $s \in \hro \sigma$. Since $t \conv t'$ we also have $t\, s \ \conv\  t' s$, by closure of $\conv$ under contexts, and so $t's \, \in \hro{\tau'}$, by the inductive hypothesis. Thus $t' \in \hro\tau$, as required.

These properties justify defining the following type structure:

We simply write $\hr{}$ for the type structure defined as follows:

* $\sigma^\hr{}$ is $\hr \sigma$.

* $\mathsf r^\hr{}$ is just $\mathsf r$ for each constant $\mathsf r$.

* $t\comp^\hr{} s$ is just $ts$.

* $=_\sigma^{\hr{}}$ is $\conv_\sigma$.

Ultimately we will show that this structure constitutes a model of $\C \setminus \extensionality$ (i.e. without extensionality).
In fact, in Section <ref> we will prove this within an appropriate theory of arithmetic, so that we may also extract terms of $\T$ that are equivalent under conversion.

Note that $\hr{}$ is a substructure of $\FARC$, in the model-theoretic sense, and so inherits its quantifier-free theory (over the respective domains).
The key feature of $\hr{}$ over $\FARC$ is that it satisfies induction, provably in $\RCA$ in the following sense:

Suppose $r(x)$ and $s(x)$ are s.
If $r(0) \conv s(0)$ and $\forall t \in \hr \nat. (r(t) \conv s(t) \implies r(\succ t) \conv s(\succ t))$, then $\forall t \in \hr \nat . r(t) \conv s(t)$.

This is essentially `forced' by the definition of $\hr\nat$, reducing the statement to induction in $\RCA$.