Dieses Kapitel vertieft sich in die komplexe Welt der Modalrechnung, einer Logik, die sich bei der Untersuchung von Computersystemen, insbesondere reaktiven Systemen, als hilfreich erwiesen hat. Sie befasst sich mit der langjährigen Herausforderung der Cut-Eliminierung, einem grundlegenden Aspekt der modernen Beweistheorie, der in der bestehenden Literatur nur teilweise gelöst wurde. Das Kapitel führt einen bahnbrechenden Ansatz ein, indem es die lineare Logik nutzt, eine ressourcensensible Logik, die entwickelt wurde, um die Cut-Elimination selbst zu analysieren. Durch die Bereitstellung einer linearen Zerlegung der Modalrechnung im Rahmen linearer Logik etablieren die Autoren ein syntaktisches Cut-Elimination-Theorem für die vollständige Modalrechnung, eine bisher unerreichte Leistung. Das Kapitel untersucht die tiefe Einheit und große Vielfalt der Logik und schlägt ein gemeinsames Rahmenwerk für Kozens modales Kalkül und Girards lineare Logik vor. Es navigiert durch die Komplexität zirkulärer und unbegründeter Beweissysteme und bietet eine detaillierte Analyse der Zulässigkeit von Schnitten versus ihrer Eliminierung. Das Kapitel diskutiert auch die möglichen Implikationen dieser Arbeit, einschließlich der Entwicklung einer denotationalen Semantik für Beweise der Modalrechnung und der Erforschung der Lichtlogik. Durch seinen innovativen Ansatz und seine umfassende Analyse ebnet dieses Kapitel den Weg für neue Fortschritte in der Beweistheorie und Rechenlogik.
KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
Abstract
This paper presents a proof-theoretic analysis of the modal \(\mu \)-calculus. More precisely, we prove a syntactic cut-elimination for the non-wellfounded modal \(\mu \)-calculus, using methods from linear logic. and its exponential modalities. To achieve this, we introduce a new system, \(\mu \textsf {LL}_{\Box }^{\infty }\), which is a linear version of the modal \(\mu \)-calculus, intertwining the modalities from the modal \(\mu \)-calculus with the exponential modalities from linear logic. Our strategy for proving cut-elimination involves (i) proving cut-elimination for \(\mu \textsf {LL}_{\Box }^{\infty }\) and (ii) translating proofs of the modal mu-calculus into this new system via a “linear translation”, allowing us to extract the cut-elimination result.
1 Introduction
Eliminability of cuts and the modal\(\mu \)-calculus. Since Kozen’s seminal work on the modal\(\mu \)-calculus [17], this logic extending basic modal logic with least and greatest fixed-points has been extremely fruitful for the study of computational systems, especially reactive systems. In addition to its wide expressive power, its deep roots in logic also allow for a number of fruitful approaches, be they model-theoretic, proof-theoretic or automata-theoretic. Still, cut-elimination – a cornerstone of modern proof-theory – has only received partial solutions [1, 6, 21, 22, 24]:
Either as cut-admissibility statements which are noneffective possibly using infinitary proof-systems such as (i) infinitely branching proof systems, allowing the \(\omega \)-rule [16] or (ii) non-wellfounded or circular proof systems [1, 24], allowing proof-trees with infinitely long branches;
Or as syntactic cut-elimination results capturing only a fragment of the calculus in systems with the \(\omega \)-rule [21, 22]. A challenge in describing a syntactic cut-elimination for such systems is that the number of applications of a \(\mu \)-rule must sometimes be determined before knowing how many are needed to match each premises of a \(\nu \)-rule. In [6], the authors discuss a specific example where syntactic cut-elimination fails. While there are syntactic cut-elimination results in systems based on the \(\omega \)-rule [6, 21, 22], they capture only strict fragments of the modal \(\mu \)-calculus.
In fact, there is no syntactic cut-elimination theorem for the full modal \(\mu \)-calculus. The present work establishes such a syntactic cut-elimination theorem for the modal \(\mu \)-calculus in the setting of non-wellfounded sequent calculus.
Anzeige
On unity and diversity in computational logic. Logic presents at the same time a deep unity and a wide diversity. Miller [20] argues that the “universal character [of logic] has been badly fractured in the past few decades”, due to the wide range of its applications, the various families of logics that have emerged and the different computational tools that are in use, often with little relationship. Miller thus proposes the following questions as the first of a list of “challenges”:
Challenge 1:Unify a wide range of logical features into a single framework. How best can we explain the many enhancements that have been designed for logic: for example, classical / intuitionistic / linear, fixed points, first-order / higher-order quantification, modalities, and temporal operators? (...)
In the present paper, we partially address Miller’s first challenge, providing a common framework for two of the main logics that emerged in the 1980s, Kozen’s modal \(\mu \)-calculus [17] and Girard’s linear logic (\(\textsf {LL}\)) [14]. Working in the setting of circular and non-wellfounded proof systems for the above logics, we propose a so-called linear decomposition of the modal \(\mu \)-calculus in linear logic with fixed-points. This proof-theoretic analysis of the modal \(\mu \)-calculus allows us to do a finer-grained treatment of syntactic cut-elimination.
Cut-admissibility vs. cut-elimination. The treatment of the cut-inference in sequent-based proof-systems follows two main traditions: (i) one can consider cut-free proofs as the primitive proof-objects and establish that the cut inference is admissible (according to this tradition, the cut-inference essentially lives at the metalevel, ensuring compositionality of the logic) or (ii) one can consider that the cut inference lives at the object-level and is a fundamental piece of proofs: one thus establishes that the cut inference is eliminable, ensuring the sub-formula property (and its numerous important consequences, ranging from consistency to interpolation properties).
This second tradition may use similar techniques as the first tradition, but it also permits the investigation of a syntactic, or effective, approach to cut-elimination, consisting of a cut-reduction relation on proofs, shown to be (at least) weakly normalizing, with the normal forms being cut-free proofs. An advantage of such syntactic cut-elimination results is that, in many settings (most notably \({\textsf {LJ}}\) and \({\textsf {LL}}\) [14]), such cut-reductions induce an interesting relation on proofs and have a computational interpretation that is the starting point of the Curry-Howard correspondence built upon sequent calculus [9].
Anzeige
Linear Logic. Linear logic (\(\textsf {LL}\)) is often described as a resource-sensitive logic. It is more accurate, though, to view it as a logic designed for analyzing cut-elimination itself. Indeed, \(\textsf {LL}\) comes from an analysis of structural rules, aiming at controlling them rather than weakening them as in substructural logics. This solves some fundamental drawbacks of cut-elimination in classical logic, such as its non-termination or non-confluence. For instance, \(\textsf {LL}\) permits the decomposition of both intuitionistic and classical logic, in a structured and fine-grained manner allowing the refinement of the cut-elimination of those logics as well as their notion of model (allowing the building of a non-trivial denotational model of classical proofs); the prototypical example of such a linear decomposition consists in decomposing the usual intuitionistic arrow (i.e., the function type of the \(\lambda \)-calculus), \(A \Rightarrow B\), into a replication operator and a linear implication:
[10, 14]. Further analyses on these exponential modalities led to the discovery of light logics, where the complexity of cut-elimination is tamed in a flexible way, usually by considering alternative, weaker exponential modalities.
The proof theory of \(\textsf {LL}\) was extended to \(\mu \textsf {LL}^{\infty }\), that is \(\textsf {LL}\) with fixed-points in the finitary and non-wellfounded setting [2, 12, 26‐28] and \(\mu \textsf {LL}^{\infty }\) allowed for the same kind of linear decomposition for (the non-wellfounded version of) \(\mu \textsf {LJ}\) and \(\mu \textsf {LK}\). A natural question is whether the extensions of \(\textsf {LL}\) with fixed-points can also help us achieve syntactic cut-elimination for the modal \(\mu \)-calculus.
Contributions. The discussion of the above paragraph suggests a first question: what would be a linear decomposition of the modal \(\mu \)-calculus? The first contribution of this paper is to provide such a linear decomposition of the modal \(\mu \)-calculus which is compatible with circular and non-wellfounded proof theory, \(\mu \textsf {LL}_{\Box }^{\infty }\). This linear-logical modal\(\mu \)-calculus will allow us to complete the analysis of cut-elimination for the modal \(\mu \)-calculus, proving the first syntactic cut-elimination theorem for the full modal \(\mu \)-calculus (in the non-wellfounded setting). We therefore adopt the following roadmap in the body of the paper.
In Section 2, we recall the necessary technical background about \(\mu \textsf {LL}^{\infty }\) and \(\mu \textsf {LK}_{\Box }^{\infty }\) proof theory. In Section 3, we motivate and introduce \(\mu \textsf {LL}_{\Box }^{\infty }\) and prove its cut-elimination in Section 4. We then define the linear decomposition of \(\mu \textsf {LK}_{\Box }^{\infty }\) into \(\mu \textsf {LL}_{\Box }^{\infty }\) from which we conclude to \(\mu \textsf {LK}_{\Box }^{\infty }\) cut-elimination theorem in Section 5 in the form of an infinitary weak-normalizing cut-reduction system.
2 Circular and (non-)wellfounded proof systems
We recall here some basic definitions of both wellfounded & non-wellfounded systems. Some standard definitions of proof theory such as derivation rules, active formula or principal formula are not recalled and can be found in [7].
2.1 The Modal \(\mu \)-calculus
Formulas Let \(\mathcal {V}\) and \(\mathcal {A}\) be two disjoint sets of fixed-point variables and of atoms respectively. We define the pre-formulas of the modal \(\mu \)-calculus, \(\mu \textsf {LK}_{\Box }^{\infty }\), as: \(F, G :\,\!:= a \mid ~\hbox {X} \mid \mu X. F \mid \nu X. F \mid \Box F \mid \lozenge F \mid F^\perp \mid F\rightarrow G \mid F \vee G \mid F \wedge G \mid \textsf{F}\mid \textsf{T}(a\in \mathcal {A}, X\in \mathcal {V})\). Knaster-Tarski’s theorem guarantees the existence of extremal fixed-points of monotonic functions on complete lattices; monotonicity is reflected syntactically as a positivity condition on variables, defined as:
Definition 1
(Positive & negative occurrence of fixed-point variables) Let \(X\in \mathcal {V}\) be a fixed-point variable, one defines the fact, for X, to occur positively (resp. negatively) in a pre-formula by induction on the structure of pre-formulas:
X occurs positively in X.
X occurs positively (resp. negatively) in \({c} (F_1, \dots , F_n)\), if there is some \(1\le i \le n\) such that X occurs positively (resp. negatively) in \(F_i\) for \(c\in \{\Box , \lozenge , \vee , \wedge \}\).
X occurs positively (resp. negatively) in \(F^\perp \) if it occurs negatively (resp. positively) in F.
X occurs positively (resp. negatively) in \(F\rightarrow G\) if X occurs either positively (resp. negatively) in G or negatively (resp. positively) in F.
X occurs positively (resp. negatively) in \(\delta Y. G\) (with \(Y\ne X\)) if it occurs positively (resp. negatively) in G (for \(\delta \in \{\mu , \nu \}\)).
We can now define the formulas of \(\mu \textsf {LK}_{\Box }^{\infty }\):
Definition 2
(Formulas) A \(\mu \textsf {LK}_{\Box }^{\infty }\)formulaF is a closed pre-formula such that for any sub-pre-formula of F of the form \(\delta X. G\) (with \(\delta \in \{\mu , \nu \}\)), X does not occur negatively in G.
By considering the \(\{\mu ,\nu , X\}\)-free formulas of this system, we get \(\textsf {LK}_{\Box }\). By considering the \(\{\Box , \lozenge \}\)-free formulas of \(\mu \textsf {LK}_{\Box }^{\infty }\), we get the \(\mu \)-calculus. Finally, the intersection of these two systems, is propositional classical logic.
Sequent calculus We define, here, the sequents, rules and proofs for \(\mu \textsf {LK}_{\Box }^{\infty }\).
Definition 3
(Sequent) A sequent is an ordered pair of two lists of formulas \(\varGamma \), the antecedent, and \(\varDelta \), the succedent, that we write \(\varGamma \vdash \varDelta \).
Remark 1
(Derivation rules & ancestor relation) In the structural proof theory literature, inference rules are defined together with an ancestor relation (or sub-occurrence relation) between formulas of the conclusion and formulas of the premises of the rule. While this relation is often overlooked we provide some details here. Sequent being lists, we define the ancestor relation, to be a relation from the positions of the formula in the conclusion, to the positions of the formula in the premises. Those ancestor relations will be dealt graphically as in Figures 1 and 2, by drawing the ancestor relation on sequents when needed and leaving it implicit when unambiguous.
Fig. 1.
Rules of \(\textsf {LK}_{\Box }\)
We define the inference rules for \(\textsf {LK}_{\Box }\) in Figure 1. Rules for \(\textsf {LK}\) will be the \(\{\Box ,\lozenge \}\)-free rules of \(\textsf {LK}_{\Box }\). We add rules of Figure 2 to \(\textsf {LK}\), (resp. \(\textsf {LK}_{\Box }\)) to get the fixed-point version \(\mu \textsf {LK}^{\infty }\) (resp. \(\mu \textsf {LK}_{\Box }^{\infty }\)) of this system. The two exchange rules\((\text {ex}_l)\) and \((\text {ex}_r)\) from Figures 1 and 4 allows one to derive the rule
for any permutations \(\sigma \) and \(\sigma '\) of \(\{ 1,\dots , \#(\varDelta )\}\) and \(\{ 1,\dots , \#(\varGamma )\}\) respectively, where \(\sigma (\varDelta )\) designates the action of \(\sigma \) on the list \(\varDelta \), with the induced ancestor relation. In the rest of the article, we will intentionally treat the exchange rule implicitly: the reader can consider that each of our rules are preceded and followed by a finite number of rule \((\text {ex})\).
Fig. 2.
Rules for the fixed-point fragment
Proofs of non fixed-point systems, \(\textsf {LK}\), \(\textsf {LK}_{\Box }\) are the trees inductively generated by the corresponding set of rules of each of these systems. We can define a first notion of infinite derivations, pre-proofs, that will soon be refined:
Definition 4
(Pre-proofs) Given a set of derivation rules, a pre-proof is a tree co-inductively generated using the rules of the system.
Example 1
(Regular pre-proof) Regular pre-proofs are those pre-proofs having a finite number of distinct sub-proofs. We represent them with back-edges. Taking \(F:=\nu X. \lozenge X\), we have:
Remark 2
The pre-proofs define an inconsistent system. In fact, any sequent is provable:
Proofs are defined as those pre-proofs satisfying a correctness condition:
Definition 5
(Validity and proofs) Let \(b=(s_i)_{i\in \omega }\) be a consecutive sequence of sequents defining an infinite branch in a pre-proof \(\pi \). A thread of b is a sequence \((F_i\in s_i)_{i>n}\), for some \(n\in \omega \), of occurrences such that for each j, \(F_j\) and \(F_{j+1}\) satisfy the ancestor relation. We say that a thread of b is valid if the minimal recurring formula of this sequence, for the sub-formula ordering, exists and is (i) either a \(\nu \)-formula appearing infinitely often on the succedent of its sequent or a \(\mu \)-formula appearing infinitely often in the antecedent of its sequent and (ii) the thread is infinitely often principal (there are an infinite number of principal formulas in it). A branch b is valid if there is a valid thread of b.
A pre-proof is valid and is a proof if each of its infinite branches is valid.
The least (\(\mu \)) and greatest (\(\nu \)) fixed-point constructors have the same (local) derivation rules: they are distinguished by the (global) validity condition, which is a parity condition akin to parity games for the \(\mu \)-calculus.
Fig. 3.
Valid and invalid pre-proofs
Example 2
(Valid and invalid pre-proofs) Here, we give some examples of infinite proofs. The pre-proof of Example 1 is valid, that of Remark 2 is invalid.
We use the notation \(\text {Nat}:= \mu X. \textsf{T}\vee X\), representing the type of natural numbers. We can represent any natural number n by a finite valid proof \(\pi _n\) defined in Figure 3a. The infinite pre-proof \(\pi _{\infty }\), defined in Figure 3a, of \(\vdash \text {Nat}\) is not valid: the infinite branch in \(\pi _\infty \) is supported by only one thread, which is not valid as the minimal formula is a \(\mu \)-formula appearing only on the right of the proof. This is coherent with the interpretation that \(\mu \) is a least fixed-point: the system would reject the infinite proof of \(\text {Nat}\). Note that the same kind of proof with \(\text {coNat}:= \nu X. \textsf{T}\vee X\) would have given a valid proof.
The pre-proof of Figure 3b (representing the double function) is valid: The only infinite branch in it is the one going infinitely to the right at the application of the \((\vee _l)\)-rule. This branch is supported by the infinite thread in the antecedent of each sequent which has a \(\mu \)-formula as its minimal formula.
2.2 Linear Logic with fixed-points
The main difference between \(\textsf {LK}\) (or \(\textsf {LJ}\)) and \(\textsf {LL}\) lies in the fact that formulas are not always erasable nor duplicable. Hence, the sequent \(A, B\vdash A\) is not always provable, neither is \(A\vdash A\otimes A\) (a sequent similar to \(A\vdash A\wedge A\) in \(\textsf {LK}\)). This restriction allows \(\textsf {LL}\) to interpret programs with finer resource control than \(\textsf {LK}\) (or \(\textsf {LJ}\)). Here we recall the usual definitions of both the wellfounded and non-wellfounded systems of \(\textsf {LL}\), following the definitions of the previous section.
Formulas As for \(\mu \textsf {LK}_{\Box }^{\infty }\), let us set \(\mathcal {V}\) and \(\mathcal {A}\) as two disjoint sets. The pre-formulas of the non-well-founded linear logic, \(\mu \textsf {LL}^{\infty }\) are:
, with \(a\in \mathcal {A}, X\in \mathcal {V}\). Positivity of pre-formulas and \(\mu \textsf {LL}^{\infty }\) formulas are defined in the same way as for \(\mu \textsf {LK}_{\Box }^{\infty }\). The \(\{!, ?\}\)-free formulas of \(\mu \textsf {LL}^{\infty }\) are the formulas of \(\mu \textsf {MALL}^{\infty }\). The \(\{\mu ,\nu , X\}\)-free fragment of formulas of \(\mu \textsf {LL}^{\infty }\) are the formulas of linear logic \({\textsf {LL}}\). The intersection of these two fragments is \(\textsf {MALL}\).
Sequent calculus The definition of sequent is the same as for \(\mu \textsf {LK}_{\Box }^{\infty }\). The rules of \(\textsf {MALL}\) are given by Figure 4, the rules of \(\textsf {LL}\) are the rules of \(\textsf {MALL}\) together with the rules of Figure 5. We add the rules of Figure 2 to \(\textsf {MALL}\) (resp. \(\textsf {LL}\)) to obtain the rules of \(\mu \textsf {MALL}^{\infty }\) (resp. \(\mu \textsf {LL}^{\infty }\)). Pre-proofs as well as validity are defined as in the previous section.
Fig. 4.
Rules of multiplicative and additive linear logic
Fig. 5.
Exponential fragment of \(\textsf {LL}\)
In linear logic, duplicability and erasability are controlled by \(?\) (why not) and \(!\) (of course) modalities. The \((!_{\text {c} })\), \((!_{\text {w}})\), and \((!_{\text {d}})\) rules allow duplication, erasure, and use of \(!\)-prefixed antecedents, respectively. The \((!_{\text {p}})\) rule enables using an \(!\)-prefixed succedent when all antecedents are \(!\)-prefixed. This controlled approach to contraction and weakening sequentializes certain reductions in cut-elimination, leading to strong normalization for \(\textsf {LL}\) [25]. However, the good normalization properties of \(\textsf {LL}\) can be recovered by using a linear translation from \(\textsf {LK}\) to \(\textsf {LL}\), similar to the double negation translations from \(\textsf {LK}\) to \(\textsf {LJ}\). Indeed, every formula, every sequent, and every proof of \(\textsf {LK}\) can be translated into a proof in \(\textsf {LL}\) by adding \(?\) and \(!\) modalities. For instance in Figure 6 we show an example where each connective \(c(A_1, \dots , A_n)\) can be translated as \(!(c(?A_1, \dots , ?A_n))\) adding a \(?\) on the formula from the succedent, the additional rules being shown in blue. By taking any maximal sequence of cut reduction on such proofs in \(\textsf {LL}\) and using the strong normalization property, we find a cut-free proof of the same sequent in \(\textsf {LL}\). This projects to an \(\textsf {LK}\) proof of the original sequent, by simply forgetting superfluous modalities. In Section 5, we will use this technique to prove the cut elimination of the modal \(\mu \)-calculus.
Fig. 6.
Example of a linear translation
Cut-elimination for\(\boldsymbol{{\mu \textsf {LL}^{\infty }} }\) We postpone to Section 4 the discussion of cut-elimination reductions (Definition 8, 10 and 11) and theorems (Theorem 2): they are directly introduced for \(\mu \textsf {LL}_{\Box }^{\infty }\) that we shall consider in the next section.
We now introduce \(\mu \textsf {LL}_{\Box }^{\infty }\), which can be viewed from two perspectives:
as an extension of \(\mu \textsf {LL}^{\infty }\) with modalities akin to the modal \(\mu \)-calculus;
as a linearization of the modal \(\mu \)-calculus (where linear refers to linear logic – by default, any assumption must be used exactly once in a proof – and not to the structures of its models, as in LTL or linear-time \(\mu \)-calculus [30]).
In designing the \(\mu \textsf {LL}_{\Box }^{\infty }\) sequent calculus, the primary challenge lies in understanding the interaction between the \(\Box \) and \(\lozenge \) modalities and \(\textsf {LL}\) exponentials, while being compatible with the fixed-point inferences. A natural requirement for such a sequent calculus is to allow us to extend the linear decomposition of \(\mu \textsf {LK}^{\infty }\) [28] to \(\mu \textsf {LK}_{\Box }^{\infty }\). The constraints imposed by such a linear decomposition will therefore guide us in defining the exponential and modal rules of \(\mu \textsf {LL}_{\Box }^{\infty }\). The following discussion illustrates these requirements through examples and will lead us to the desired sequent calculus defined in Definition 6 below.
A first approach would be to simply extend \(\mu \textsf {LL}^{\infty }\) with the usual inferences for \(\Box \) and \(\lozenge \), extending the translation \({(-)}^{\bullet }\) from [28] on modalities as in Figure 6 setting \( {(\lozenge A)}^{\bullet } := !\lozenge ?{(A)}^{\bullet }\) and \({(\Box A)}^{\bullet } := !\Box ?{(A)}^{\bullet } \). This approach is too simplistic, though, and fails. Consider indeed an instance of the modal rule \(\Box _{\text {p}}\) (defined in Figure 1) with \(\varGamma =[]\) and \(\varDelta =[B]\):
Following the standard sequent translation from \(\textsf {LK}\) to \(\textsf {LL}\), we need to derive \(\vdash ?!\Box ?{A}^{\bullet }, ?!\lozenge ?{B}^{\bullet }\) from the premise \(\vdash ?{A}^{\bullet }, ?{B}^{\bullet }\). Reasoning bottom-up: to conclude \(\vdash ?{A}^{\bullet }, ?{B}^{\bullet }\), we must remove both the \(\lozenge \) and the \(\Box \) with a modal rule. However, regardless of the sequence of rules used, we always end up with a sequent containing an \(!\) together with either \(\Box \) or \(\lozenge \). An example of such a derivation is shown in Figure 7a. In our attempt to translate this rule, we are left with an unprovable sequent: indeed, the top sequent cannot be the conclusion of any rule in the system (except for cut and exchange, of course): \(!\Box ?{A}^{\bullet }\) cannot be principal since there is a \(\lozenge \)-formula in the context, and \(\lozenge ?{B}^{\bullet }\) cannot be principal since there is an \(!\)-formula.
Fig. 7.
Translating the modal rule in a linear framework
A natural solution is to allow \(!\)-promotion in contexts containing \(!,\Box \)-formulas on the left and \(?,\lozenge \)-formulas on the right as in Figure 7c.1 The derivation of the translation of our \((\Box _{\text {p}})\) instance can be completed as in Figure 7b.
Allowing \(\Box /\lozenge \)-formulas in the context of a promotion rule has implications for the system’s robustness to cut-elimination. For instance, taking the \((?_{\text {p}}/?_{\text {w}})\) principal case and adding modal formulas to the context naturally requires being able to weaken \(\Box \) and \(\lozenge \)-formulas in the antecedent (resp. succedent):
Similarly, the \((?_{\text {c}}/?_{\text {p}})\) key-case requires the ability to contract \(\Box /\lozenge \)-formulas.
We now give a formal definition of the linear-logical modal \(\mu \)-calculus:
Definition 6
(Linear-logical modal\(\mu \)-calculus) Pre-formulas of \(\mu \textsf {LL}_{\Box }^{\infty }\) are defined as:
We obtain positivity of an occurrence and the definition of formulas of \(\mu \textsf {LL}_{\Box }^{\infty }\) in the same way as for \(\mu \textsf {LL}^{\infty }\) and \(\mu \textsf {LK}_{\Box }^{\infty }\). Rules for \({\mu \textsf {LL}_{\Box }^{\infty }}\) are the rules for \(\mu \textsf {LL}^{\infty }\) together with those of Figure 8. Note that \((!_{\text {p}})\) (resp. \((?_{\text {p}})\)) is an instance of \((!_{\text {p}}^{\lozenge })\) (resp. \((?_{\text {p}}^{\Box })\)). We define the sequents, pre-proofs, and proofs as in Section 2.
Fig. 8.
Rules involving modalities for \(\mu \textsf {LL}_{\Box }^{\infty }\)
To justify the relevance of \(\mu \textsf {LL}_{\Box }^{\infty }\) we prove that there is a forgetful operation from \(\mu \textsf {LL}_{\Box }^{\infty }\) proofs to \(\mu \textsf {LK}_{\Box }^{\infty }\), the skeleton. We define a translation \(\textsc {SK}(-)\) from \(\mu \textsf {LL}_{\Box }^{\infty }\) formulas, rules and pre-proofs to \(\mu \textsf {LK}_{\Box }^{\infty }\) :
Definition 7
(\({\mu \textsf {LK}_{\Box }^{\infty }}\)-Skeleton) We define the skeleton of formulas inductively:
Sequents of \(\mu \textsf {LL}_{\Box }^{\infty }\) are translated to sequents of skeletons of these formulas. Translation of rules are standard. Translations of pre-proofs are obtained co-inductively by applying rule translations.
The following ensures that validity is preserved both ways by \(\textsc {SK}(-)\):
Proposition 1
(Robustness of the skeleton to validity) If \(\pi \) is a valid pre-proof, then \(\textsc {SK}(\pi )\) is a \(\mu \textsf {LK}_{\Box }^{\infty }\) valid pre-proof, and vice versa.
4 Cut-elimination for \(\mu \textsf {LL}_{\Box }^{\infty }\)
To eliminate cuts in \(\mu \textsf {LL}_{\Box }^{\infty }\), we employ a generalization of the cut inference called multicuts, as done in previous works on similar non-wellfounded proof systems [3, 4, 12, 28].
Definition 8
(Multicut rule) The multicut rule is the following rule:
It can have any number of premises. The ancestor relation \(\iota \) maps one formula of the conclusion to exactly one formula of the premises, while the \(\perp \!\!\!\perp \)-relation links cut-formulas together, subject to acyclicity and connectedness conditions.
Remark 3
The idea behind the multicut is to abstract a finite tree of binary cuts quotiented by the cut-commutation rule. We provide an example of a multicut rule and represent graphically \(\iota \) in red and \(\perp \!\!\!\perp \) in blue.
The multicut rule should be seen as a tree of binary cuts, cf (cut/mcut)-case:
Here, \(\iota '(p)=\iota (p)\) for positions of formulas sent to \(\mathcal {C}\), and uses the ancestor relation of the \(\text {cut}\)-rule together with \(\iota \) to determine the image of the other positions. The relation \(\perp \!\!\!\perp '\) is obtained from \(\perp \!\!\!\perp \) by adding \(p\perp \!\!\!\perp p'\), where p and \(p'\) are the positions of the two cut-formulas F.
4.1 The (mcut) reduction steps
As we use a multicut reduction strategy, we first describe the steps of reduction. To describe these mcut-steps of reduction, we will use a notation and a definition:
Notation 1
(\((!)\)-contexts) If \(\mathcal {C}\) is a list of \({\mu \textsf {LL}_{\Box }^{\infty }}\)-proofs, we denote by \(\mathcal {C}^{!/\Box }\) the list of proofs obtained by applying one of \((!_{\text {p}}^{\lozenge })\), \((?_{\text {p}}^{\Box })\), \((\Box _{\text {p}})\) or \((\lozenge _{\text {p}})\) rules to each proof of \(\mathcal {C}\). If \(\mathcal {C}\) is a list of \({\mu \textsf {LL}_{\Box }^{\infty }}\)-proofs, we denote by \(\mathcal {C}^\Box \) the list of proofs obtained by applying one of \((\Box _{\text {p}})\) or \((\lozenge _{\text {p}})\) rules to each proof of \(\mathcal {C}\).
Definition 9
(Restriction of a\(\textsf{mcut}\)context) Let
be a multicut occurrence such that \(\mathcal {C}= s_1~\dots ~ s_n\) with \(s_i := F_1, \dots , F_{k_i}\vdash G_1, \dots , G_{r_i}\). We define \(\mathcal {C}_{F_j}\) (resp. \(\mathcal {C}_{G_j}\)) to be the sequents \(\perp \!\!\!\perp \)-connected to the formula \(F_j\) (resp. \(G_j\)). This is extended to contexts of formulas with \(\mathcal {C}_\varGamma := \cup _{F\in \varGamma } \mathcal {C}_F\).
Fig. 9.
Examples of (mcut)-step of \(\mu \textsf {MALL}^{\infty }\)
The mcut-reduction steps of \(\mu \textsf {MALL}^{\infty }\) can be found in [4, 28]; we provide examples of these steps in Figure 9. The reduction steps for the exponential and modal fragment of \(\mu \textsf {LL}_{\Box }^{\infty }\) are presented in Figures 10 and 11, which include the exponential steps of \(\mu \textsf {LL}^{\infty }\). For commutative steps, we present only the cases where the principal formula of the rule being commuted appears in the succedent of the sequent. For principal steps, we present only the cases where the cut-formula is a \(?\)- or \(\lozenge \)-formula. All other cases can be derived by duality.
One side of the \(\mu \textsf {LL}_{\Box }^{\infty }\) exponential & modal principal cut-elimination steps – in all these proofs, \(\delta \in \{?, \lozenge \}\)
Definition 10
(Reduction sequence) A reduction sequence \((\pi _i)_{i\in 1+\lambda }\) (\(\lambda \in \omega +1\)) is a \(\rightsquigarrow \) sequence s.t. \(\pi _0\) contains at most one \(\mathsf {(mcut)}\) rule per branch.
We aim to prove that each reduction sequence converges to a cut-free proof. However, this theorem is not true as stated, even for infinite reduction sequences: one could apply infinitely many reductions only on some part of the proof, without reducing cuts in another part of the proof. Therefore, we need to be more precise, which motivates the following definition, directly borrowed from [3, 4] (the notion of residual is the usual one from rewriting):
Definition 11
(Fair reduction sequences [3, 4]) A mcut-reduction sequence \((\pi _i)_{i\in \omega }\) is fair if, for each \(\pi _i\) such that there is a reduction \(\mathcal {R}\) to a proof \(\pi '\), there exists a \(j>i\) such that \(\pi _j\) does not contain any residual of \(\mathcal {R}\).
We can now state our cut-elimination theorem:
Theorem 1
(Cut-elimination for\(\mu \textsf {LL}_{\Box }^{\infty }\)) Each fair \(\mathsf {(mcut)}\)-reduction se-quence of \(\mu \textsf {LL}_{\Box }^{\infty }\) valid proofs converges to a cut-free valid proof.
To prove it, we will translate formulas, proofs, and (mcut)-steps of \(\mu \textsf {LL}_{\Box }^{\infty }\) into \(\mu \textsf {LL}^{\infty }\) and use the following cut-elimination result from [28]:
Theorem 2
(Cut-elimination for\(\mu \textsf {LL}^{\infty }\) [28]) Every fair \((\text {mcut})\)-reduction sequence of \(\mu \textsf {LL}^{\infty }\) valid proofs converges to a cut-free valid proof.
Remark 4
In [28], exponential formulas, proofs, and cut-steps are encoded into \(\mu \textsf {MALL}^{\infty }\). We could have encoded \(\mu \textsf {LL}_{\Box }^{\infty }\) modalities into \(\mu \textsf {MALL}^{\infty }\), replaying the proof of [28] for cut-elimination. However, using the \(\mu \textsf {LL}^{\infty }\) cut-elimination theorem makes the result more modular and adaptable to future extensions of \(\mu \textsf {LL}^{\infty }\) validity conditions or cut-elimination variants.
4.2 Translation of \(\mu \textsf {LL}_{\Box }^{\infty }\) into \(\mu \textsf {LL}^{\infty }\)
We provide a translation of \(\mu \textsf {LL}_{\Box }^{\infty }\) into \(\mu \textsf {LL}^{\infty }\):
Definition 12
(Translation of\(\mu \textsf {LL}_{\Box }^{\infty }\)into\(\mu \textsf {LL}^{\infty }\)) The translation of formulas is defined inductively:
Translations of structural rules for modalities, \((\lozenge _{\text {c}})\), \((\lozenge _{\text {w}})\), \((\Box _{\text {c}})\) and \((\Box _{\text {w}})\) are respectively \((?_{\text {c}})\), \((?_{\text {w}})\), \((!_{\text {c} })\) and \((!_{\text {w}})\). Translations for the promotions \((!_{\text {p}}^{\lozenge })\) and \((?_{\text {p}}^{\Box })\) are respectively \((!_{\text {p}})\) and \((?_{\text {p}})\). Translations of the modal rules are given by:
Translations of other inference rules (r) are (r) themselves. Translations of pre-proofs are defined co-inductively using translations of rules.
The translation preserves the validity of pre-proof in both directions:
Lemma 1
(Validity robustness to\((-)^\circ \)translation) Let \(\pi \) be a \(\mu \textsf {LL}_{\Box }^{\infty }\) pre-proof. The proof \(\pi \) is valid if and only if the proof \(\pi ^\circ \) is valid.
Proof
Let B be a branch of \(\pi \). We have that B is validated by a thread \((A_i)\) if and only if \(B^\circ \) is validated by \((A^\circ _i)\), as the minimal recurring fixed point formula is a \(\nu \) on the right (resp. \(\mu \) on the left) in \((A_i)\) if and only if it is in \((A^\circ _i)\).
Finally, we need to ensure that \((\text {mcut})\)-reduction sequences are robust under this translation. In our proof of the final theorem, we also need one-step reduction rules to be simulated by a finite number of reduction steps in the translation.
Lemma 2
Consider a \(\mu \textsf {LL}_{\Box }^{\infty }\) reduction step \(\pi _0\rightsquigarrow \pi _1\). There exist a finite number of \(\mu \textsf {LL}^{\infty }\) proofs \(\theta _0, \dots , \theta _n\) such that: \(\pi _0^\circ = \theta _0 \rightarrow \theta _1\rightarrow \dots \rightarrow \theta _{n-1} \rightarrow \theta _n = \pi _1^{\circ }.\)
Proof (Proof sketch)
Reductions from the non-exponential part of \({\mu \textsf {LL}_{\Box }^{\infty }}\) translate easily to one step of reduction in \(\mu \textsf {LL}^{\infty }\). The same is true for the exponential part, except for the commutation of the modal rule. The translation of the left proof of this step is of the form (we only consider the case of \(\lozenge _{\text {p}}\); \(\Box _{\text {p}}\) is similar):
Here, we notice that for each dereliction on a cut-formula, there exists a corresponding promotion that will be erased by a dereliction/promotion key-case. The first promotion will therefore commute under the cut, and then each dereliction on formulas of the conclusion will commute as well. Each dereliction and each promotion on cut-formulas will be erased, giving us the correct translation .
Now that we know that a step of (mcut)-reduction in \(\mu \textsf {LL}_{\Box }^{\infty }\) translates to one or more \(\mu \textsf {LL}^{\infty }\) (mcut)-reduction steps, it is easy to translate each reduction sequence of \(\mu \textsf {LL}_{\Box }^{\infty }\) into a reduction sequence of \(\mu \textsf {LL}^{\infty }\). However, to use the cut-elimination theorem of \(\mu \textsf {LL}^{\infty }\), we need the reduction sequence to be fair. The purpose of the following lemma is to control the fairness of the translated reduction sequence:
Lemma 3
(Completeness of the (mcut)-reduction system) Let \(\pi \) and \(\pi '\) be two \(\mu \textsf {LL}_{\Box }^{\infty }\) proofs. If there is a \(\mu \textsf {LL}^{\infty }\)-redex \(\mathcal {R}\) sending \(\pi ^\circ \) to \(\pi '\), then there is also a \({\mu \textsf {LL}_{\Box }^{\infty }}\)-redex \(\mathcal {R}'\) sending \(\pi \) to a proof \(\pi ''\), such that in the translation of \(\mathcal {R}'\), \(\mathcal {R}\) is reduced.
Proof
We only prove the exponential cases, as the non-exponential cases are immediate. We have several cases:
If the case is the commutative step of a weakening (resp. contraction, resp. dereliction) (r), it necessarily means that (r) is the translation of a rule \((r')\) being a contraction (resp. weakening, resp. dereliction) which is also on top of a (mcut) in \(\pi \). We can take \(\mathcal {R}'\) as the step commuting \((r')\) under the cut.
If it is a principal case on a contraction or a weakening (r) on a formula \(?A\) (resp. \(!A\)), it means that each proof cut-connected to \(?A\) (resp. \(!A\)) ends with a promotion. As \(\pi ^\circ \) is the translation of a \({\mu \textsf {LL}_{\Box }^{\infty }}\)-proof, it means that (r) is the translation of a weakening or contraction rule \((r')\) on a formula \(?A'\) (resp. \(!A'\)) or \(\lozenge A'\) (resp. \(\Box A'\)) on top of a (mcut). It also means that all the proofs cut-connected to these formulas are promotions or modal rules (no other rules than a modal rule or a promotion in \({\mu \textsf {LL}_{\Box }^{\infty }}\) translates to a derivation ending with a promotion). Therefore, \(\mathcal {R'}\) is the principal case on \((r')\).
If it is a dereliction/promotion key case, the dereliction (resp. promotion) is the translation of a dereliction (resp. promotion). We take \(\mathcal {R}'\) to be the redex formed by these two rules.
If it is the commutative step of a promotion (r), it means that all the proofs of the contexts of the (mcut) are promotion rules. This means that all these rules come from the translation of promotion or modal rules. We need to ensure that each (mcut) with a context full of promotions or modal rules is covered by the (mcut)-reductions of \({\mu \textsf {LL}_{\Box }^{\infty }}\):
The commutation of \((!_{\text {p}}^{\lozenge })\) (or \((?_{\text {p}}^{\Box })\)) is covered by the first commutative case in Figure 10.
If it is a modal rule that is ready to be commuted, then other rules are necessarily modal rules and therefore is covered by the second commutative case in Figure 10.
We use the two previous lemmas, to prove the following:
Corollary 1
If \(\lambda \in \omega +1\) & \((\pi _i)_{i\in 1+\lambda }\) is a fair \(\mu \textsf {LL}_{\Box }^{\infty }\) reduction sequence, then:
there exists a fair \(\mu \textsf {LL}^{\infty }\) reduction sequence \((\theta _i)_{i\in 1+\lambda '}\) with \(\lambda '\in \omega +1\);
there exists a sequence of strictly increasing \((\varphi (i))_{i\in 1+\lambda }\) of elements of \(1+\lambda '\);
such that for each i, \(\theta _{\varphi (i)}=\pi _i^\circ \).
Proof
We construct the sequence by induction on the steps of \((\pi _i)_{i\in 1+\lambda }\).
For \(i=0\): \(\theta _0=\pi _0^\circ \) and \(\varphi (0)=0\):
For \(i+1\), suppose we have defined both sequences up to rank i. We use Lemma 2 on the step \(\pi _i \rightsquigarrow \pi _{i+1}\) to get a finite sequence of reduction \(\pi _i = \theta '_0 \rightsquigarrow \dots \rightsquigarrow \theta '_n = \pi _{i+1}\). We then construct both sequences by setting \(\varphi (i+1):=\varphi (i)+n, \quad \theta _{\varphi (i)+j} := {\theta '}_j\) (for \(j\in \llbracket 0, n\rrbracket \)).
Fairness of \((\theta _i)_{i\in 1+\lambda '}\) follows from Lemma 3 and from the fact that after the translation of an (mcut)-step, \(\pi ^\circ \rightsquigarrow {\pi '}^\circ \), each residual of a redex \(\mathcal {R}\) of \(\pi ^\circ \), is contained in the translations of residuals of the associated redex \(\mathcal {R}'\) of Lemma 3.
4.3 Cut-elimination for \(\mu \textsf {LL}_{\Box }^{\infty }\)
Finally, we can prove the main theorem of the section:
Proof
(of Theorem1). Let \((\pi _i)_{i\in 1+\lambda }\) be a fair \(\mu \textsf {LL}_{\Box }^{\infty }\) reduction sequence. We use Corollary 1 and get a fair \(\mu \textsf {LL}^{\infty }\) reduction sequence \((\theta _i)_{i\in 1+\lambda '}\) and a sequence \((\varphi (i))_{i\in 1+\lambda }\) of natural numbers. By Theorem 2, we know that \((\theta _i)_{i\in \omega }\) converges to a cut-free proof \(\theta \) of \(\mu \textsf {LL}^{\infty }\). Now suppose for the sake of contradiction that \((\pi _i)_{i\in 1+\lambda }\) does not converge to an \((\text {mcut})\)-free pre-proof. There is a j and a path p such that for each proof \(\pi _{j'}\), with \(j'\ge j\), there is an \((\text {mcut})\)-rule at the end of path p. This means that the translation of p leads to an \((\text {mcut})\) for each proof \(\theta _{j'}\) with \(j'\ge \varphi (j)\), contradicting the convergence of \((\theta _j)\) to a cut-free proof. Moreover \((\pi _i)\) converges to a pre-proof \(\pi \) such that \(\pi ^\circ =\theta \), since \(\theta _{\varphi (j)}\) equals \(\pi _j^\circ \) under multicuts. Since \(\theta \) is cut-free, \(\pi \) is both valid and cut-free by Lemma 1.
5 Cut-elimination of \(\mu \textsf {LK}_{\Box }^{\infty }\)
Fig. 12.
Translating the Modal Rule with Non-Empty Antecedent
We extend the linear translation of \(\mu \textsf {LK}^{\infty }\) from [28] to a translation from \(\mu \textsf {LK}_{\Box }^{\infty }\) into \(\mu \textsf {LL}_{\Box }^{\infty }\). The tentative translation of the modal formulas studied at the beginning of Section 3 actually only works with an empty antecedent. Adapting our example by adding an antecedent to it:
results in a derivation attempt as shown in Figure 12a. If \(\varGamma \) contains more than two formulas, \((?_{\text {p}})\) cannot be applied. However, adding an \(!\)-connective in the translation of \(\Box \)-formulas as
, allows us to complete the derivation (see Figure 12b).
Based on this, we define a translation from \(\mu \textsf {LK}_{\Box }^{\infty }\) into \(\mu \textsf {LL}_{\Box }^{\infty }\):
Definition 13
(Linear translation of\(\mu \textsf {LK}_{\Box }^{\infty }\)) The translation\({(-)}^{\bullet }\) from \(\mu \textsf {LK}_{\Box }^{\infty }\) formulas to \(\mu \textsf {LL}_{\Box }^{\infty }\) formulas is defined by induction on formulas:
Sequents are translated as \({(\varGamma \vdash \varDelta )}^{\bullet } := {\varGamma }^{\bullet }\vdash ?{\varDelta }^{\bullet }.\)
The following property must be kept in mind when defining rule translations and is proved by an induction the formulas of \(\mu \textsf {LK}_{\Box }^{\infty }\):
Proposition 2
For any \(\mu \textsf {LK}_{\Box }^{\infty }\) formula A, \({A}^{\bullet }\) is an \(!\)-formula.
We provide the translation of modal rules in Figure 13. We define translations of proofs coinductively using rule translations. As the smallest formula of a totally ordered set of translations is the translation of the smallest formula, and branches of \({\pi }^{\bullet }\) contain translations of threads from \(\pi \) and vice-versa, we have:
Lemma 4
(Robustness of\({(-)}^{\bullet }\)to validity) A pre-proof \(\pi \) is valid if and only if \({\pi }^{\bullet }\) is valid.
Fig. 13.
Linear translation of the modal rules
Lemma 5
(Composition of\(\textsc {SK}(-)\)and of\({(-)}^{\bullet }\)) For any \(\mu \textsf {LK}_{\Box }^{\infty }\) pre-proof \(\pi \), \(\textsc {SK}({\pi }^{\bullet })\) is equal to \(\pi \).
We define our rewriting system using the \(\textsc {SK}(-)\) translation:
Definition 14
((mcut)-rewriting system of\(\mu \textsf {LK}_{\Box }^{\infty }\)) The \(\mathsf {(mcut)}\)-rewriting system of \(\mu \textsf {LK}_{\Box }^{\infty }\) is defined as the (mcut)-system obtained from the \(\mu \textsf {LL}_{\Box }^{\infty }\) (mcut)-system by discarding the linear information of proofs in this system.
Finally, we have the following theorem:
Theorem 3
The reduction system of \(\mu \textsf {LK}_{\Box }^{\infty }\) is infinitary weakly-normalizing.
Proof
Consider a \(\mu \textsf {LK}_{\Box }^{\infty }\) proof \(\pi \) and a fair reduction sequence \(\sigma _{\textsf{L}}\) from \({\pi }^{\bullet }\). By Theorem 1, \(\sigma _{\textsf{L}}\) converges to a cut-free \(\mu \textsf {LL}_{\Box }^{\infty }\) proof. By applying \(\textsc {SK}(-)\) to each proof in the sequence, we obtain a sequence of valid \(\mu \textsf {LK}_{\Box }^{\infty }\) proofs such that either \(\textsc {SK}(\pi _i) = \textsc {SK}(\pi _{i+1})\) or \(\textsc {SK}(\pi _i)\) reduces to \(\textsc {SK}(\pi _{i+1})\) with one step of \(\mu \textsf {LK}_{\Box }^{\infty }\) mcut-reduction. We obtain a \(\mu \textsf {LK}_{\Box }^{\infty }\) cut-reduction sequence \(\sigma _{\textsf{K}}\) that is infinite and converges to a valid, cut-free \(\mu \textsf {LK}_{\Box }^{\infty }\) proof.
6 Conclusion
We have introduced \(\mu \textsf {LL}_{\Box }^{\infty }\), a linear version of the modal \(\mu \)-calculus, along with its circular and non-wellfounded proof systems. We have proved a cut-elimination theorem for fair cut-elimination reduction sequences, generalizing previous results on the non-wellfounded proof theory of linear logic. Through a linear translation of the circular and non-wellfounded proof systems for the modal \(\mu \)-calculus (\(\mu \textsf {LK}_{\Box }^{\infty }\)) to \(\mu \textsf {LL}_{\Box }^{\infty }\), we have obtained a cut-elimination theorem for the non-wellfounded sequent calculus of the modal \(\mu \)-calculus.
In our opinion, this work presents a new and interesting application of linear logic to the modal \(\mu \)-calculus, developing proof theories in both domains and highlighting the potential for cross-fertilization for the two communities. Indeed, this constitutes the first full syntactic cut-elimination theorem for a proof system modeling the full modal \(\mu \)-calculus.
Furthermore, the fine-grained cut-elimination inherited from linear logic opens up the possibility of developing a non-trivial cut-elimination equivalence on \(\mu \textsf {LK}_{\Box }^{\infty }\) proofs. This, in turn, could lead to the design of a denotational semantics for proofs of modal \(\mu \)-calculus, a question that was previously out of reach due to both the lack of a syntactic cut-elimination theorem and the absence of structure in proofs of the modal \(\mu \)-calculus.
However, this is not the first work studying both linear logic and modal logic. Notably, studies on modal logic S4 through linear logic have addressed both its intuitionistic fragment, proving cut-admissibility [13], and its classical version [19, 29]. Our work differs from these studies in two key aspects: (i) We employ a non-wellfounded setting. (ii) The logic S4 treats modalities as linear logic exponentials with a standard promotion and dereliction, making it a sub-system of the subexponentials [23]. Our work is different because we use a functorial promotion for modal rules, which requires us to examine the interaction between functorial and non-functorial promotion.
An important direction for future work is to explore whether our linear-logical modal mu-calculus can be adapted to wellfounded proof-systems of linear logic with fixed-points in a \(\mu \textsf {LL}_{\Box }\) sequent calculus. We aim to investigate if our methodology can be extended to obtain a cut-elimination theorem for the finitary modal \(\mu \)-sequent calculus via a linear translation from \(\mu \textsf {LK}_{\Box }\) to \(\mu \textsf {LL}_{\Box }\), building upon Baelde’s results [2]. This question presents significant challenges due to the complex structure of fixed-point rules in finitary \(\mu \textsf {LL}\). While omitting linear information from \(\mu \textsf {LL}_{\Box }\) proofs should yield \(\mu \textsf {LK}_{\Box }\) proofs that simulate cut-elimination, designing a linear translation from \(\mu \textsf {LK}_{\Box }\) to \(\mu \textsf {LL}_{\Box }\) that commutes with cut-elimination, as shown in this paper, remains a non-trivial task.
From the linear logic-theoretic point of view, our system \(\mu \textsf {LL}_{\Box }^{\infty }\) can be viewed as a linear logic with two sets of exponential modalities satisfying different structural rules and exponentials. This is akin to so-called light logics [15, 18], that are variants of linear logics developed by taming the power of exponential modalities in order to control the complexity of cut-elimination (for instance constraining the \(?\)-context of a promotion to be immediately derelicted after a promotion ensures that typable programs have at most elementary complexity [15]).
Building on these ideas, we propose to develop a uniform framework for proving cut elimination in wellfounded proof systems of linear logic fragments that encompass both light logics and modal logics. This framework could be inspired by the subexponential system of Nigam & Miller [23] and the first author with Laurent [5], but extended to include functorial promotion. Such a system would allow us to treat light logics and our linear-logical modal mu-calculus as instances of a more general linear logic system.
In a similar direction, we shall investigate whether our approach of reducing cut-elimination to that of simpler systems can be useful for the circular approaches to session types [11, 31] as well as to the study of productivity and normalization properties in functional reactive programming [8].
Funding. This work was partially funded by the ANR project RECIPROG, project reference ANR-21-CE48-019-01.
Acknowledgments
The authors would like to thank the anonymous reviewers for their constructive and valuable comments, as well as Anupam Das, Abhishek De, Farzad Jafarrahmani, Johannes Kloibhofer, Paul-André Melliès and Bahareh Afshari for fruitful discussions on this work.
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Note that allowing modal rules in contexts containing \(?\) on the right and \(!\) on the left would also solve our problem. However, forgetting the linear information of such a rule would not give us a rule derivable in \(\mu \textsf {LK}_{\Box }^{\infty }\).
[10, 14]. Further analyses on these exponential modalities led to the discovery of light logics, where the complexity of cut-elimination is tamed in a flexible way, usually by considering alternative, weaker exponential modalities.
for any permutations \(\sigma \) and \(\sigma '\) of \(\{ 1,\dots , \#(\varDelta )\}\) and \(\{ 1,\dots , \#(\varGamma )\}\) respectively, where \(\sigma (\varDelta )\) designates the action of \(\sigma \) on the list \(\varDelta \), with the induced ancestor relation. In the rest of the article, we will intentionally treat the exchange rule implicitly: the reader can consider that each of our rules are preceded and followed by a finite number of rule \((\text {ex})\).
, with \(a\in \mathcal {A}, X\in \mathcal {V}\). Positivity of pre-formulas and \(\mu \textsf {LL}^{\infty }\) formulas are defined in the same way as for \(\mu \textsf {LK}_{\Box }^{\infty }\). The \(\{!, ?\}\)-free formulas of \(\mu \textsf {LL}^{\infty }\) are the formulas of \(\mu \textsf {MALL}^{\infty }\). The \(\{\mu ,\nu , X\}\)-free fragment of formulas of \(\mu \textsf {LL}^{\infty }\) are the formulas of linear logic \({\textsf {LL}}\). The intersection of these two fragments is \(\textsf {MALL}\).
Following the standard sequent translation from \(\textsf {LK}\) to \(\textsf {LL}\), we need to derive \(\vdash ?!\Box ?{A}^{\bullet }, ?!\lozenge ?{B}^{\bullet }\) from the premise \(\vdash ?{A}^{\bullet }, ?{B}^{\bullet }\). Reasoning bottom-up: to conclude \(\vdash ?{A}^{\bullet }, ?{B}^{\bullet }\), we must remove both the \(\lozenge \) and the \(\Box \) with a modal rule. However, regardless of the sequence of rules used, we always end up with a sequent containing an \(!\) together with either \(\Box \) or \(\lozenge \). An example of such a derivation is shown in Figure 7a. In our attempt to translate this rule, we are left with an unprovable sequent: indeed, the top sequent cannot be the conclusion of any rule in the system (except for cut and exchange, of course): \(!\Box ?{A}^{\bullet }\) cannot be principal since there is a \(\lozenge \)-formula in the context, and \(\lozenge ?{B}^{\bullet }\) cannot be principal since there is an \(!\)-formula.
be a multicut occurrence such that \(\mathcal {C}= s_1~\dots ~ s_n\) with \(s_i := F_1, \dots , F_{k_i}\vdash G_1, \dots , G_{r_i}\). We define \(\mathcal {C}_{F_j}\) (resp. \(\mathcal {C}_{G_j}\)) to be the sequents \(\perp \!\!\!\perp \)-connected to the formula \(F_j\) (resp. \(G_j\)). This is extended to contexts of formulas with \(\mathcal {C}_\varGamma := \cup _{F\in \varGamma } \mathcal {C}_F\).
results in a derivation attempt as shown in Figure 12a. If \(\varGamma \) contains more than two formulas, \((?_{\text {p}})\) cannot be applied. However, adding an \(!\)-connective in the translation of \(\Box \)-formulas as
, allows us to complete the derivation (see Figure 12b).
