Conuclear images of substructural logics
With a substructural logic \(\mathcal{L}\) one can associate a logic \(\mathcal{L}_\sigma\) obtained from \(\mathcal{L}\) by endowing it with new unary operator \(\sigma\) and the following axioms {\parindent=0.75cm\begin{itemize}\item[(i)] \(\sigma(A) \cdot \sigma(B) \to \sigma(A\cdot B)\); \item[(ii)] \(\sigma(A) \to A\); \item[(iii)] \(\sigma(A) \to \sigma(\sigma(A))\); NEWLINENEWLINE\end{itemize}} and the necessitation rule \(A/\sigma(A)\). If \(A\) is a formula, \(A^\sigma\) denotes the formula obtained from \(A\) by replacing with \(\sigma(B)\) each subformula \(B\) of \(A\). The conuclear \(\sigma(\mathcal{L})\) image of the logic \(\mathcal{L}\) is a the logic whose theorems are precisely the formulas \(A\) such that \(\mathcal{L} \vdash A^\sigma\). For every substructural logic \(\mathcal{L}\), the logic \(\sigma(L)\) is always substractural.NEWLINENEWLINEIt is proven that: {\parindent=0.7cm \begin{itemize}\item[(a)] the logic \(\mathcal{L}\) extends \(\sigma(\mathcal{L})\), and \(\sigma(\mathcal{L})\) has the disjunction property; \item[(b)] \(\mathcal{L}_\sigma\) and \(\sigma(\mathcal{L})\) are PSPACE-hard; \item[(c)] for any consistent substructural logic \(\mathcal{L}\), its conuclear image does not admit double negation principle. NEWLINENEWLINE\end{itemize}} Section 5 of the paper is devoted to the study of properties that are preserved under \(\sigma\).
- Algebraic proof theory for substructural logics: cut-elimination and completions
- An algebraic approach to the disjunction property of substructural logics
- Cancellative residuated lattices
- Disjunction property and complexity of substructural logics
- Embedding theorems for classes of GBL-algebras
- Linear logic
- Ordered groups with a conucleus
- Residuated lattices. An algebraic glimpse at substructural logics
- Some theorems about the sentential calculi of Lewis and Heyting
- The algebra of topology
- The Blok-Ferreirim theorem for normal GBL-algebras and its application
This page was built for publication: Conuclear images of substructural logics
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2813674)
