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 的扩展中分析其逻辑强度，其中特定公式（跳跃公式）上的公理引入了对可能顺序化的约束。跳跃公式需以非线性方式处理，我们采用公理化方式，或将其嵌入乘法指数线性逻辑的受控片段中，从而揭示顺序化的指数逻辑。