×

Cyclic involutive distributive full Lambek calculus is decidable. (English) Zbl 1225.03022

A cut-elimination theorem for positive propositional relevance logic \(R^+\) was established by M. Dunn and the reviewer. The decidability status of \(R^+\) is unknown since there is no obvious bound on the number of contraction inferences. The author gives a (rather complicated) proof of cut elimination along the same lines for some subsystems (and their extensions with negation) when fusion (relevant conjunction \(\neg(A\rightarrow \neg B)\)) is cyclic but not necessarily commutative. In many of these cases he is able to obtain decidability by known methods.

MSC:

03B47 Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics)
03B25 Decidability of theories and sets of sentences
03F05 Cut-elimination and normal-form theorems
Full Text: DOI