Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Note on Switching Conditions for the Generalized Logical Connectives in Multiplicative Linear Logic

Yuki Nishimuta, Mitsuhiro Okada

TL;DR

The paper addresses how to extend switching conditions to generalize multiplicative connectives in ${\mathsf{MLL}}$ to $n$-ary forms. It introduces partition switching, a natural extension that mirrors the partition structure of $n$-ary connectives, and shows that Laurent's sequentialization proof for binary connectives extends to these generalized connectives under partition switching. A key result is that partition switching yields sequentialization but loses the expansion property, while Danos–Regnier switching preserves expansion but fails to guarantee sequentialization in general; only the purely tensor-based or purely par-based cases can satisfy both. This clarifies a fundamental trade-off in designing switching conditions for generalized connectives and informs future work on proof-nets and cut-elimination in extended linear logic.

Abstract

Danos and Regnier (1989) introduced the par-switching condition for multiplicative proof-structures and simplified the sequentialization theorem of Girard (1987) by means of par-switching. Danos and Regnier (1989) also generalized the par-switching to a switching for n-ary connectives (hereafter called an n-ary switching) and showed that the "expansion" property holds, namely that any "excluded-middle" formula admits a correct proof-net in the sense of their n-ary switching. They added a remark that the sequentialization theorem does not hold with their switching. Their definition of switching for n-ary connectives is a natural generalization of the original switching for the binary connectives. However, there are many other possible definitions of switching for n-ary connectives. We give an alternative and "natural" definition of n-ary switching, and we show that the proof of sequentialization theorem by Olivier Laurent with the par-switching works for our n-ary switching; Consequently, the sequentialization theorem holds for our n-ary switching. On the other hand, we remark that the "expansion" property no longer holds under our switching anymore. We point out that no definition of n-ary switching satisfies both the sequentialization theorem and the "expansion" property at the same time except for the purely tensor-based (or purely par-based) connectives.

A Note on Switching Conditions for the Generalized Logical Connectives in Multiplicative Linear Logic

TL;DR

The paper addresses how to extend switching conditions to generalize multiplicative connectives in to -ary forms. It introduces partition switching, a natural extension that mirrors the partition structure of -ary connectives, and shows that Laurent's sequentialization proof for binary connectives extends to these generalized connectives under partition switching. A key result is that partition switching yields sequentialization but loses the expansion property, while Danos–Regnier switching preserves expansion but fails to guarantee sequentialization in general; only the purely tensor-based or purely par-based cases can satisfy both. This clarifies a fundamental trade-off in designing switching conditions for generalized connectives and informs future work on proof-nets and cut-elimination in extended linear logic.

Abstract

Danos and Regnier (1989) introduced the par-switching condition for multiplicative proof-structures and simplified the sequentialization theorem of Girard (1987) by means of par-switching. Danos and Regnier (1989) also generalized the par-switching to a switching for n-ary connectives (hereafter called an n-ary switching) and showed that the "expansion" property holds, namely that any "excluded-middle" formula admits a correct proof-net in the sense of their n-ary switching. They added a remark that the sequentialization theorem does not hold with their switching. Their definition of switching for n-ary connectives is a natural generalization of the original switching for the binary connectives. However, there are many other possible definitions of switching for n-ary connectives. We give an alternative and "natural" definition of n-ary switching, and we show that the proof of sequentialization theorem by Olivier Laurent with the par-switching works for our n-ary switching; Consequently, the sequentialization theorem holds for our n-ary switching. On the other hand, we remark that the "expansion" property no longer holds under our switching anymore. We point out that no definition of n-ary switching satisfies both the sequentialization theorem and the "expansion" property at the same time except for the purely tensor-based (or purely par-based) connectives.

Paper Structure

This paper contains 5 sections, 8 theorems, 1 equation, 7 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Partition switching for the sequentialization theorem
  4. Conclusions
  5. Appendix

Key Result

Lemma 1

DR For any $n$-ary connectives $\mathcal{C}_1$ and $\mathcal{C}_2$, the main cut-elimination step holds for any cut between any of the introduction rules for $\mathcal{C}_1$ and any of the introduction rules for $\mathcal{C}_2$ if and only if the corresponding partition[ sets] are orthogonal.

Figures (7)

  • Figure 1: Example of the partition switching
  • Figure 2: Figure representing the proof argument of the case $n>1$
  • Figure 3: Example of Danos-Regnier switching
  • Figure 4: Axiom expansion : the upper diagram is expanded to the lower diagram.
  • Figure 5: Inference rules of $\mathsf{MLL}$
  • ...and 2 more figures

Theorems & Definitions (34)

  • Definition 1
  • Definition 2
  • Definition 3
  • Definition 4
  • Definition 5
  • Lemma 1
  • Proposition 1
  • Definition 6
  • Definition 7
  • Definition 8
  • ...and 24 more