Computational expressivity of (circular) proofs with fixed points
Gianluca Curzi, Anupam Das
TL;DR
This paper investigates the computational power of proof systems with fixed points, showing they can represent the same complex functions as a strong subsystem of second-order arithmetic, and develops new models and reverse mathematics results.
Contribution
It establishes the equivalence in computational expressivity between muLJ and CmuLJ proof systems and $ ext{Pi}^1_2$-$ ext{CA}_0$, and introduces novel models and reverse mathematics techniques.
Findings
Both muLJ and CmuLJ represent the same class of provably total functions.
The proof systems capture functions provably total in $ ext{Pi}^1_2$-$ ext{CA}_0$.
New reverse mathematics results for the Knaster-Tarski fixed point theorem.
Abstract
We study the computational expressivity of proof systems with fixed point operators, within the 'proofs-as-programs' paradigm. We start with a calculus muLJ (due to Clairambault) that extends intuitionistic logic by least and greatest positive fixed points. Based in the sequent calculus, muLJ admits a standard extension to a 'circular' calculus CmuLJ. Our main result is that, perhaps surprisingly, both muLJ and CmuLJ represent the same first-order functions: those provably total in -, a subsystem of second-order arithmetic beyond the 'big five' of reverse mathematics and one of the strongest theories for which we have an ordinal analysis (due to Rathjen). This solves various questions in the literature on the computational strength of (circular) proof systems with fixed points. For the lower bound we give a realisability interpretation from an extension of…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, Reasoning, and Knowledge · Logic, programming, and type systems · Philosophy and Theoretical Science
Computational expressivity of (circular) proofs
with fixed points
Gianluca Curzi∗ and Anupam Das∗
∗University of Birmingham
Abstract.
We study the computational expressivity of proof systems with fixed point operators, within the ‘proofs-as-programs’ paradigm. We start with a calculus (due to Clairambault) that extends intuitionistic logic by least and greatest positive fixed points. Based in the sequent calculus, admits a standard extension to a ‘circular’ calculus .
Our main result is that, perhaps surprisingly, both and represent the same first-order functions: those provably total in , a subsystem of second-order arithmetic beyond the ‘big five’ of reverse mathematics and one of the strongest theories for which we have an ordinal analysis (due to Rathjen). This solves various questions in the literature on the computational strength of (circular) proof systems with fixed points.
For the lower bound we give a realisability interpretation from an extension of Peano Arithmetic by fixed points that has been shown to be arithmetically equivalent to (due to Möllerfeld). For the upper bound we construct a novel computability model in order to give a totality argument for circular proofs with fixed points. In fact we formalise this argument itself within in order to obtain the tight bounds we are after. Along the way we develop some novel reverse mathematics for the Knaster-Tarski fixed point theorem.
1. Introduction
Fixed points abound in mathematics and computer science. In logic we may enrich languages by ‘positive’ fixed points to perform (co)inductive reasoning, while in programming languages positive fixed points in type systems are used to represent (co)datatypes and carry out (co)recursion. In both settings the underlying systems may be construed as fragments of their second-order counterparts.
In this work we investigate the computational expressivity of type systems with least and greatest (positive) fixed points. We pay particular attention to circular proof systems, where typing derivations are possibly non-well-founded (but regular), equipped with an -regular ‘correctness criterion’ at the level of infinite branches. Such systems have their origins in modal fixed point logics, notably the seminal work of Niwinski and Walukiewicz [28]. Viewed as type systems under the ‘Curry-Howard’ correspondence, circular proofs have received significant attention in recent years, notably based in systems of linear logic [4, 16, 17, 3, 14, 13, 12] after foundational work on related finitary systems in [5, 2]. In these settings circular proofs are known to be (at least) as expressive as their finitary counterparts, but classifying the exact expressivity of both systems has remained an open problem. This motivates the main question of the present work:
Question 1**.**
What functions do (circular) proof systems with fixed points represent?
Circular type systems with fixed points were arguably pre-empted by foundational work of Clairambault [7], who introduced an extension of Gentzen’s sequent calculus for intuitionistic propositional logic by least and greatest positive fixed points. forms the starting point of our work and, using standard methods, admits an extension into a circular calculus, here called , whose computational content we also investigate.
In parallel lines of research, fixed points have historically received considerable attention within mathematical logic. The ordinal analysis of extensions of Peano Arithmetic () by inductive definitions has played a crucial role in giving proof theoretic treatments to (impredicative) second-order theories (see, e.g., [31]). More recently, inspired by Lubarsky’s work on ‘-definable sets’ [24], Möllerfeld has notably classified the proof theoretic strength of extensions of by general inductive definitions in [27].
In this work we somewhat bridge these two traditions, in computational logic and in mathematical logic, in order to answer our main question. In particular we apply proof theoretic and metamathematical techniques to show that both and represent just the functions provably recursive in the subsystem of second-order arithmetic. This theory is far beyond the ‘big five’ of reverse mathematics, and is among the strongest theories for which we have an ordinal analysis (see [30]). In contrast, the best known lower bound for before was Gödel’s , i.e. recursion up to [7].
Finally let us point out that our characterisation also applies to aforementioned (circular) systems of linear logic, namely and its circular counterpart, here called , from [5, 2, 4, 16, 17, 3, 14, 13, 12], by adapting structural proof theoretic interpretations between the systems. Again, the previously best known lower bounds for these systems were forms of (higher-order) primitive recursion, cf. [2, 15, 16]. Thus this work resolves our main Question 1.
1.1. Outline and contribution
The structure of our overall argument is visualised in Figure 1. (1) is a standard embedding of finitary proofs into circular proofs (Proposition 23). (2) reduces to its ‘negative fragment’, in particular free of greatest fixed points (), via a double negation translation (Proposition 26).
(3) is one of our main contributions: we build a higher-order computability model that interprets (Theorem 45), and moreover formalise this construction itself within to obtain our upper bound (Theorem 76). The domain of this model a priori is an (untyped) term extension of . It is important for logical complexity that we interpret fixed points semantically as bona fide fixed points, rather than via encoding into a second-order system. Along the way we must also establish some novel reverse mathematics of the Knaster-Tarski fixed point theorem (Theorem 72).
(4) is an intricate and nontrivial result established by Möllerfeld in [27], which we use as a ‘black box’. (5) is again a double negation translation and can be seen as a specialisation of the -conservativity of full second-order arithmetic over its intuitionistic counterpart (Theorem 82). (6) is our second main contribution: we provide a realisability interpretation from into (Theorem 89), morally by considerable specialisation of the analogous interpretation from into Girard-Reynolds’ system [19, 32]. Our domain of realisers is a (typed) term extension of (the negative fragment of ), which is itself interpretable within (Proposition 26).
Finally, the application of our results to characterise the representable functions of (circular) is given in Section 8 (Theorem 98).
1.2. Related work
Fixed points have been studied extensively in type systems for programming languages. In particular foundational work by Mendler in the late ’80s [25, 26] already cast inductive type systems as fragments of second-order ones such as Girard-Reynolds’ [19, 32]. Aside from works we have already mentioned, (a variant of) (5) has already been obtained by Tupailo in [38]. Berger and Tsuiki have also obtained a similar result to (6) in a related setting [6], for strictly positive fixed points.111Bound variables may never occur under the left of an arrow. Their interpretation of fixed points is more akin to that in our type structure than our realisability model.
Finally the structure of our argument, cf. Figure 1, is inspired by recent works in cyclic proof theory, notably [34, 10] for (cyclic) (fragments of) and [9, 11, 23] for (circular) (fragments of) Gödel’s system .
1.3. Notation
Throughout this work we employ standard rewriting theoretic notation. Namely for a relation , we denote by the reflexive and transitive closure of , and by the symmetric closure of .
We shall make use of (first-order) variables, written etc., and (second-order) variables, written etc. throughout. We shall use these both in the setting of type systems and arithmetic theories, as a convenient abuse of notation.
2. Simple types with fixed points: system
In this section we recall the system from [7, 8].222More precisely, we present the ‘strong’ version of from [8].
2.1. The sequent calculus
Pretypes, written etc., are generated by the following grammar:
[TABLE]
Free (second-order) variables of a pretype are defined as expected, construing and as binders:
- •
- •
- •
, for
- •
, for
A pretype is closed if it has no free variables (otherwise it is open).
Throughout this work we shall assume some standard conventions on variable binding, in particular that each occurrence of a binder and binds a variable distinct from all other binder occurrences in consideration. This avoids having to deal with variable renaming explicitly. We follow usual bracketing conventions, in particular writing, say, for .
Definition 2** (Types and polarity).**
Positive* and negative variables in a pretype are defined as expected:*
- •
* is positive in .*
- •
* is positive and negative in .*
- •
if are positive (negative) in then so are and (resp.), for and .
- •
if is negative (positive) in and is positive (resp., negative) in , then is positive (resp., negative) in .
A pretype is a type (or even formula) if, for any subexpression , is positive in . The notions of (type) context and substitution are defined as usual.
Remark 3** (Positivity vs strict positivity).**
Many authors require variables bound by fixed point operators to appear in strictly positive position, i.e. never under the left-scope of . Like Clairambault [7, 8] we do not impose this stronger requirement, requiring only positivity in the usual syntactic sense.
Definition 4** (System ).**
A cedent, written etc., is just a list of types. A sequent is an expression .333The symbol is, formally, just a syntactic delimiter, but the arrow notation is suggestive. The system is given by the rules of Figures 2, 3 and 4.444Colours may be ignored for now. The notions of derivation (or proof) are defined as usual. We write if is a derivation of the sequent .
Remark 5** (General identity and substitutions).**
Note that is equipped with a general identity rule, not only for atomic types. This has the apparently simple but useful consequence that typing derivations are closed under substitution of types for free variables, i.e. if in (with all occurrences of indicated), then also in for any type . Later, this will allow us to derive inductively general functors for fixed points in rather than including them natively; this will in turn become important later for verifying our realisability model for .
Remark 6** ( as a fragment of second-order logic).**
We may regard properly as a fragment of Girard-Reynolds System [19, 32], an extension of simple types to a second-order setting. In particular, (co)inductive types may be identified with second-order formulas by:
[TABLE]
The rules for fixed points in are essentially inherited from this encoding, modulo some constraints on proof search strategy. Later we shall use a different encoding of fixed point types into a second-order setting, namely in arithmetic, as bona fide fixed points, in order to better control logical complexity.
In proofs that follow, we shall frequently only consider the cases of least fixed points (-types) and not greatest fixed points (-types), appealing to ‘duality’ for the latter. The cases for should be deemed analogous. As we shall soon see, in Subsection 3.4, we can indeed reduce our consideration to -free types, without loss of generality in terms of representable functions.
Remark 7** (Why sequent calculus?).**
Using a sequent calculus as our underlying type system is by no means the only choice. However, since we shall soon consider non-wellfounded and circular typing derivations, it is important to have access to a well behaved notion of formula ancestry, in order to properly define the usual totality criterion that underlies them. This is why the sequent calculus is the formalism of choice in circular proof theory.
Remark 8** (Variations of the fixed point rules).**
It is common, e.g. for semantic considerations, to consider context-free (or ‘weak’) specialisations of the fixed point rules:555Note that we have simply omitted identity premisses, for legibility.
[TABLE]
In the presence of cut the ‘(co)iterator’ rules above are equivalent to those of , but since the computational model we presume is cut-reduction, as we shall soon see, it is not appropriate to take them as first-class citizens. However, when giving a semantics that interprets directly, e.g. as we do for the term calculi in Section 4, it is often simpler to work with the (co)iterators above.
In the remainder of this work we shall freely use (variations of) the versions above in proofs.
Definition 9** (Functors).**
Let and be (possibly open) types that are positive (and negative, respectively) in . For a proof we define and by simultaneous induction as follows:
- •
If then is just . Notice that it is never the case that , as can only occur negatively in .
- •
If and are or some then and are defined respectively as follows:
[TABLE]
- •
If and then we define and respectively as follows:
[TABLE]
- •
If and then we define and respectively as follows:
[TABLE]
- •
If and then we define and respectively as follows:
[TABLE]
- •
if and then we define and respectively as follows:
[TABLE]
where (resp., ) are obtained from the IH for (resp., ) under substitution of for (resp., ), cf. Remark 5.
- •
if and then we define and respectively as follows:
[TABLE]
where (resp., ) are obtained from the IH for (resp., ) under substitution of for (resp., ), cf. Remark 5.
Example 10** (Post-fixed point).**
*It is implicit in the rules of that may be seen as the least fixed point of , under a suitable semantics (e.g. later in Section 5). The rule indicates that it is a pre-fixed point, while the rule indicates that it is least among them. To see that it is also a post-fixed point
we may use a derivation that mimics standard textbook-style proofs of Knaster-Tarski:*
[TABLE]
*Dually, we can derive
as follows:*
[TABLE]
2.2. Computing with derivations
The underlying computational model for sequent calculi, with respect to the ‘proofs-as-programs’ paradigm, is cut-reduction. In our case this follows a standard set of cut-reduction rules for the calculus . For the fixed points, cut-reduction is inherited directly from the encoding of fixed points in system that induces our rules, cf. Remark 6. Following Baelde and Miller [5], we give self-contained cut-reductions here:
Definition 11** (Cut-reduction for fixed points).**
Cut-reduction* on -derivations, written , is the smallest relation on derivations including all the usual cut-reductions of 666As usual, we allow these reductions to be performed on sub-derivations. I.e. they are ‘context-closed’. and the cut-reduction in Figure 5 and its dual for greatest fixed points (see Appendix A).*
*When speaking of (subsets of) as a computational model, we always mean with respect to the relation . *
Definition 12** (Representability in ).**
We define the type of natural numbers as . We also define the numeral by induction on :
[TABLE]
We say that a (possibly partial) function is representable in if there is a -derivation s.t., for any , the derivation,
[TABLE]
reduces under to the numeral , whenever it is defined (otherwise it reduces to no numeral). In this case we say that represents in .
Example 13** (Native rules for natural number computation).**
‘Native’ rules for type in are given in Figure 6 . The corresponding ‘native’ cut-reductions, derivable using , are routine. Note that, from here we can recover the usual recursor of system , as shown formally by Clairambault [8].
2.3. Further examples
Example 14**.**
The least and greatest fixed point operators and allow us to encode inductive data (natural numbers, lists, etc) and coinductive data (streams, infinite trees, etc). We have already seen the encoding of natural numbers. The type of lists and streams (both over natural numbers) can be represented by, respectively, and . Figure 7, left-to-right, shows the encoding of the successor on natural numbers, the encoding of and (i.e., the empty list and the operation appending a natural number to a list). Figure 8 shows the encoding of a concatenation of a list and a stream into a stream (by recursion over the list with the invariant ).777Both examples were originally given for in [15].
3. A circular version of
In this section we shall develop a variation of that does not have rules for (co)iteration, but rather devolves such work to the proof structure. First, let us set up the basic system of rules we will work with:
Definition 15** ( ‘without (co)iteration’).**
Write for the system of all rules in Figures 2, 3 and 9 (but not 4).
3.1. ‘Non-wellfounded’ proofs over
‘Coderivations’ are generated coinductively by the rules of a system, dually to derivations that are generated inductively. I.e. they are possibly infinite proof trees generated by the rules of a system.
Definition 16** (Coderivations).**
*A (-)coderivation is a possibly infinite rooted tree (of height ) generated by the rules of . Formally, we identify with a prefix-closed subset of (i.e. a binary tree) where each node is labelled by an inference step from such that, whenever is labelled by a step
S_{1}$$\cdots$$S_{n}
, for , has children in labelled by steps with conclusions respectively.*
We say that a coderivation is regular (or circular) if it has only finitely many distinct sub-coderivations.
Let us point out that a regular coderivation can, of course, be represented as a finite labelled graph (possibly with cycles).
3.2. Computing with coderivations
Just like for usual derivations, the underlying notion of computation for coderivations is cut-reduction, and the notion of representability remains the same. However we must also adapt the theory of cut-reduction to the different fixed point rules of .
Definition 17** (Cut-reduction on coderivations).**
* is the smallest relation on -coderivations including all the usual cut-reductions of and the cut-reductions in Figure 10,888Again, we allow these reductions to be applied on sub-coderivations.. When speaking of (subsets of) coderivations as computational models, we typically mean with respect to .*
Example 18** (Decomposing the (co)iterators).**
The ‘(co)iterator’ rules of Figure 4 can be expressed by regular coderivations using only the unfolding rules for fixed points as follows:
[TABLE]
Here we mark with roots of identical coderivations, a convention that we shall continue to use throughout this work. Dually for the coiterator:
[TABLE]
Moreover, one can verify that this embedding gives rise to a bona fide simulation of by . We do not cover the details at this point, but make a stronger statement later in Proposition 23.
Example 19** (Functors and -expansion of identity).**
Thanks to the decomposition of (co)iterators above, we can derive ‘functors’ in , cf. Definition 9. This gives rise to an ‘-expansion’ of identity steps, reducing them to atomic form. The critical least fixed point case is:
[TABLE]
The case for the greatest fixed point is the same:
[TABLE]
Note that the coderivation above is ‘logic-independent’, and indeed this reduction is common in other circular systems for fixed point logics, such as the modal -calculus and (see, e.g., [4]).
3.3. A totality criterion
We shall adapt to our setting a well-known ‘termination criterion’ from non-wellfounded proof theory. First, let us recall some standard proof theoretic concepts about (co)derivations, similar to those in [4, 23, 9, 11].
Definition 20** (Ancestry).**
Fix a -coderivation . We say that a type occurrence is an immediate ancestor of a type occurrence in if they are types in a premiss and conclusion (respectively) of an inference step and, as typeset in Figure 2, Figure 3 and Figure 9, have the same colour. If and are in some {\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\Gamma} or {\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Delta}, then furthermore they must be in the same position in the list.
Being a binary relation, immediate ancestry forms a directed graph upon which our correctness criterion is built. Our criterion is essentially the same as that from [4], only for instead of .
Definition 21** (Threads and progress).**
A thread along (a branch of) is a maximal path in ’s graph of immediate ancestry. We say a thread is progressing if it is infinitely often principal and whose smallest infinitely often principal formula is either a -formula on the LHS or a -formula on the RHS. A coderivation is progressing if each of its infinite branches has a progressing thread.
We shall use several properties of (progressing) threads in Section 5 which are relatively standard, e.g. [15, 36].
Definition 22** (Circular system).**
* is the class of regular progressing -coderivations.*
Referencing Example 18, and for later use, we shall appeal to the notion of simulation for comparing models of computation in this work. Recalling that we construe as a model of computation under and as a model of computation under , we have:
Proposition 23** (Simulation).**
* simulates .*
Proof sketch.
Replace each instance of a (co)iterator by the corresponding regular coderivation in Example 18. Note that those coderivations are indeed progressing due to the progressing thread on along the unique infinite branch in the case of (dually for ). The statement follows by closure of under its rules. ∎
Example 24** (Revisiting natural number computation).**
Just like for , we give native rules for in , along with corresponding cut-reductions in Figure 11. We just show how to derive the conditional:
[TABLE]
As before, it is routine to show that these reductions are derivable using .
Now, specialising our simulation result to recursion on , we have the following regular coderivation for the recursor of system (at type ):
[TABLE]
Indeed it is immediate that contains circular versions of system from [9, 11, 23].
3.4. Reduction to the negative fragment
It is folklore that coinductive types can be eliminated using inductive types (possibly at the loss of strict positivity) using, say, a version of the Gödel-Gentzen negative translation, without affecting the class of representable functions (as long as is included as a primitive data type) (see, e.g., [1]). Indeed this translation can be designed to eliminate other ‘positive’ connectives too, in particular .999Note that the attribution of ‘positive’ or ‘negative’ to a connective is unrelated to that of positive or negative context.
The same trick does not quite work for coderivations since it introduces cuts globally that may break the progressing criterion in the limit of the translation. However a version of the Kolmogorov translation, more well behaved at the level of cut-free proof theory, is well suited for this purpose.
In this section we establish such a reduction from to its ‘negative’ fragment. Not only is this of self-contained interest, being more subtle than the analogous argument for (and type systems with (co)inductive data types), this will also greatly simplify reasoning about the representable functions of in what follows, in particular requiring fewer cases in arguments therein.
Definition 25** (Negative fragments).**
We define as the subsystem of using only (native) rules and cut-reductions over .101010In particular we insist that the native rules and cut-reductions for are used to avoid extraneous occurrences of and remain internal to the fragment. We define and similarly, only as subsystems of -coderivations and their cut-reductions.
The main result of this subsection is:
Proposition 26**.**
Any function on natural numbers representable in is also representable in .
Proof idea.
We give a bespoke combination of a Kolmogorov negative translation and a Friedman-Dragalin ‘-translation’ (setting ). We define the translations and from arbitrary types to types over as follows, where :
[TABLE]
The translation can be extended to coderivations by mapping every inference rule to a gadget preserving threads. ∎
3.5. Further examples
Example 27**.**
Figure 12 shows the encoding of a stream by a (not necessarily regular) coderivation.111111Indeed, the coderivation is regular just if the stream is a regular word. Figure 13 shows the circular presentation of the concatenation of a list and a stream into a stream discussed in Example 14. Note that, compared to the inductive encoding of this function, the circular one has a more ‘explicit’ computational meaning.
It is worth discussing how computation over streams is simulated in via the double negation translation illustrated in Proposition 26. The type of streams is translated into , for some appropriate translation of the type for natural numbers. Hence, computation over streams is simulated by computation over a type of the form . Note that this resembles (and embeds) the type for representing streams in system .
Example 28**.**
Figure 13* provides an example of regular coderivation. By contrast, the coderivation in Figure 12 is not necessarily regular, as there might be infinitely many distinct natural numbers in a stream. Both coderivations are progressing, as the red-thread contained in their only infinite branch progresses infinitely many times.*
4. Extensions to (un)typed term calculi
In light of the reduction to the negative fragment at the end of the previous section, we shall only consider types formed from henceforth.
4.1. From (co)derivations to (co)terms: rules as combinators
It will be convenient for us to extend our computational model from just (co)derivations to a larger class of untyped (co)terms. The main technical reason behind this is to allow the definition of a higher-order computability model necessary for our ultimate totality argument for . At the same time, we obtain a compressed notation for (co)derivations for notational convenience, and indeed carve out typed (conservative) extensions of the proof calculi thusfar considered.
In what follows, we use the metavariables etc. to vary over inference steps of and/or 121212I.e. instances of any inference rules in these systems.
Definition 29** ((Co)terms [11]).**
A coterm, written etc., is generated coinductively by the grammar:131313I.e. they are possibly infinite expressions (of depth ).
[TABLE]
A coterm is a term if it is a finite expression, i.e. generated inductively from the grammar above. If all steps in a (co)term are from a system , we may refer to it as a -(co)term.
Our notion of (co)term is untyped, in that an application may be formed regardless of any underlying typing.
(Co)terms will be equipped with a theory that (a) subsumes cut-reduction on (co)derivations; and (b) results in a computational model that is Turing complete. Before that, however, let us see how (co)derivations can be seen as (co)terms.
Definition 30** ((Co)derivations as (co)terms).**
We construe each coderivation as a coterm (and each derivation as a term) by identifying rule application with term application: if ends with an inference step with immediate sub-coderivations then is .
Given a set of (co)terms, the closure of , written , is the smallest set of coterms containing and closed under application, i.e. if then also .
Of course if is a derivation, then it is also a term. Of particular interest to us in this work will be the class , essentially finitary applications of progressing regular -coderivations.
Example 31** (Iterator coderivation as a regular coterm).**
*Recalling the decomposition of the iterator as a circular coderivation in Example 18, let us specialise to the variation
. by a regular coderivation, say , that, viewed as a coterm, satisfies the (syntactic) equation,*
[TABLE]
Note that above is indeed a regular coterm: it has only finitely many distinct sub-coterms.
4.2. Computational models: theories of (co)terms
Let us henceforth make the following abbreviations:141414We may omit types from subscripts when unimportant.
[TABLE]
[TABLE]
[TABLE]
for .
When referring to an arbitrary instance of a rule, the specification should be understood to be as originally typeset, unless otherwise indicated. In particular, we follow this convention to define our notion of reduction on coterms:
Definition 32** (Theories).**
We define two (context-closed) reduction relations on (co)terms:151515The use of both variables and term metavariables in these rules is purely to aid parsing. All rules are closed under substitution.
- •
* is generated by the clauses in Figures 14, 16 and 17.*
- •
* is generated by the rules in Figures 14, 15 and 18.*
When referring to (fragments of) as a computational model, we typically mean with respect to , and when referring to (fragments of) as a computational model, we typically mean with respect to . However we also consider a (weakly) extensional version of :161616This is not necessary to reason about representability, since extensionality can be eliminated for low type levels, but simplifies some of the theorem statements.
- •
* is the closure of under the rule *
.171717 here must be a (free) variable, not a (co)term.
Example 33** (Iteration equations).**
The fundamental equation for iteration is indeed derivable by :
[TABLE]
For , recalling Example 31 and using its notation, we can simulate the iteration equation for with :
[TABLE]
More importantly for us, our notion of extensional reduction on coterms subsumes that of cut-reduction on coderivations. Since we have identified coderivations as coterms, we may state this rather succinctly, constituting the main result of this subsection:
Theorem 34** (Extensional reduction includes cut-reduction).**
.
Proof.
We show that, if then, for some sufficiently large, and for any , . We then conclude by repeatedly applying the rule .
So, let . It suffices to consider the case where the last rule of is the cut rule rewritten by the cut-reduction step. Indeed, the latter implies the general statement by appealing to the contextual closure of . We only consider some relevant cases.
Suppose is the following coderivation:
[TABLE]
We have:
[TABLE]
Suppose now that is as follows:
[TABLE]
We have
[TABLE]
Notice that the case above is the one requiring a sufficiently large number of applications , as we crucially require an extra coterm to fire the reduction step .
Let us now suppose that is as follows:
[TABLE]
We have:
[TABLE]
∎
4.3. An embedding into -terms
While the significant technical development of this work involves ‘totality’ arguments, e.g. in Section 5 showing that the representable partial functions of (under ) are total, we better address determinism too.
As it stands, can fire distinct reductions on the same or overlapping redexes, so there is a priori no guarantee that the output of representable functions is unique. However this can be shown by defining a straightfoward interpretation of coterms of into the (untyped) -calculus. We shall prove that the (untyped) -calculus, under -reduction, simulates under . This simulation relies on the fact that we can express regular coterms as a finite system of equations, which are known to always have solutions in the (untyped) -calculus.
-terms, written etc., are generated as usual by:
[TABLE]
We write for the set of all terms. For this (and later) notion(s) of term we follow usual bracketing conventions, e.g. writing instead of . The notion of ‘free variable’ is defined as expected.
To define our type structures later we will need to work with a standard equational theory on -terms. is the smallest congruence on satisfying:
[TABLE]
Figure 19 displays some macros for -terms (and the corresponding reduction rules) we will adopt in this subsection.
We define an interpretation of coterms in into . We start with an interpretation of terms (i.e., the finite coterms).
Definition 35** (Interpreting terms of ).**
To each rule of we associate a -term as shown in Figure 20. We extend to terms (i.e., finite coterms) by setting .
It is easy to check that this interpretation faithfully preserves the equations given in Figure 14, 15, and 18.
Lemma 36**.**
The following equations hold in for any :
[TABLE]
Also, if then by using -reduction.
We now show how to define for general coterms in . First, we show that any such coterm can be described by a finite system of simultaneous equations.
Lemma 37**.**
Let . There exist a system of simultaneous equations:
[TABLE]
such that:
- •
* are (term) variables and are (finite) terms that contain free variables in .*
- •
If then .
Proof.
Follows from the fact that is essentially obtained by finite applications of regular coterms, so has finitely many distinct coterms. ∎
Now, let . By the above Lemma there is a system of simultaneous equations . Since are finite terms, we have -terms . Then, we consider the following system of equations in :
[TABLE]
Now we may set , where are solutions (respectively) of the above system of simultaneous equations181818These solutions always exist (see, e.g., [18]) but are not necessarily unique.
By putting everything together, we have:
Proposition 38**.**
If and then .
Proof.
Straightforward by Lemma 36 and Proposition 37. ∎
From here, by confluence of -reduction on -terms, we immediately have:
Corollary 39** (Uniqueness).**
Let . If then .
Proof.
Clearly, by Proposition 38 we have and . Since , we have and . Since and are normal forms, by confluence of it must be that , and hence . ∎
4.4. From typed terms back to proofs
Let us restrict our attention to -terms in this subsection. In what follows, for a list of types , we write for . In order to more easily carry out our realisability argument in Section 7, it will be convenient to work with a typed version of :
Definition 40** (Type assignment).**
Type assignment* is the smallest (infix) relation ‘’ from terms to types satisfying:*
- •
*for each step *
\vec{\sigma}_{1}\Rightarrow\tau_{1}$$\cdots$$\vec{\sigma}_{n}\Rightarrow\tau_{n}
-
we have .*
- •
if and then .
- •
if and then .
- •
if , and positive in , then .
We write for the class of typed -terms.
Naturally, by inspection of the reduction rules of , we have ‘subject reduction’:
Proposition 41** (Type preservation).**
If and then .
Proof.
It suffices to consider the case where the reduction fires the outermost redex, as this allows us to conclude by appealing to contextual closure for . This boils down to checking that the reductions in Figure 14, Figure 16 and Figure 17 preserve types. The first group of reduction rules is routine, while the third one is derivable, so we will focus on the reduction rules in Figure 16.
Suppose This means that , , , and . Since , . Putting everything together, .
Clearly, , with and . So . Hence, .
Suppose . Then, and . So, .
Last, suppose . Then, and . This means that , and so . Therefore, . ∎
The main result of this subsection is:
Theorem 42** (Terms to derivations).**
* and represent the same natural number functions.*
Proof.
First, given a derivation of in , we define the derivation of as follows:
[TABLE]
We now define an interpretation of typing derivations into (possibly open) derivations of by induction on as follows:
- •
For each step , is the derivation of in :
[TABLE]
- •
if is inferred from and then is
[TABLE]
- •
if is inferred from and then we define as follows:
[TABLE]
- •
if is inferred from then, by induction hypothesis, we have a derivation of , and so we have a derivation of . We define by applying a cut rule to the followiing derivations:
[TABLE]
[TABLE]
where the substitution of for in is justified by Remark 5.
To show that typed- and represent the same functions on natural numbers, it suffices to prove that if and then for some . Notice that a type assignment derivation exists by Proposition 41. This requires to consider the case where the reduction fires the outermost redex, as this allows us to conclude by appealing to contextual closure for . This boils down to checking that the reductions in Figure 14, Figure 16 and Figure 17 are simulated by a series of cut-reduction rules on , which is routine.
∎
5. Totality of circular proofs
In this section we provide a semantics for (circular) proofs, using higher-order computability theoretic tools. Our aim is to show that represents only total functions on (Corollary 46), by carefully extending circular proof theoretic techniques to our semantics.
Throughout this section we shall only consider types formed from , unless otherwise indicated.
5.1. A type structure of regular coterms
We shall define a type structure whose domain will be contained within . Before that, it will be convenient to have access to a notion of a ‘good’ set of terms.
A (totality) candidate is some that is closed under . We henceforth expand our language of types by including each candidate as a type constant.
An immediate albeit powerful observation is that the class of candidates forms a complete lattice under set inclusion. This justifies the following definition of our type structure:
Definition 43** (Type structure).**
For each type we define by:
[TABLE]
We write for the function on candidates .
As we shall see, the interpretation of -types above is indeed a least fixed point of the corresponding operation on candidates.
A natural, but important, property is:
Proposition 44** (Closure under conversion).**
If and then .
Let us point out that this immediately entails, by contraposition and symmetry of , closure of non-elementhood of the type structure under conversion: if and then also . This simple observation is important is critical for our main totality argument, which proceeds by contradiction.
The main result of this section is:
Theorem 45** (Interpretation).**
For any -coderivation and we have .
The rest of this section is devoted to proving this result, but before that let us state our desired consequence:
Corollary 46**.**
* represents only total functions on with respect to .*
Proof idea.
Consider a -coderivation . By the Interpretation Theorem 45 and closure under conversion, Proposition 44 (namely applying -reductions), we have for all there is with . ∎
5.2. Montonicity and transfinite types
To prove our main Interpretation Theorem, we shall need to appeal to a lot of background theory on fixed point theorems, ordinals and approximants, fixed point formulas, and cyclic proof theory. In fact we will go on to formalise this argument within fragments of second-order arithmetic.
At this point it is pertinent to observe that the positivity constraint we impose for fixed point types indeed corresponds to monotonicity of the induced operation on candidates with respect to our type structure:
Lemma 47** (Monotonicity).**
Let be candidates.
- (1)
If is positive in then ; 2. (2)
If is negative in then .
These properties are proved (simultaneously) by a straightforward induction on the structure of . Note that, by the Knaster-Tarski fixed point theorem this yields:
Proposition 48** (“Fixed points” are fixed points).**
* is the least fixed point of on candidates.*
We will need to appeal to an alternative characterisation of fixed points via an inflationary construction, yielding a notion of ‘approximant’ that:
- (a)
allows us to prove the Interpretation Theorem by reduction to well-foundedness of approximants (or, rather, the ordinals that index them); and 2. (b)
allows a logically simpler formalisation within second-order arithmetic, cf. Section 6, crucial for obtaining a tight bound on representable functions,
Definition 49** (Approximants).**
Let be a monotone operation on candidates, with respect to . For ordinals we define by transfinite induction on :191919In fact, for our purposes we will only need the special case of the definition when .
- •
**
- •
**
- •
, when is a limit ordinal.
Writing for the class of all ordinals, the following is well known:
Proposition 50** (Fixed points via approximants).**
Let be the least fixed point of a monotone operation . We have .
From here it is convenient to admit formal type expressions representing approximants. We henceforth expand the language of types to be closed under:202020Again we shall only need the special case of for our purposes.
- •
for positive in , an ordinal, is a type.
Definition 51** (Type structure, continued).**
We duly expand Definition 43 to account for transfinite types by setting .
We have immediately from Proposition 50:
Corollary 52**.**
.
5.3. Ordinal assignments
We shall write if is a subformula of .
The Fischer-Ladner (well) preorder, written , is the smallest extension of satisfying . We write if . Note that -equivalence classes are naturally (well) partially ordered by .
The Fischer-Ladner closure of a type , written , is the set . Note that is the smallest set of types closed under subformulas and, whenever , then also ; this is necessarily a finite set.
Definition 53** (Priority).**
We say that a type has higher priority than a type , written , if or and . (I.e. .)
Note that is a (strict) well partial order on types. Intuitively, if has higher priority than , in a usual sense of fixed point logics, e.g., [36, 15, 39]
In what follows, we shall assume an arbitrary extension of to a total well order.
Let be a type whose -greatest fixed point subformula occurring in positive position is . We write for , i.e. with each occurrence of in positive position replaced by . is defined the same way by for the -greatest fixed point subformula occurring in negative position.
Note that, if has fixed point subformulas in positive position and then is a -free (transfinite) type. Similarly for negatively occurring fixed points. We shall call such sequences (positive or negative) assignments (respectively).
We shall order assignments by a lexicographical product order, i.e. by setting when there is some with but for all .212121Note that this renders the order type of simply , but it will be easier to explicitly work with the lexicographical order on ordinal sequences.
By the Monotonicity Lemma 47 we have:
Proposition 54** (Positive and negative approximants).**
If there are (least) ordinal(s) s.t. .
Dually, if there are (least) ordinal(s) s.t. .
5.4. Reflecting non-totality in rules of
Before giving our non-total branch construction, let us first make a local definition that will facilitate our construction:
Definition 55** (Reflecting non-totality).**
Fix a -step,
[TABLE]
for some and regular coderivations .
For s.t. , we can define a premiss and and some inputs such that
We give here the important cases:
- •
*If is *
\Sigma_{0}\Rightarrow\tau_{0}$$\Sigma_{1}\Rightarrow\tau_{1}
and ,*
[TABLE]
for some , so we set , , .
- •
*If is *
-
and and :*
[TABLE]
Now, by definition of we have indeed for , so we set , and .
- •
*If is *
and ,*
[TABLE]
so we set , and and .
- •
*If is *
\Gamma\Rightarrow\rho$$\Delta,\sigma\Rightarrow\tau
let and . Like before, let be the least assignment such that . We have two cases:*
- –
if then we set , and and .
- –
otherwise and we have:
[TABLE]
Since and we have so we set , and and .
- •
*If is *
and ,*
[TABLE]
so we set , and .
- •
*if is *
and and we have:*
[TABLE]
Since then also by Proposition 48, so we set , and and .
The cases for the Definition above are particularly subtle, requiring consideration of least ordinal assignments similar to the handling of -left in fixed point modal logics, cf. e.g. [28].
5.5. Non-total branch construction
From here the proof of the Interpretation Theorem 45 proceeds by contradiction, as is usual in cyclic proof theory. The Definition above is used to construct an infinite ‘non-total’ branch, along which there must be a progressing thread. We assign ordinals approximating the critical fixed point formula and positive formulas of higher priority, which must always be present as positive subformulas along the thread.222222Positive here with respect to the LHS, i.e. negative if on the RHS. Tracking the Definition above, we note that this ordinal assignment sequence is non-increasing; moreover at any step on the critical fixed point, the corresponding ordinal must be a successor and strictly decreases. Thus the ordinal sequence does not converge, yielding a contradiction.
Proof of theorem 45.
Let and be as in the statement, and suppose for contradiction that Setting and , we use Definition 55 to construct an infinite branch and associated inputs by always setting , and .
Now let be a progressing thread along , since is progressing, and let be the corresponding input, for , when is on the LHS.
Since is progressing, let enumerate the fixed points occurring in every positively in the LHS, and negatively in the RHS.232323This is because we have necessarily , and so the thread must eventually stabilise within some Fischer-Ladner class. Of course, no inference step changes polarity of the subformulas occurring on the same side. Note that, by definition is infinitely often principal and, WLoG, no , for , is principal along .
By Proposition 54, let , for , be the least assignments such that:
- •
if is on the LHS then ;
- •
if is on the RHS then .
We claim that is a monotone non-increasing sequence of ordinal assignments that does not converge:
- •
By construction of and , appealing to Definition 55, note that for each rule for which is not principal (along on the LHS) we have that . Note in particular that the -cases of Definition 55 are designed to guarantee at -steps.
- •
Now, consider a -step along the progressing thread on the critical fixed point formula,
[TABLE]
with . Writing (a prefix of ) we have:
[TABLE]
for some since must be a successor ordinal.242424An element must enter a fixed point for the first time at a successor ordinal, since a limit approximant is just the union of smaller approximants. Thus indeed .
This contradicts the well-foundedness of ordinals. ∎
6. Some reverse mathematics of Knaster-Tarski
In order to obtain sub-recursive upper bounds on the functions represented by , we will need to formalise the totality argument of the previous section itself within fragments of ‘second-order’ arithmetic. To this end we will need to formalise some of the reverse mathematics about fixed point theorems on which our type structure relies.
First let us note that we have an analogue of ‘functoriality’ in predicate logic, by structural induction on positive formulas:
Lemma 56** (Monotonicity).**
Let be positive in .
[TABLE]
In what follows this will often facilitate arguments by allowing a form of ‘deep inference’ reasoning.
6.1. Language and theories of ‘second-order’ arithmetic
Let us recall , the language of ‘second-order’ arithmetic, e.g. as given in [35]. It extends the language of arithmetic by:
- •
an additional sort of sets, whose variables are written etc. Individuals of are considered of number sort.
- •
an elementhood (or application) relation relating the number sort to the set sort. I.e. there are formulas (also ) when is a number term and is a set variable. (We will not consider any non-variable set terms here.)
When speaking about the ‘free variables’ of a formula, we always include set variables as well as individual variables.
We shall assume a De Morgan basis of connectives, namely with negation only on atomic formulas. Hence, we say that a formula is positive (or negative) in if no (every, resp.) subformula occurs under a negation.
We shall work with subtheories of full second-order arithmetic () such as etc., whose definitions may be found in standard textbooks, e.g. [35]. We shall freely use basic facts about them.
Proposition 57** (Some basic reverse mathematics, e.g. [35]).**
We have the following:
- (1)
** 2. (2)
* (arithmetical transfinite recursion).* 3. (3)
* (axiom of choice)*
A simple consequence of -choice in is that (and ) is provably closed under positive (resp. ) combinations (even with and parameters). We shall actually need a refinement of this fact to take account of polarity, so we better state it here. First let us set up some notation.
Definition 58** (Polarised analytical hierarchy).**
We write for the class of formulas positive in and negative in . Similarly for . is , in a theory , if it is -provably equivalent to both a -formula and a -formula.
Lemma 59** (Polarised substitution lemma, ).**
If and then . Similarly for in place of .
Proof idea.
By induction on the structure of , using at each alternation of a FO and SO quantifier. ∎
Note that the Lemma above, in particular, allows for arbitrary substitutions of and formulas free of , which we shall rely on implicitly in the sequel.
6.2. Countable orders
We can develop a basic theory of (countable) ordinals in even weak second-order theories, as has been done in [35] and also comprehensively surveyed in [21]. Let us point out that, while distinctions between natural notions of ‘order comparison’ are pertinent for weak theories, the theories we mainly consider contain , for which order comparison is robust.
A (countable) binary relation is a pair where and are sets, the latter construed as ranging over pairs. (Sometimes we write to specify this.) We say that is a partial order, written , if:
- •
- •
- •
is a total order, written , if it is a partial order that is total:
- •
Given a relation , we may write for its strict version, given by
[TABLE]
We employ similar notational conventions for other similar order-theoretic binary symbols.
We say that a binary relation is well-founded, written , if:
- •
is a well-order, written , if it is a well-founded total order, i.e.:
[TABLE]
Henceforth we shall write etc. to range over countable binary relations. If we may write , and similarly for . We may also write simply instead of , as abuse of notation.
It is not hard to see that admits an induction principle over any provable well-order (see, e.g., [35]):
Fact 60** (Transfinite induction, ).**
If then:
[TABLE]
In fact, in extensions of , we even have (transfinite) induction on arithmetical formulas, a fact that we shall use implicitly in what follows. For instance, in , we may admit (transfinite) induction on arithmetical combinations of formulas.
6.3. Comparing orders
Following Simpson in [35], given we write if there is an order-isomorphism from onto a proper initial segment of . We also write if and are order-isomorphic, and if . Thanks to the uniqueness of comparison maps, we crucially have
Proposition 61** ().**
* are .*
We shall now state a number of well-known facts about comparison, all of which may be found in, e.g., [35] or [21].252525Note that we have intentionally refrained from specifying the ‘optimal’ theories for each statement, for simplicity of exposition
Proposition 62** (Facts about ordinal comparison, ).**
Let be well-orders. We have the following:
- (1)
(Comparison is a preorder)
- (a)
** 2. (b)
** 2. (2)
(Comparison is pseudo-antisymmetric) If then . 3. (3)
(Comparison is total) 4. (4)
(Comparison is well-founded)
We shall assume basic ordinal existence principles, in particular constructions for successor (), addition () and maximum (, initial segments ( for ), all definable and satisfying characteristic properties provably in . We shall also make crucial use of a ‘bounding’ principle:
Proposition 63** (-Bounding, ).**
Let with . Then .
When appealing to Bounding, we use notation such as for an ordinal bounding all such that .
6.4. Knaster-Tarski theorem and approximants
Throughout this section let . We shall typically ignore/suppress the parameters , focussing primarily on and , and sometimes even write instead of . We shall work within unless otherwise stated.
Remark 64** (Reverse mathematics of fixed point theorems).**
Let us point out that, while previous work on the reverse mathematics of fixed point theorems exist in the literature, e.g. [29], even for the Knaster-Tarski theorem [33], these results apply to situations when the lattice or space at hand is countable (a subset of ). Here we require a version of the theorem where sets themselves are elements of the lattice, under inclusion. Our operators are specified non-uniformly, namely via positive formulas. This amounts to a sort of non-uniform ‘3rd order reverse mathematics’ of Knaster-Tarski, peculiar to the powerset lattice on .
While we can define (bounded) approximants along any well-order simply by appeal to , it will be helpful to retain the well-order (and other free set variables) as a parameter of an explicit formula to be bound later in comprehension instances, and so we give the constructions explicitly here.
Definition 65** ((Bounded) approximants).**
If and we write (or even ) for:
[TABLE]
We also write,
[TABLE]
sometimes written simply and resp.
Proposition 66**.**
If then is . In particular, is equivalent to:
[TABLE]
Proof.
As written is a positive combination of , so it is certainly by Lemma 59. So it suffices to prove the ‘in particular’ clause, since (4) is already a positive combination of .
For this we note that we can ‘merge’ the two definitions into an instance of , obtaining (after -comprehension) some satisfying for all and :
[TABLE]
Now we show that in fact . For the right-left implication, we simply witness the quantifier in the definition of by . For the left-right implication, let such that:
[TABLE]
We show by -induction on :
[TABLE]
We may prove similarly, concluding the proof. ∎
Eventually we will also show that too, but we shall need to prove the fixed point theorem first, in order to appeal to a duality property. First let us note a consequence of the above proposition:
Corollary 67** ((Bounded) recursion).**
Suppose .
- (1)
(Bounded recursion) . I.e.
[TABLE] 2. (2)
(Recursion) , i.e.
[TABLE]
Proof.
1 immediately from the equivalence between and satisfying (5) in the previous proof.
For 2 we first need an intermediate result. For , let us write for the initial segment of up to (and including) . We show,
[TABLE]
by transfinite induction on . We have:
[TABLE]
Now, turning back to 2, we have:
[TABLE]
∎
Proposition 68** ((Bounded) approximants are inflationary).**
Let . We have the following:
- (1)
** 2. (2)
**
Proof.
1 follows directly from Bounded Recursion:
[TABLE]
2 follows directly from Recursion:
[TABLE]
∎
Definition 69** (Least (pre)fixed points).**
Define (or even ) by:
[TABLE]
Note that we may treat as a set in since , and so is . By mimicking a text-book proof of the Knaster-Tarski theorem we obtain:
Proposition 70** (‘Knaster-Tarski’).**
, i.e.
[TABLE]
Proof.
For , note that for any with we have:
[TABLE]
Thus , and so indeed .
For , we have:
[TABLE]
∎
Lemma 71** (Closure ordinals).**
. I.e.
[TABLE]
Proof sketch.
We have:
[TABLE]
where is obtained by Bounding,272727To be precise, we apply bounding on the formula . Proposition 63, such that . ∎
The main result of this subsection is:
Theorem 72** (LFP dual characterisation).**
, i.e.:
[TABLE]
Proof.
For the left-right inclusion, , we show that is a pre-fixed point of , i.e.:
[TABLE]
By Lemma 71 let such that . We have:
[TABLE]
Since we have access to as a set, under , this indeed yields .
For the right-left inclusion, , let and we show:
[TABLE]
by transfinite induction on . For logical complexity, recall that we indeed have access to as a set, since so . We have:
[TABLE]
∎
One of the main consequences of the Characterisation Theorem is:
Corollary 73** ().**
* is .*
Let us point out that the above result amounts to a partial arithmetisation of purely descriptive characterisation of -definable sets in Lubarsky’s work [24].
6.5. Arithmetising the totality argument
Thanks to the results of this section, we may duly formalise the type structure from Section 5 within and prove basic properties.
Throughout this section we shall identify terms with their codes. In the case of and subsystems, we note that terms may still be specified finitely thanks to regularity of coderivations in , and that syntactic equality is verifiable already in between different representations [9, 11]. Let us also note that the various notions of reduction, in particular and are relations on terms.282828Note here that it is convenient that is formulated using only the extensionality rule, rather than being fully extensional.
Let us recall the structure from earlier from Section 5. Note that, as written in Definition 43, these sets, a priori, climb up the analytical hierarchy due to alternation of and . This is where the results of the previous section come into play and serve to adequately control the logical complexity of .
Definition 74** (Type structure, formalised).**
We define the following second-order formulas:
- •
**
- •
**
- •
**
- •
**
- •
**
Weak theories such as are able to verify closure of under conversion by a syntax analysis (see [11]). That each itself is closed under conversion, cf. 44, is also available already in by (meta-level) induction on the structure of . More importantly, and critically, we have as a consequence of the previous section:
Corollary 75**.**
Let be positive in and negative in . is -provably .
Proof sketch.
We proceed by induction on the structure of , for which the critical case is when has the form . By definition is positive in , and so by IH . We conclude by Corollary 73. ∎
Now, recall that a function is provably recursive in a theory if there is a -formula with:
- •
if and only if ; and,
- •
.
We may formalise the entire totality argument within , in a similar fashion to analogous arguments in [11, 23, 9], only peculiarised to the current setting. This requires some bespoke arithmetical arguments and properties of our type structure. As a consequence we obtain:
Theorem 76**.**
Any -representable function on natural numbers is provably recursive in .
We give some more details for establishing the above theorem. In particular, we apply the fixed point theorems within second-order arithmetic in Section 6 to arithmetise the totality argument in Section 5 within . We shall focus on explaining at a high level the important aspects of the formalisation, broadly following the structure of Section 5.
Notice that it will not actually be possible to prove the Interpretation Theorem 45 uniformly, due to Gödelian issues. Instead we will demonstrate a non-uniform version of it:
Theorem 77** (Nonuniform Interpretation, formalised).**
Let . Then .
Note that, from Theorem 77 above, Theorem 76 will follow directly via a version of Corollary 46 internal to . In particular, when contains only s and is , note that the statement of Theorem 77, , is indeed .
Let us now fix for the remainder of this section.
Formalising monotonicity and transfinite types
All the technology built up in Subsection 5.2 has been appropriately formalised in the previous Section 6.
Formalising closures and priorities
All the notions about closures and priorities in the totality argument involve only finitary combinatorics and are readily formalised within .
Formalising ordinal assignments
We define ordinal assignments within relative to some varying over . What is important is to establish the ‘positive and negative approximants’ Proposition 54. However this follows directly from the Closure Ordinal Lemma 71 and the Monotonicity Lemma 56.
Formalising reflection of non-totality.
Since has only finitely many distinct lines, and so only finitely many distinct formulas, we will need to consider only finitely many distinct henceforth which we combine to describe to establish the reflection of non-totality Definition 55 all at once within SO arithmetic. Working in , let us point out that the description of from 292929We assume here that are sub-coderivations of the we fixed earlier. is recursive in the following oracles:
- •
, for each occurring in , which is by Corollary 75; and,
- •
finding the least such that ; this is by fixing the closure ordinal, cf. 71, say of , and searching for the least appropriate instead; again this is ;
- •
finding an inhabitant of some nonempty , for which we can simply take the ‘least’ (seen as a natural number coding it), and so is .
Consequently we have that Definition 55, the description of from , is indeed a -provably formula in .
Formalising the non-total branch construction
The ‘non-total’ branch constructed in the proof of the Interpretation Theorem 45 is recursive in the ‘reflecting non-totality’ definition, and so we have access to it as a set within .
One subtlety at this point is that needs to ‘know’ that is indeed progressing. However earlier work on the cyclic proof theory of arithmetic [34, 10], building on the reverse mathematics of -automaton theory [22], means that this poses us no problem at all:
Proposition 78** (Formalised cyclic proof checking [10]).**
* proves that is progressing, i.e. that every infinite branch has a progressing thread.*
From here we readily have that there is a progressing thread and inputs along along the non-total branch. The assignment of ordinals along the branch follows by the ‘positive and negative approximants’ result. The verification that for non-critical steps follows by inspection of the ‘reflecting non-totality’ definition. Finally, for the critical fixed point unfolding, we need that is a successor. For this we need that the approximant at a limit ordinal is a union of smaller approximants, for which we use Recursion, cf. Corollary 67.
This concludes the proof of Theorem 77, and so also of Theorem 76.
7. Realisability with fixed points
So far we have shown an upper bound on the representable functions of and , namely that they are all provably recursive in . In this section we turn our attention to proving the analogous lower bound, namely by giving a realisability interpretation into (in fact typed-) from a theory over which is conservative.
In particular, we consider a version of first-order arithmetic, , with native fixed point operators, (essentially) introduced by Möllerfeld in [27]. Unlike that work, we shall formulate in a purely first-order fashion in order to facilitate the ultimate realisability interpretation.
7.1. Language of arithmetic with fixed points
We consider an extension of whose language is closed under (parameterised) least (and greatest) fixed points.
Let us extend the language of arithmetic by countably many predicate symbols, written etc., that we shall refer to as ‘set variables’. In this way we shall identify -formulas with the arithmetical formulas of the language of second-order arithmetic , but we shall remain in the first-order setting for self-containment. As such, when referring to the ‘free variables’ of a formula, we include both set variables and number variables.
-formulas are generated just like -formulas with the additional clause:
- •
if is a formula with free variables , and in which occurs positively, and is a (number) term with free variables then (sometimes ) is a formula with free variables .
We also write for , a suggestive notation witnessing the De Morgan duality between and (in classical logic).
Remark 79** ( as a proper extension of ).**
Again referring to the identification of formulas with arithmetical formulas, we may construe as a formal extension of by certain relation symbols. Namely may be identified with the closure of under:
- •
if is an arithmetical formula with free variables among , and in which occurs positively, then there is a relation symbol taking set inputs and number inputs.
In this case, for arithmetical , we simply write, say, instead of . Let us note that this is indeed the route taken by Möllerfeld. Instead we choose to treat the construct syntactically as ‘binder’.
Semantically we construe in the intended model as a bona fide least fixed point of the (parametrised) operator defined by . Namely, in the sense of the remark above, we can set to be the least fixed point of the operator , for all sets and numbers . Note that by simple algebraic reasoning this forces to be interpreted as the analogous greatest fixed point in .
As in earlier parts of this work, we shall frequently suppress variables in formulas, e.g. writing simply for when are unambiguously clear from context.
7.2. Theories and
Let us expand Peano Arithmetic () to the language , i.e. by including induction instances for all -formulas. The theory we consider here is equivalent to (the first-order part of) Möllerfeld’s .
Definition 80** (Theory).**
The theory is the extension of by the following axioms for formulas , :
- ()
**
- ()
**
We may construe as a proper fragment of full second-order arithmetic by the interpretation:
[TABLE]
The axioms above are readily verified by mimicking a standard textbook algebraic proof of Knaster-Tarski in the logical setting, cf. Proposition 70.
Möllerfeld’s main result was that is in fact -conservative over his theory , and so we have:
Theorem 81** (Implied by [27]).**
* is arithmetically conservative over .*
We set to be the intuitionistic counterpart of . I.e. is axiomatised by Heyting Arithmetic (extended to the language ) and the schemes and in Definition 80 above. We shall assume that uses only the logical symbols .
Once again, we may construe as a proper fragment of full second-order Heyting Arithmetic by (8) above. By essentially specialising known conservativity results for second-order arithmetic, we may thus show that and provably define the same functions on natural numbers.
Proposition 82** (Implied by [38]).**
* (and so also ) is -conservative over .*
7.3. Realisability judgement
In what follows we shall work with the untyped calculus and its typed version from Section 4. For convenience, we identify numerals of these calculi with numerals of the language of arithmetic.
A (realisability) candidate is an (infix) relation relating a (untyped) term to a natural number such that is always closed under . Let us expand by a (unary) predicate symbol for each realisability candidate. The idea is that each consists of the just the realisers of the sentence .
Definition 83** (Realisability judgement).**
For each term and closed formula we define the (meta-level) judgement as follows:303030Recall that closed terms of arithmetic always evaluate to numerals. We shall identify closed terms with their evaluation throughout this section to simplify the exposition. This also avoids any confusion arising from metavariable clash between terms of arithmetic and terms of .
- •
* if .*
- •
* if and .*
- •
* if .*
- •
* if there is with and *
- •
* if, whenever , we have .*
- •
* if whenever we have .*
- •
, where is not a -formula, if for all we have
- •
* if for all candidates .*
Definition 84** (Realising type).**
The realising type of a (possibly open) formula without candidate symbols, written , is given by:
- •
**
- •
**
- •
**
- •
**
- •
**
- •
**
- •
* if not a -formula.*
- •
**
Remark 85** (Peculiarities of our realisability notions).**
Note that we have, somewhat unusually, divided the realisability clause for -formulas into two cases, depending on whether the matrix is an implication or not. The reason for this is to streamline the definition of realisers for the and axioms, which will end up being versions of and respectively. It might have been natural to further decompose the matrix of a universal quantification, and to account for several universal quantifiers at a time, but the present exposition suffices for our purposes.
In fact, it is quite important to modify the realisability judgement in this way, due to the fact that quantifiers implicitly vary over natural numbers, and not other domains. Since the realisability judgement inlines this presumption, the usual -clause would create a type-mismatch between the usual realisability type for and the way the axioms of are (and, indeed, must be) formulated.
This issue could be elegantly sidestepped by using the notion of ‘abstract realisability’, cf. [37], where the realisability judgment actually commutes with quantifiers, but inductive definitions are employed to relativise the domain. The advantage of this is that inductive definitions in predicate logic correspond exactly to inductive types, in terms of realising type. Indeed, this is the approach taken by Berger and Tsuiki in [6] for a similar setting. They considered only strictly positive inductive definitions within intuitionistic logic,313131Though we suspect that their methods shuoold equally apply in the non-strict case, just as for our type structure . and their corresponding domain of realisers treats inductive definitions as bona fide fixed points, much like our type structure from Section 5.
We do not take this approach, instead choosing to keep our predicate logic/theory as standard as possible and instead modifying appropriately the notions of realisability judgement and type. Our argument should be seen as a suitable specialisation of the realisability argument for into Girard-Reynolds , inlining many of the technicalities (in particular avoiding the need to apply terms to types). Let us point out that our argument naturally applies to Berger and Tsuiki’s logic too, and its extension to (not necsssarily strictly) positive fixed points.
7.4. Main realisability argument
We start with proving some closure properties of our realisability model:
Lemma 86** (Closure under ).**
If and then .
Proof.
By induction on the complexity of :
- •
if is an equation then still by symmetry/transitivity of .
- •
if is then the statement follows by the fact that is a candidate, and so closed under the theory.
- •
if is then we have and , and so by IH we have and , thus indeed .
- •
if is then for any we have , and so also by IH. Since choice of was arbitrary we are done.
- •
if is then there is some with and . So by IH we have , and so also .
- •
if is then for each we have , and so also by IH. Since choice of was arbitrary we are done.
- •
if is then, for all candidates we have , and so also by IH. Since choice of was arbitrary we are done.
∎
Note that, despite its simplicity, the above lemma has the following powerful consequence, by consideration of the candidate :
Proposition 87**.**
If then .
We also have as expected:
Lemma 88** (Functoriality lemma).**
If and then for all candidates :
- (1)
for positive in , ; 2. (2)
for negative in , .
The main result of this subsection is:
Theorem 89** (Realisability).**
If then there is a (typed) term in such that .
Proof.
The axioms and rules of intuitionistic predicate logic are realised as usual (in particular since typed- derives typed versions of combinators). Note that our particular variation of the realisability judgement and type, cf. Remark 85, pose no significant issues here, simply requiring some extra (un)currying operations on realisers. Induction is realised by as usual. We shall focus on fixed point axioms peculiar to .
For (an instance of) the (ind) axiom
[TABLE]
where and , we shall take as realiser . Note that this indeed matches , by our variation of realisability type. To justify this let let and and we show that :
[TABLE]
For the (pre) axiom we shall actually realise a (clearly) logically equivalent version (pre’) in order to simplify the realiser,
[TABLE]
where . We will sometimes suppress the variables , writing just instead of when it is convenient and unambiguous. We shall take as realiser simply . Note that this indeed matches the variation (pre’) of the (pre) axiom above. To justify this let and , for a candidate , and we show that :
[TABLE]
∎
We can finally state the desired consequence of our realisability argument.
Corollary 90**.**
Any provably recursive function of (and so also ) is representable in (and so also ).
8. Extension to other fixed point logics
As promised in the introduction, our results cover more than just the systems and , accounting also for linear logic systems from [5, 2, 4, 16, 17, 3, 14, 13, 12]. We will briefly recall the systems and from, say, [4]323232 is the regular fragment of in that work.. Both systems are construed as computational models in terms of their notions of cut-reduction (analogous to and respectively).
8.1. The system
is the extension of by fixed point rules , (with no context in the left-premiss),333333This is crucial for cut-reduction due to the underlying linearity. and (with no context in the right-premiss).
Definition 91** (Pretypes, types, sequents).**
Pretypes*, written etc. are generated by the following grammar:*
[TABLE]
where, as usual, the operators and bind the variable in . Negation is the involution on pretypes written and satisfying: , , , . As usual, we set . Free variables of a pretype and the notion of positive and negative polarity of a variable in a pretype are as expected, with negation flipping polarity. A pretype is a type (or even formula) if, for any subexpression , is positive in . The notion of substitution for types is defined in the usual way, noticing that . A cedent, written etc., is just a list of types. If , we write for . A sequent is an expression .
Definition 92** (System ).**
The system is given by the rules of Figure 22 and Figure 23. The notions of derivation (or proof) are defined as usual.
Let be a (possibly open) type that is positive in . For a proof we define a proof of inductively. We only define . Then, is
[TABLE]
the other cases are easy to define. The above functoriality property allows us to define cut-reduction rules for , which are standard. Figure 25 shows the case corresponding to the interaction between and .
We define the type of natural numbers as . We also define the numeral by induction on :
[TABLE]
We say that a function is representable in if there is a coderivation of such that, for any , the derivation
[TABLE]
reduces under to the numeral . In this case we say that represents in .
Remark 93**.**
It is well-known that can encode the modalities and from linear logic (see, e.g., [2]). Given a type , we define as the type and we set . If , we write (resp. ) for (resp., ) The following exponential rules from linear logic, and the corresponding cut-reduction rules, are derivable:
[TABLE]
Theorem 94**.**
If in then there is derivation in such that and represent the same function on natural numbers.
Proof idea.
As a consequence of our grand tour results, and represent the same numerical functions. We define a translation from to . This translation is obtained by extending the standard call-by-name translation of intuitionistic logic into linear logic (see, e.g., [20]) which, in particular, satisfies the equations and , using Baelde’s encoding of linear logic [20] in as in Remark 93. Details are reported in Section D.1. ∎
8.2. The system
We shall write for the circular version of this system, defined in a similar way to over the extension of by rules , , and .
Definition 95** (System ).**
A (-) coderivation is a possibly infinite rooted tree (of height ) generated by the rules of in Figure 22 and Figure 24. We say that a coderivation is regular (or circular) if it has only finitely many distinct sub-coderivations. The notions of ancestry, thread, and progressiveness for coderivations are standard and require minor adaptations of Definition 20 and Definition 21 (see, for example, [4]). is the class of regular progressing -coderivations.
The cut-reduction rules on coderivations are standard (we refer to [4] for more detail). Figure 25 displays the cut reduction corresponding to the interaction between and .
The notion of representability for is defined as representability for . It is known that the former systems represents as many numerical functions as the latter. Its proof is similar to the one for Proposition 23:
Theorem 96** (Simulation [15]).**
* simulates .*
The following result can be established via a negative translation similar to Proposition 26. Details are reported in Section D.2.
Theorem 97**.**
If of in then there is coderivation of in such that and represent the same function on natural numbers.
8.3. Comparing , , , and
Putting every result together, we have:
Theorem 98** (Computational equivalence).**
The following systems represent the same functions on natural numbers:
- (1)
** 2. (2)
** 3. (3)
** 4. (4)
**
Proof.
Point 1 implies point 2 by Theorem 94. Point 2 implies point 3 by Theorem 96. Point 4 implies point 1 by Theorem 97. Finally, point 4 implies point 1 as a consequence of our grand tour results.
∎
9. Conclusions
In this work we investigated the computational expressivity of fixed point logics. Our main contribution is a characterisation of the functions representable in the systems as the functions provably recursive in the second-order theory . Referring to Rathjen’s ordinal notation system in [30], this means that all these systems represent just the functions computable by recursion on ordinals of . To this end we used a range of techniques from proof theory, reverse mathematics, higher-order computability and metamathematics. This contribution settles the question of computational expressivity of (circular) systems with fixed points, cf. Question 1.
In future work it would be interesting to investigate the computational expressivity of systems with only strictly positive fixed points, where may only bind variables that are never under the left of . We suspect that such systems are computationally weaker than those we have considered here. On the arithmetical side, it would be interesting to investigate the higher-order reverse mathematics of the Knaster-Tarski theorem, cf. [33] and the present work.
Appendix A Appendix for Section 2
A.1. Weak and strong (co)iteration rules
Our presentation of the iteration rule (i.e., ) and the coiteration rule (i.e., ) for is the most permissive one, in that contexts are allowed to appear in both premises:
[TABLE]
Their cut-reduction rules are as in Figure 26. The reader should notice that the context in both the rules of (9) is contracted during cut-reduction. For this reason, alternative presentations of and without the context have been studied in the literature, especially in the setting of linear logic, where contraction cannot be freely used (see, e.g., [5])
[TABLE]
Single premise formulations of and for both (9) and (10) have been investigated in the literature as well (see, e.g., [7]):
[TABLE]
[TABLE]
The corresponding cut-reduction rules for (10), (11), and (12) can be easily extracted from the ones in Figure 26.
It is worth mentioning, however, that cut-elimination fails in presence of the rules (11) and (12). By contrast, being essentially endowed with a built-in cut, the rules (9) and (10) allow cut-elimination results.
Perhaps surprisingly, all formulations of and are equivalent, meaning they can derive each other crucially using the cut rule.
Proposition 99**.**
In endowed with the rules and (Figure 3), the rules (9), (10), (11), and (12) and their cut-reduction are inter-derivable.
Proof.
It suffices to show that the rules in (12) can derive the rules in (11). We only show the case of , as the case of is symmetric. W.l.o.g., we will treat in (11) as a single formula. The case where is an arbitrary context can be recovered using and . The derivation is the following:
[TABLE]
where is the derivation in Figure 27. It is tedious but routine to show that the above derivation of allows us to derive the cut-reduction rule for (12). ∎
Appendix B Appendix for Section 3
B.1. Proof of Proposition 26
We give a bespoke combination of a negative translation and a Friedman-Dragalin ‘A translation’ suitable for our purposes. Writing and . At the risk of ambiguity but to reduce syntax, we shall simply write for henceforth.343434 Any confusion will be minimal as we shall not parametrise negation by any other A-translation in this work. Also, we shall include the following derivable rules of :
[TABLE]
[TABLE]
We define the translations and from arbitrary types to types over as follows:
[TABLE]
Proposition 100** (Substitution).**
- •
**
- •
**
- •
.
We shall extend the notations and to cedents, e.g. writing and , by distributing the translation over the list. For a sequent , we also write for
Definition 101** (-translation of steps).**
For each inference step
[TABLE]
we define a gadget,
[TABLE]
as in Figure 28. We lift this to a translation on coderivations in the obvious way.
Proposition 102**.**
If is progressing and regular then so is .
Proof.
As for regularity, we observe that the translation maps any inference rule to a gadget with constantly many rules. Concerning progressiveness, it is easy to check that:
- •
for any infinite branch of there is an infinite branch of such that for some sequence
- •
for any thread in connecting a formula in with a formula in there is a thread in connecting in with a formula in ; moreover, if the former thread has progressing points then the latter has.
∎
Proposition 103**.**
If then
Proof.
The proof is routine. We just consider the cut-reduction step eliminating a cut of the form vs . W.l.o.g., we assume ends with this cut. Then, has the following shape:
[TABLE]
Which is translated into a cut between the following two coderivations:
[TABLE]
[TABLE]
by applying a few cut-reduction steps we obtain the following:
[TABLE]
Which is the translation of the following:
[TABLE]
∎
Proposition 104** ((De)coding for ).**
There are coderivations and over in such that, for any :
[TABLE]
[TABLE]
Proof.
and are defined, respectively, as follows:
[TABLE]
[TABLE]
where [math] and are derivations as in Figure 6. ∎
Theorem 105**.**
If in then there is coderivation over in such that and represent the same functions on natural numbers.
Proof.
Let be a numerical function of , w.l.o.g. we can assume is unary. This means that there is a derivation of such that
[TABLE]
By Proposition 103 we have that, for any :
[TABLE]
Then, can be represented by the following coderivation over :
[TABLE]
∎
Appendix C Appendix for Section 7
C.1. Conservativity via double negation translation
In what follows we prove Proposition 82353535A different proof can be found in [Tupailo04]. Henceforth, with little abuse of notation, with (resp., ) we denote the conservative extensions obtained by endowing the language with new function symbols representing arbitrary primitive recursive functions, and by adding equations defining the new identities as axioms. The following is a standard property:
Lemma 106**.**
Let be quanfier-free. Then, there is a primitive recursive function symbol such that , in both and .
Here we give an alternative and self-contained proof for the sake of exposition.. We start with a definition a Gödel-Gentzen-style translation of formulas of into formulas of :
[TABLE]
Some straightforward properties of the translation:
Lemma 107**.**
- (1)
** 2. (2)
**
Lemma 108**.**
If then .
Proof.
We show that any axiom of is derivable in , where the translation on equations is justified by the fact that . We just check the axioms for the least fixed point operator . On the one hand, we have as an instance of (pre), and by logic. We conclude by applying transitivity of implication and the generalisation rule introducing . On the other hand, let us assume . By (ind) we obtain . By logic we have and (Lemma 107.2). We conclude by applying transitivity of implication and deduction theorem, using Lemma 107.1. ∎
We now use a standard simply trick called Friedman’s translation to infer our conservativity result from the above lemma. Let be a fixed formula of . For any formula of we define as follows:
[TABLE]
The replacement must be done without variable capture, so whenever we consider, e.g., , we must assume that is not free in .
Some straightforward properties of :
Lemma 109**.**
- (1)
** 2. (2)
**
Lemma 110** (Friedman’s translation, adapted).**
If then .
Proof.
It is easy to check that implies , where , observing that by Lemma 109.2. So, Friedman’s translation preserves derivability. Therefore, to conclude, it suffices to show that proves Friedman’s translation of ’s axioms. We only consider the cases of the axioms for the least fixed point operator . On the one hand, by instantiating (pre), we have , with (Lemma 109.1), so that we can conclude . On the other hand, we have to prove that implies . By instantiating (ind) we have that the former implies . Also, from Lemma 109.2 we infer , so implies . This concludes the proof. ∎
We can finally prove Proposition 82:
Proof of Proposition 82.
Assume for quantifier-free. By Lemma 106 there is a primitive recursive function symbol such that in both and , so it suffices to show . We set . Of course, , so by Lemma 108. By Lemma 109 we have , where , which is clearly equivalent to . Thus, we have , and so . We conclude by generalising over . ∎
Appendix D Appendix for Section 8
D.1. A translation of into
We now show that any function on natural numbers representable in is also representable in . W.l.o.g., we will focus on the subsystem of , which includes only (native) rules and cut-reductions over (see Definition 25). Notice that and have the same computational strength as a consequence of the grand tour results of this paper. Also, we shall replace the rules and in Figure 4 with their “weaker” formulation in (10). With little abuse of notation, we keep writing for the resulting system, as this substitution causes no loss in expressivity (by Proposition 99). This will allow us to relate the rules and with the rule in , whose right-hand premise is context-free to avoid linearity issues as discussed in Appendix A.
We now define a translation from pretypes of into pretypes of as follows:
[TABLE]
Proposition 111** (Substitution).**
.
We shall extend the translation to sequents of by defining as .
For each inference step
\Sigma_{1}\Rightarrow\tau_{1}$$\cdots$$\Sigma_{n}\Rightarrow\tau_{n}
we define a gadget,
[TABLE]
As the (call-by-name) translation of intuitionistic into linear logic is standard (see, e.g., [20]), we shall only show the case of the inference rules for and in Figure 29. We lift this to a translation on coderivations in the obvious way.
Proposition 112**.**
If then
Proof.
It is routine. ∎
From which we conclude:
Proof of Theorem 94.
As a consequence of our grand tour results, and represent the same numerical functions. Let now be a derivation of in . The translation maps into a derivation of the same sequent. We conclude by applying Proposition 112. ∎
D.2. A translation from into
We give a translation of into similar to the one defined in Section B.1, using the same convention of writing and using the derivable rules in Equation 13.
We define the translations and from to as follows:
[TABLE]
Proposition 113**.**
We have:
- •
**
- •
**
- •
**
Proposition 114** (Substitution).**
- •
**
- •
**
- •
.
We shall extend the notations and to cedents, e.g. writing and , by distributing the translation over the list. For a sequent , we also write for . For each inference step
\Rightarrow\Sigma_{1}$$\cdots$$\Rightarrow\Sigma_{n}
we define a gadget,
[TABLE]
as in Figure 28. We lift this to a translation on coderivations in the obvious way.
Proposition 115**.**
If is progressing and regular then so is .
Proof.
By applying a reasoning similar to Proposition 102. ∎
Proposition 116**.**
If then
Proof.
It is routine. ∎
The following is an adaptation of Proposition 104.
Proposition 117** ((De)coding for ).**
There are coderivations and in such that, for any :
[TABLE]
[TABLE]
Proof.
and are defined, respectively, as follows:
[TABLE]
[TABLE]
∎
Proof of Theorem 97.
We apply the same reasoning of Theorem 105 ∎
The reference list from the paper itself. Each links out to its DOI / PubMed record.
- 1[1] Jeremy Avigad and Solomon Feferman. Gödel’s functional (“dialectica”) interpretation. Handbook of proof theory , 137:337–405, 1998.
- 2[2] David Baelde. Least and greatest fixed points in linear logic. ACM Trans. Comput. Log. , 13(1):2:1–2:44, 2012.
- 3[3] David Baelde, Amina Doumane, Denis Kuperberg, and Alexis Saurin. Bouncing threads for circular and non-wellfounded proofs: Towards compositionality with circular proofs. In Christel Baier and Dana Fisman, editors, LICS ’22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Haifa, Israel, August 2 - 5, 2022 , pages 63:1–63:13. ACM, 2022.
- 4[4] David Baelde, Amina Doumane, and Alexis Saurin. Infinitary proof theory: the multiplicative additive case. In Jean-Marc Talbot and Laurent Regnier, editors, 25th EACSL Annual Conference on Computer Science Logic, CSL 2016, August 29 - September 1, 2016, Marseille, France , volume 62 of LIP Ics , pages 42:1–42:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016.
- 5[5] David Baelde and Dale Miller. Least and greatest fixed points in linear logic. In Nachum Dershowitz and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning, 14th International Conference, LPAR 2007, Yerevan, Armenia, October 15-19, 2007, Proceedings , volume 4790 of Lecture Notes in Computer Science , pages 92–106. Springer, 2007.
- 6[6] Ulrich Berger and Hideki Tsuiki. Intuitionistic fixed point logic. Annals of Pure and Applied Logic , 172(3):102903, 2021.
- 7[7] Pierre Clairambault. Least and greatest fixpoints in game semantics. In Ralph Matthes and Tarmo Uustalu, editors, 6th Workshop on Fixed Points in Computer Science, FICS 2009, Coimbra, Portugal, September 12-13, 2009 , pages 39–45. Institute of Cybernetics, 2009.
- 8[8] Pierre Clairambault. Strong functors and interleaving fixpoints in game semantics. RAIRO Theor. Informatics Appl. , 47(1):25–68, 2013.