Cut-Expansion in Proof-Nets of Multiplicative Linear Logic
Rémi Di Guardia
IRIF, Paris Cité
https://www.irif.fr/~diguardia/
Date(s) : 09/10/2025 iCal
11h00 - 12h30
Cut-elimination is a rewriting system defined in many logics, which has been widely studied. In general, a major result is to prove its weak normalization, which implies a provable formula always admits a cut-free proof. From this, various results can be more easily deduced: for instance that there is no proof of false. However, the reverse procedure – that we call cut-expansion – has been much less studied even though it is also useful! A goal here is the following: given a proof π with many cuts, can we find a proof π’ with exactly one cut at its root and that reduces to π? Such a result has two applications. First, it allows to find a Kraig’s interpolant in the spirit of [Sau25,FOS25]. It is also useful in the case of a denotational semantic: while it is often clear how to interpret a single cut-rule between two proofs, it may not be the case for two proofs linked by « a bunch » of cut-rules – this problem was encountered e.g. in [EFP24].
We will present a very simple proof on how to apply cut-expansion steps to obtain only one cut-rule from a proof with many cut-rules in Multiplicative Linear Logic. We do so in the proof-net syntax as the proof is really easy to intuit in this formalism. We then use this result to immediately get a proof of Kraig’s interpolation. Lastly, and if time allows, we sketch how to extend our proof to full linear logic.
[Sau25] Alexis Saurin. Interpolation as Cut-Introduction: On the Computational Content of Craig-Lyndon Interpolation. FSCD 2025. https://doi.org/10.4230/LIPIcs.FSCD.2025.32
[FOS25] Guido Fiorillo, Daniel Osorio Valencia, and Alexis Saurin. On Correctness, Sequentialization and Interpolation. TLLA 2025.
[EFP24] Thomas Ehrhard, Claudia Faggian, and Michele Pagani. Bayesian Networks and Proof-Nets: a proof-theoretical account of Bayesian Inference. Technical Report. https://doi.org/10.48550/arXiv.2412.20540
Catégories
