Phase semantics and sequent calculus for pure noncommutative classical linear propositional logic. (English) Zbl 0746.03044

Linear logic, created by J.-Y. Girard [Theor. Comput. Sci. 50, 1- 102 (1987; Zbl 0625.03037)], is a new approach to get constructive logics needed in computer science. New connectives are introduced with special semantics and rules of inference. The rules for weakening and of contraction are abandoned but the exchange rule is kept, although it is throughout in the spirit of linear logic also to drop this rule and thus meet the situation in the “real world” of computer science. But Girard characterizes the noncommutative case to be more delicate and confines his paper to the commutative case.
The author of the paper under review is concerned with the delicate case. In an earlier paper [Z. Math. Logik Grundlagen Math. 36, No. 4, 297-318 (1990)] he investigated the corresponding intuitionistic system. Now he considers the classical case, in both papers confining himself to propositional logic.
To establish the appropriate semantics he introduces the noncommutative classical version of phase spaces. Phases are the concept corresponding to possible universes in intuitionistic or modal semantics. Here they are to be subsets of a noncommutative monoid with unit for which certain operations are defined which correspond to the connectives of the noncommutative classical linear propositional logic: linear postnegation, retronegation, postimplication, retroimplication, times, par, with and plus.
A two-sided sequent calculus for this logic is defined and soundness as well as completeness with respect to the phase semantics are proved.
As Girard for the commutative case, the author defines proof-nets to visualize the structure of proofs. For the noncommutative logic system they are planar graphs. The difficulties caused by noncommutativity are overcome by certain conditions on the cut rule and the binary rules for the multiplicative connectives. Since this system PNCL of pure noncommutative classical linear propositional logic does not enjoy cut elimination, two other systems of one-sided sequent calculi are introduced. In one of them a restriction on the cut rule is imposed, in the other one such conditions are avoided by introducing two new rules.
For these systems cut elimination is shown, and it is shortly discussed why cut elimination in the two-sided calculus fails.


03F05 Cut-elimination and normal-form theorems
03B70 Logic in computer science
03B20 Subsystems of classical logic (including intuitionistic logic)
03F07 Structure of proofs


Zbl 0625.03037
Full Text: DOI


[1] Quantales and (noncommutative) linear logic 55 pp 41– (1990)
[2] DOI: 10.1017/S0305004100065403 · Zbl 0658.06007 · doi:10.1017/S0305004100065403
[3] DOI: 10.1002/malq.19900360405 · Zbl 0810.03005 · doi:10.1002/malq.19900360405
[4] DOI: 10.1016/0304-3975(87)90045-4 · Zbl 0625.03037 · doi:10.1016/0304-3975(87)90045-4
[5] DOI: 10.1090/conm/092/1003197 · doi:10.1090/conm/092/1003197
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.