Metacompleteness of substructural logics (Q1935554)

The paper studies the extensions of the logic \(\mathbf{FL}\) -- the logic of full Lambek calculus. A logic \(L\) is said to enjoy the disjunction property if the fact that \(\alpha \lor \beta\) is a theorem of \(L\) entails that \(\alpha\) or \(\beta\) is a theorem of \(L\). A logic \(L\) is said to enjoy the existence property if the fact that \(\exists x\alpha(x)\) is a theorem of \(L\) entails that for some term \(t\), \(\alpha(t)\) is a theorem of \(L\). The metacompleteness of some logics over \(\mathbf{FL}\) is proved. Metacompleteness is used in order to establish disjunction and existence properties (or the absence of these properties) of extensions of \(\mathbf{FL}\). In particular, it is proved that no substructural logic that is both involutive and contractive has the disjunction or the existence property. Also, using metacompleteness, the admissibility of some inference rules is proven.