It has been known for a while that the exponential modalities of linear logic may be simulated by least and greatest fixed point operators. However it is apparently not widely known whether this simulation is faithful. In this post we explain that this is not the case, using only first principles of linear logic.

### Linear logic

It would not be reasonable to recap all the foundations and motivations of linear logic here, so I will be brief. But let me first give some helpful pointers for further background. A good is the SEP article [1]. Unfortunately there is (still!) no textbook on linear logic that I am aware of, but Dale Miller and Roberto Di Cosmo (the authors of the SEP article) each have produced some publicly available lecture notes, here and here respectively. There is always the original TCS paper of Jean-Yves Girard too [2].

#### Multiplicative additive linear logic

In a nutshell, (exponential-free) linear logic decomposes the usual conjunction and disjunction connectives of classical propositional logic (CPL) into so-called *additive* and *multiplicative* versions:

Disjunction | Conjunction | |

Multiplicative | ||

Additive |

Each connective also comes with its own unit, for respectively. Of course these distinctions only make sense because linear logic is substructural [3]: it does not admit weakening and contraction in general (although exchange is typically permitted). Thus cedents should be construed as *multisets*, rather than lists or sets. At least one advantage of these sensitivities is that they play well with cut-elimination, admitting a more resource-sensitive analysis of normalisation via the Curry-Howard correspondence.

Note that linear logic is, by default, classical, with the additive connectives and multiplicative connectives respectively enjoying their own De Morgan dualities. In this way negation of a formula , written , can be reduced to atomic formulas by equalities and so on; indeed this explains the one-sided presentation of the rules as above.

#### Exponentials

Now comes the funky part: exponentials! These allow us to recover structural behaviour, weakening and contraction, in a controlled manner:

Adding the exponentials to yields full (first-order, propositional) linear logic .

At first glance the exponentials look an awful lot like modalities [4]. Indeed the laws of the ! and ? are just those of S4 modalities, and respectively, along with structural rules. Exponentials also give us a way to relate the multiplicative and additive connectives, just like exponentiation in arithmetic relates addition and multiplication, namely by the ‘exponential isomorphism‘ .

#### The problem of non-canonicity

One interesting aspect of the exponentials is that they are not *canonical*: if we introduce copies of the exponentials, say satisfying the same respective laws as , we cannot prove that necessarily and on this basis alone (see Section 6.1 of [1]). This is in stark contrast with the multiplicative and additive connectives, which are indeed canonical in this way.

### An interpretation of the exponentials by fixed points

The recovery of structural behaviour by exponentials allows for complex cut-elimination behaviour. For instance, we can embed all of intuitionistic propositional logic (IPL) into by Girard’s embedding, which in particular interprets (where ). However, this is not the only way to recover such behaviours. An alternative is via extremal *fixed points*.

#### Least and greatest fixed points

We may expand the syntax of formulas to allow expressions of the form and , where is a propositional variable. Very roughly the intended reading is as the least and greatest fixed points, respectively, of . This is formalised by their inference rules:

The system , extending by the rules above, was introduced and studied by David Baelde and Dale Miller in [5] and [6].

Under duality of and , i.e. (and symmetrically), these rules are induced from the ‘least prefixed point’ reading of (dually, ‘greatest postfixed point’ for ), à la Knaster-Tarski. Similar rules and axioms are found across mathematical and computational logic, for instance in extensions of Peano Arithmetic by inductive definitions. In linear logic fixed points are best understood in Curry-Howard style. For instance we can write a type of natural numbers , and then a type of streams, . Further examples can be found in [7].

#### Simulating exponentials with fixed points

More interestingly, we can interpret the exponentials themselves as fixed points!

It is not hard to see that all the rules for exponentials can be derived for the encodings above, crucially using coinduction (i.e. the rule) to simulate promotion (i.e. the ! rule). Writing for the extension of by both exponentials and fixed points, we have:

Proposition 1.([6]) If then .

