A Note on Switching Conditions for the Generalized Logical Connectives in Multiplicative Linear Logic
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2018
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866914284130271232 |
|---|---|
| author | Nishimuta, Yuki Okada, Mitsuhiro |
| author_facet | Nishimuta, Yuki Okada, Mitsuhiro |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_1804_02540 |
| institution | arXiv |
| publishDate | 2018 |
| record_format | arxiv |
| spellingShingle | A Note on Switching Conditions for the Generalized Logical Connectives in Multiplicative Linear Logic Nishimuta, Yuki Okada, Mitsuhiro Logic 03F52, 03F05 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. |
| title | A Note on Switching Conditions for the Generalized Logical Connectives in Multiplicative Linear Logic |
| topic | Logic 03F52, 03F05 |
| url | https://arxiv.org/abs/1804.02540 |