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

Abrusci, V. Michele

J. Symb. Log. 56, No. 4, 1403-1451 (1991).

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.

Reviewer: H.Pfeiffer (Hannover)

MSC:

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

Keywords:

noncommutative linear logic; propositional logic; semantics; phase spaces; noncommutative monoid with unit; two-sided sequent calculus; soundness; completeness; proof-nets; planar graphs; cut rule; one-sided sequent calculi; cut elimination

Citations:

Zbl 0625.03037

References:

[1]	Quantales and (noncommutative) linear logic 55 pp 41– (1990)
[2]	DOI: 10.1017/S0305004100065403 · Zbl 0658.06007
[3]	DOI: 10.1002/malq.19900360405 · Zbl 0810.03005
[4]	DOI: 10.1016/0304-3975(87)90045-4 · Zbl 0625.03037
[5]	DOI: 10.1090/conm/092/1003197