### Non-faithfulness via non-canonicity

Can we establish a converse to Proposition 1 above? This question was left open by Baelde in [6], and seems to generally have been a curiosity within the community over the last 15 years or so. At least one reason to believe this should not be the case is that fixed points are, in a sense, canonical by their extremal characterisations. It turns out we can make this intuition precise.

#### An induction principle

does not only satisfy the rules of , it is designed to be the *least *such formula. Write for, informally, ‘ is a ?-exponential of ‘. Formally:

Since is the ‘least ?-exponential’ of , we can prove that it implies any other ?-exponential of :

Proposition 2..

**Proof.** By induction on (equivalently coinduction on ), with invariant .

#### Separation via proof search

On the other hand, as one might expect, we cannot prove a similar property for the usual ?:

Proposition 3..

**Proof.** By analysis of cut-free .

So we have identified a separating formula! Indeed, the usual exponentials cannot simulate their fixed point encodings respectively in linear logic. Note that, though the separation above makes use of the exponentials themselves, as contains both and their fixed point encodings , it can be made exponential-free by Proposition 1.

Corollary 4.There is a formula , with all exponentials distinguished, such that but .

### Conclusions

In hindsight, the separation above is quite natural and hardly seems surprising. This is a good thing! It is reassuring when something turns out to be ‘obvious’ all along, not least as it emphasises the correct intuitions, which were certainly clear from various previous works, e.g. [5], [6], [8], [9].

The argument for non-provability of in was via cut-free proof search, but it would be nice to construct an appropriate countermodel by way of phase semantics [10] (see also the recent [9] for phase semantics of variations of ). In a more proof relevant direction, it would be interesting to further examine this separation from a Curry-Howard viewpoint: what are the inhabitants of and , that are not typed by and , respectively? I understand that these last two directions are the subject of ongoing investigations by Abhishek De, Farzad Jafarrahmani and Alexis Saurin.

#### Acknowledgements

I would like to thank David Baelde, Eben Blaisdell, Kostia Chardonnet, Gianluca Curzi, Abhishek De, Dale Miller and Alexis Saurin for several interesting conversations leading to the observations in this post, in particular during LICS ’23 in Boston.

### References

[Bibtex]

```
@InCollection{sep-logic-linear,
author = {Di Cosmo, Roberto and Miller, Dale},
title = {{Linear Logic}},
booktitle = {The {Stanford} Encyclopedia of Philosophy},
editor = {Edward N. Zalta and Uri Nodelman},
howpublished = {\url{https://plato.stanford.edu/archives/fall2023/entries/logic-linear/}},
year = {2023},
edition = {Fall 2023},
publisher = {Metaphysics Research Lab, Stanford University}
}
```

```
@article{Girard87,
author = {Jean-Yves Girard},
title = {Linear Logic},
journal = {Theor. Comput. Sci.},
volume = {50},
pages = {1--102},
year = {1987},
url = {https://doi.org/10.1016/0304-3975(87)90045-4},
doi = {10.1016/0304-3975(87)90045-4},
timestamp = {Wed, 17 Feb 2021 22:00:41 +0100},
biburl = {https://dblp.org/rec/journals/tcs/Girard87.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
```

[Bibtex]

```
@InCollection{sep-logic-substructural,
author = {Restall, Greg},
title = {{Substructural Logics}},
booktitle = {The {Stanford} Encyclopedia of Philosophy},
editor = {Edward N. Zalta},
howpublished = {\url{https://plato.stanford.edu/archives/spr2018/entries/logic-substructural/}},
year = {2018},
edition = {{S}pring 2018},
publisher = {Metaphysics Research Lab, Stanford University}
}
```

[Bibtex]

```
@InCollection{sep-logic-modal,
author = {Garson, James},
title = {{Modal Logic}},
booktitle = {The {Stanford} Encyclopedia of Philosophy},
editor = {Edward N. Zalta and Uri Nodelman},
howpublished = {\url{https://plato.stanford.edu/archives/spr2024/entries/logic-modal/}},
year = {2024},
edition = {{S}pring 2024},
publisher = {Metaphysics Research Lab, Stanford University}
}
```

