On noncommutative extensions of linear logic
Pomset logic introduced by Retor\'e is an extension of linear logic with a self-dual noncommutative connective. The logic is defined by means of proof-nets, rather than a sequent calculus. Later a deep inference system BV was developed with an eye to capturing Pomset logic, but equivalence of s...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2019-09-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/3765/pdf |
| _version_ | 1827322787901997056 |
|---|---|
| author | Sergey Slavnov |
| author_facet | Sergey Slavnov |
| author_sort | Sergey Slavnov |
| collection | DOAJ |
| description | Pomset logic introduced by Retor\'e is an extension of linear logic with a
self-dual noncommutative connective. The logic is defined by means of
proof-nets, rather than a sequent calculus. Later a deep inference system BV
was developed with an eye to capturing Pomset logic, but equivalence of system
has not been proven up to now. As for a sequent calculus formulation, it has
not been known for either of these logics, and there are convincing arguments
that such a sequent calculus in the usual sense simply does not exist for them.
In an on-going work on semantics we discovered a system similar to Pomset
logic, where a noncommutative connective is no longer self-dual. Pomset logic
appears as a degeneration, when the class of models is restricted. Motivated by
these semantic considerations, we define in the current work a semicommutative
multiplicative linear logic}, which is multiplicative linear logic extended
with two nonisomorphic noncommutative connectives (not to be confused with very
different Abrusci-Ruet noncommutative logic). We develop a syntax of proof-nets
and show how this logic degenerates to Pomset logic. However, a more
interesting problem than just finding yet another noncommutative logic is to
find a sequent calculus for this logic. We introduce decorated sequents, which
are sequents equipped with an extra structure of a binary relation of
reachability on formulas. We define a decorated sequent calculus for
semicommutative logic and prove that it is cut-free, sound and complete. This
is adapted to "degenerate" variations, including Pomset logic. Thus, in
particular, we give a variant of sequent calculus formulation for Pomset logic,
which is one of the key results of the paper. |
| first_indexed | 2024-04-25T01:34:27Z |
| format | Article |
| id | doaj.art-63da3bf9cfd24c4b97a9c629f069fc35 |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:34:27Z |
| publishDate | 2019-09-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-63da3bf9cfd24c4b97a9c629f069fc352024-03-08T10:28:03ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742019-09-01Volume 15, Issue 310.23638/LMCS-15(3:30)20193765On noncommutative extensions of linear logicSergey SlavnovPomset logic introduced by Retor\'e is an extension of linear logic with a self-dual noncommutative connective. The logic is defined by means of proof-nets, rather than a sequent calculus. Later a deep inference system BV was developed with an eye to capturing Pomset logic, but equivalence of system has not been proven up to now. As for a sequent calculus formulation, it has not been known for either of these logics, and there are convincing arguments that such a sequent calculus in the usual sense simply does not exist for them. In an on-going work on semantics we discovered a system similar to Pomset logic, where a noncommutative connective is no longer self-dual. Pomset logic appears as a degeneration, when the class of models is restricted. Motivated by these semantic considerations, we define in the current work a semicommutative multiplicative linear logic}, which is multiplicative linear logic extended with two nonisomorphic noncommutative connectives (not to be confused with very different Abrusci-Ruet noncommutative logic). We develop a syntax of proof-nets and show how this logic degenerates to Pomset logic. However, a more interesting problem than just finding yet another noncommutative logic is to find a sequent calculus for this logic. We introduce decorated sequents, which are sequents equipped with an extra structure of a binary relation of reachability on formulas. We define a decorated sequent calculus for semicommutative logic and prove that it is cut-free, sound and complete. This is adapted to "degenerate" variations, including Pomset logic. Thus, in particular, we give a variant of sequent calculus formulation for Pomset logic, which is one of the key results of the paper.https://lmcs.episciences.org/3765/pdfcomputer science - logic in computer sciencemathematics - logic |
| spellingShingle | Sergey Slavnov On noncommutative extensions of linear logic Logical Methods in Computer Science computer science - logic in computer science mathematics - logic |
| title | On noncommutative extensions of linear logic |
| title_full | On noncommutative extensions of linear logic |
| title_fullStr | On noncommutative extensions of linear logic |
| title_full_unstemmed | On noncommutative extensions of linear logic |
| title_short | On noncommutative extensions of linear logic |
| title_sort | on noncommutative extensions of linear logic |
| topic | computer science - logic in computer science mathematics - logic |
| url | https://lmcs.episciences.org/3765/pdf |
| work_keys_str_mv | AT sergeyslavnov onnoncommutativeextensionsoflinearlogic |