Metacompleteness of substructural logics
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.
scientific article; zbMATH DE number 6136992