An algebraic approach to the disjunction property of substructural logics (Q2425350)

Let \textbf{FL} be the sequent system obtained from Gentzen's \textbf{LJ} for intuitionistic logic by deleting all structural rules and adding rules for fusion. By a substructural logic (simply called logic if no confusion occurs) over \textbf{FL} we mean an axiomatic extension of \textbf{FL}. A logic \textbf{L} has the disjunction property (DP, for short) when, for any formulas \(\varphi\) and \(\psi\), if \(\varphi\vee \psi\) is provable in \textbf{L} then at least one of the formulas \(\varphi\) and \(\psi\) is provable in it. An \textbf{FL}-algebra is an algebra \((A,\wedge,\vee,\cdot ,/,\setminus,0,1)\) where \((A,\wedge,\vee,\cdot ,/,\setminus,1)\) is a residuated lattices and 0 is an arbitrary element of \(A\). Formulas of the language for \textbf{FL} are interpreted in a given \textbf{FL}-algebra \textbf{A} in the usual way by using valuations on it. For each logic \textbf{L}, let V(\textbf{L}) be the class of all \textbf{FL}-algebras in which every formula provable in \textbf{L} is valid. In fact, V(\textbf{L}) is a subvariety of the variety \(\mathcal{FL}\) of all {\text\textbf{FL}}-algebras, and, conversely, any subvariety of \(\mathcal{FL}\) is equal to V(\textbf{L}) for some logic \textbf{L}. A logic \textbf{L} is said to be complete with respect to a subclass \(\mathcal{K}\) of V(\textbf{L}) when \(\mathcal{K}\) generates V(\textbf{L}). An \textbf{FL}-algebra is well-connected if and only if for all \(x,y\in {\mathbf A},x\vee y\geq 1\) implies either \(x\geq 1\) or \(y\geq 1\). The author shows that Maksimova's criterion on the disjunction property of superintuitionistic logics can be naturally extended to one on the DP of substructural logics over \textbf{FL}: If \textbf{L} is a complete logic over \textbf{FL} with respect to a class \(\mathcal{K}\) of \textbf{FL}-algebras, then \textbf{L} has DP if and only if for all \({\mathbf A},{\mathbf B}\in \mathcal{K}\) there exits a well-connected \textbf{FL}-algebra \({\mathbf C}\in V({\mathbf L})\) and a surjective homomorphism from \textbf{C} onto the direct product \({\mathbf A}\times {\mathbf B}\) of \textbf{A} and \textbf{B}. By using this, he shows the DP for some of the substructural logics for which syntactic methods don't work well.