Permutative logic (PL) is a noncommutative variant of multiplicative linear logic (MLL) arising from recent investigations concerning the topology of linear proofs. Permutative sequents are structured as oriented surfaces with boundary whose topological complexity is able to encode some information about the exchange in sequential proofs. In this paper we provide a complete permutative sequent calculus by extending that one of PL with rules for additives and exponentials. This extended system, here called permutative linear logic (PLL), is shown to be a conservative extension of linear logic and able to enjoy cut-elimination. Moreover, some basic isomorphisms are pointed out.
Permutative Additives and Exponentials
PULCINI, GABRIELE
2007-01-01
Abstract
Permutative logic (PL) is a noncommutative variant of multiplicative linear logic (MLL) arising from recent investigations concerning the topology of linear proofs. Permutative sequents are structured as oriented surfaces with boundary whose topological complexity is able to encode some information about the exchange in sequential proofs. In this paper we provide a complete permutative sequent calculus by extending that one of PL with rules for additives and exponentials. This extended system, here called permutative linear logic (PLL), is shown to be a conservative extension of linear logic and able to enjoy cut-elimination. Moreover, some basic isomorphisms are pointed out.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