[Bibtex]

```
@inproceedings{BaeldeMiller07,
author = {David Baelde and
Dale Miller},
editor = {Nachum Dershowitz and
Andrei Voronkov},
title = {Least and Greatest Fixed Points in Linear Logic},
booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning, 14th
International Conference, {LPAR} 2007, Yerevan, Armenia, October 15-19,
2007, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {4790},
pages = {92--106},
publisher = {Springer},
year = {2007},
url = {https://doi.org/10.1007/978-3-540-75560-9\_9},
doi = {10.1007/978-3-540-75560-9\_9},
timestamp = {Sat, 09 Apr 2022 12:44:41 +0200},
biburl = {https://dblp.org/rec/conf/lpar/BaeldeM07.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
```

[Bibtex]

```
@article{Baelde12,
author = {David Baelde},
title = {Least and Greatest Fixed Points in Linear Logic},
journal = {{ACM} Trans. Comput. Log.},
volume = {13},
number = {1},
pages = {2:1--2:44},
year = {2012},
url = {https://doi.org/10.1145/2071368.2071370},
doi = {10.1145/2071368.2071370},
timestamp = {Tue, 06 Nov 2018 12:51:53 +0100},
biburl = {https://dblp.org/rec/journals/tocl/Baelde12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
```

[Bibtex]

```
@InProceedings{BDS16,
author = {Baelde, David and Doumane, Amina and Saurin, Alexis},
title = {{Infinitary Proof Theory: the Multiplicative Additive Case}},
booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
pages = {42:1--42:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-022-4},
ISSN = {1868-8969},
year = {2016},
volume = {62},
editor = {Talbot, Jean-Marc and Regnier, Laurent},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.42},
URN = {urn:nbn:de:0030-drops-65825},
doi = {10.4230/LIPIcs.CSL.2016.42},
annote = {Keywords: Infinitary proofs, linear logic}
}
```

[Bibtex]

```
@inproceedings{Saurin23,
author = {Alexis Saurin},
editor = {Revantha Ramanayake and
Josef Urban},
title = {A Linear Perspective on Cut-Elimination for Non-wellfounded Sequent
Calculi with Least and Greatest Fixed-Points},
booktitle = {Automated Reasoning with Analytic Tableaux and Related Methods - 32nd
International Conference, {TABLEAUX} 2023, Prague, Czech Republic,
September 18-21, 2023, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {14278},
pages = {203--222},
publisher = {Springer},
year = {2023},
url = {https://doi.org/10.1007/978-3-031-43513-3\_12},
doi = {10.1007/978-3-031-43513-3\_12},
timestamp = {Wed, 01 Nov 2023 08:59:02 +0100},
biburl = {https://dblp.org/rec/conf/tableaux/Saurin23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
```

[Bibtex]

```
@InProceedings{DJS22,
author = {De, Abhishek and Jafarrahmani, Farzad and Saurin, Alexis},
title = {{Phase Semantics for Linear Logic with Least and Greatest Fixed Points}},
booktitle = {42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022)},
pages = {35:1--35:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-261-7},
ISSN = {1868-8969},
year = {2022},
volume = {250},
editor = {Dawar, Anuj and Guruswami, Venkatesan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2022.35},
URN = {urn:nbn:de:0030-drops-174272},
doi = {10.4230/LIPIcs.FSTTCS.2022.35},
annote = {Keywords: Linear logic, fixed points, phase semantics, closure ordinals, cut elimination}
}
```

[Bibtex]

```
@inproceedings{Girard95,
title={Linear logic: its syntax and semantics},
author={Girard, Jean-Yves},
booktitle={Proceedings of the workshop on Advances in linear logic},
pages={1--42},
year={1995}
}
```