Non-commutative logic II: sequent calculus and phase semantics
In Part I [Ann. Pure Appl. Logic 101, No. 1, 29-64 (2000; Zbl 0962.03054)], \textit{V. M. Abrusci} and the author introduced a non-commutative extension of the multiplicative fragment of linear logic, called ``non-commutative logic (NL). The discovery of the structure of an order variety (introduced by the author in his PhD thesis) was the crucial step towards NL sequent calculus. An order variety is a ternary relation which is a particular case of cyclic order: it also satisfies the so-called ``spreading condition. Every cyclic order \(\alpha\) on a set \(E\) induces a (binary) order relation \(\alpha_x\) (on \(E\)), for every element \(x\) of \(E\). Conversely, with every order on a set \(E\), one can associate its ``closure, which is a cyclic order on \(E\). But the spreading condition is necessary (and sufficient) to prove that every order variety \(\alpha\) on \(E\) is the closure of the parallel (resp. serial) composition of the two order relations \(\alpha_x\) and \(x\), for every \(x\) in \(E\). This is the key property of order varieties, which is (also) used to associate with every sequent of an NL sequent calculus proof an order variety: every rule corresponds to an operation on order varieties. In this paper, the sequent calculus is extended to the additive connectives and to the exponentials. This requires the study of the entropy relation between orders and the introduction of the series-parallel order varieties. Phase semantics is also introduced, and a cut-elimination theorem is proven semantically, in the spirit of previous work by \textit{M. Okada} [Theor. Comput. Sci. 227, No. 1-2, 333-396 (1999; Zbl 0951.03058)]. The notion of a proof-net introduced for the multiplicative fragment (in the previous work with Abrusci) cannot be easily extended to the full propositional fragment.
- Non-commutative logic. I: The multiplicative fragment
- Non-commutative logic. III: Focusing proofs.
- scientific article; zbMATH DE number 2185722
- scientific article; zbMATH DE number 1980929
- Phase semantics for a pure noncommutative linear propositional logic
- Phase semantics and sequent calculus for pure noncommutative classical linear propositional logic
- A new correctness criterion for multiplicative non-commutative proof nets
- One-Sided Sequent Systems for Nonassociative Bilinear Logic: Cut Elimination and Complexity
- Classical conservative extensions of Lambek calculus
- Towards a semantics of proofs for non-commutative logic: Multiplicatives and additives
- Non-commutative logic. III: Focusing proofs.
- Non-commutative logic. I: The multiplicative fragment
- A mixed -calculus
- Non-commutative proof construction: a constraint-based approach
- Multiplicative linear logics and fibrations
- scientific article; zbMATH DE number 5295711 (Why is no real title available?)
- Non-Commutative First-Order Sequent Calculus
- Phase semantics and sequent calculus for pure noncommutative classical linear propositional logic
- Study of behaviours via visitable paths
- Non-commutative classical arithmetical sequent calculi are intuitionistic
- scientific article; zbMATH DE number 1865920 (Why is no real title available?)
- scientific article; zbMATH DE number 1418443 (Why is no real title available?)
- Pomset logic. The other approach to noncommutativity in logic
- Cyclic extensions of order varieties
- A System of Interaction and Structure III: The Complexity of BV and Pomset Logic
- Ordered adjoint logic
This page was built for publication: Non-commutative logic II: sequent calculus and phase semantics
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4487273)
