An algebraic approach to the disjunction property of substructural logics
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.
- Disjunction property and complexity of substructural logics
- scientific article; zbMATH DE number 4142010
- Relational Methods in Computer Science
- scientific article; zbMATH DE number 7644094
- Algebraic proof theory for substructural logics: cut-elimination and completions
- An algebraic approach to subframe logics. Intuitionistic case
- Cut elimination and strong separation for substructural logics: an algebraic approach
- Theorems of Alternatives for Substructural Logics
- scientific article; zbMATH DE number 1907195
- Extension properties and subdirect representation in abstract algebraic logic
- Metacompleteness of substructural logics
- Fuzzy logics from substructural perspective
- Algebraization, parametrized local deduction theorem and interpolation for substructural logics over FL
- Conuclear images of substructural logics
- Algebraic characterizations of variable separation properties
- The proof by cases property and its variants in structural consequence relations
- Indecomposability of free algebras in some subvarieties of residuated lattices and their bounded subreducts
- Variable sharing in substructural logics: an algebraic characterization
- Theorems of Alternatives for Substructural Logics
- An algebraic approach to subframe logics. Modal case
- Disjunction property and complexity of substructural logics
- Relational Methods in Computer Science
- Algebraic proof theory for LE-logics
This page was built for publication: An algebraic approach to the disjunction property of substructural logics
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2425350)
