The exponential logic of sequentialization
Aurore Alcolei, Luc Pellissier, Alexis Saurin
TL;DR
This work tackles the problem of capturing sequential order in proof nets for expressive linear-logics, where purely graphical representations lose the sequencing encoded by sequent calculi. It introduces a logical mechanism for sequencing—graphical jumps—by internalizing them as axioms via a new atom $oldsymbol{J}$ in an extended system $ extsf{MLL}_{oldsymbol{J}}$, and shows that jumps precisely correspond to constraints on sequentializations relative to a jump pair $(F,F')$. The paper then extends the idea to multiple jumps through contractions, establishes a bisimulation with cut-elimination dynamics, and proves a correction criterion that aligns with the Danos–Regnier criterion after erasure. Finally, it demonstrates how to realize jumps inside $ extsf{MELL}$ with Mix by encoding $oldsymbol{J}$ and $oldsymbol{J}^{ot}$ using exponentials and discusses the implications for extending sequentialization results to richer logics. The results provide a principled, logical bridge between graph-theoretic proof nets and sequent-calculus sequencing, with potential applications to broader linear-logics and a clearer understanding of sequentialization mechanisms.
Abstract
Linear logic has provided new perspectives on proof-theory, denotational semantics and the study of programming languages. One of its main successes are proof-nets, canonical representations of proofs that lie at the intersection between logic and graph theory. In the case of the minimalist proof-system of multiplicative linear logic without units (MLL), these two aspects are completely fused: proof-nets for this system are graphs satisfying a correctness criterion that can be fully expressed in the language of graphs. For more expressive logical systems (containing logical constants, quantifiers and exponential modalities), this is not completely the case. The purely graphical approach of proof-nets deprives them of any sequential structure that is crucial to represent the order in which arguments are presented, which is necessary for these extensions. Rebuilding this order of presentation - sequentializing the graph - is thus a requirement for a graph to be logical. Presentations and study of the artifacts ensuring that sequentialization can be done, such as boxes or jumps, are an integral part of researches on linear logic. Jumps, extensively studied by Faggian and di Giamberardino, can express intermediate degrees of sequentialization between a sequent calculus proof and a fully desequentialized proof-net. We propose to analyze the logical strength of jumps by internalizing them in an extention of MLL where axioms on a specific formula, the jumping formula, introduce constrains on the possible sequentializations. The jumping formula needs to be treated non-linearly, which we do either axiomatically, or by embedding it in a very controlled fragment of multiplicative-exponential linear logic, uncovering the exponential logic of sequentialization.