Sequent-systems and groupoid models. I (Q1119625)

The author studies a family of non-classical propositional logics related to Heyting's and Johansson's as well as to relevant logics, Lambek calculus of syntactic categories and BCK algebras. Their language contains propositional binary connectives \(\to\), \(\wedge\), \(\vee\), \(\circ\) and constants \(\bot\), \(\top\). The least of these logics (called L) corresponds to a class of algebras called urlogs (right-residuated lattice-ordered groupoids). A cut-free sequent calculus is built for L. Also some extensions of L and their sequent variants are considered. In particular, Heyting logic is an extension in which, among other properties, \(\circ\) and \(\wedge\) are equivalent, etc. A nice feature of the sequent systems studied is that their formulations directly correspond to properties of groupoid models.