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.

翻译：线性逻辑为证明论、指称语义学以及编程语言研究提供了新视角。其主要成就之一是证明网——位于逻辑与图论交叉点的证明的规范表示。对于无单位的乘法线性逻辑（MLL）这一极简证明系统而言，这两个方面完全融合：该系统的证明网是满足正确性准则的图，且该准则可完全用图的语言表达。但对于更富表达力的逻辑系统（包含逻辑常量、量词和指数模态），情况并非完全如此。证明网的纯图方法剥夺了其任何序列结构，而这种结构对于表示参数呈现的顺序至关重要——这正是这些扩展系统所必需的。因此，重建这种呈现顺序（即对图进行序列化）是图具有逻辑属性的必要条件。确保序列化得以实现的构件（如盒子或跳跃）的呈现与研究，是线性逻辑研究的重要组成部分。Faggian与di Giamberardino深入研究的跳跃，能够表达从相继式演算证明到完全去序列化证明网之间的中间序列化程度。我们建议通过将跳跃内化到MLL的扩展中来分析其逻辑强度：在该扩展中，关于特定公式（跳跃公式）的公理对可能的序列化施加约束。跳跃公式需进行非线性处理——这可通过公理化方式实现，或将其嵌入乘法指数线性逻辑的高度受限片段，从而揭示序列化的指数逻辑。