Conuclear images of substructural logics (Q2813674)

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\).