Non-commutative logic. III: Focusing proofs. (Q1427855)

The paper studies the focalization property in the framework of \textit{V. M. Abrusci} and \textit{P. Ruet}'s non-commutative logic [Ann. Pure Appl. Logic 101, 29--64 (2000; Zbl 0962.03054)]. Abrusci and Ruet introduced sequent calculus and proof-nets for multiplicative non-commutative logic (MNL), and later \textit{P. Ruet} [Math. Struct. Comput. Sci. 10, 277--312 (2000; Zbl 0999.03056)] extended the sequent calculus to full propositional non-commutative logic (NL). In this paper, the authors define a focalized sequent calculus for NL. The main problem to overcome is related to the extra structure (the order variety) of NL: does it fit in with the (now standard) splitting of connectives into reversible/irreversible? It is shown that one can ``push'' the entropy rule of NL towards the rules of conjunction, and thus give a positive answer. A nice thing is how completeness of the focalized system is proven for MNL: it is shown that every MNL proof-net can be sequentialized into a focalized sequent calculus proof. In the general NL case, completeness is achieved thanks to a careful study of the permutability of the rules.