Categorical abstract algebraic logic: meet-combination of logical systems (Q355641): Difference between revisions

In the article under review, which is part of a series of earlier articles by the author devoted to the categorical abstract algebraic logic program (CAAL for short), the author generalizes some results of \textit{A. Sernadas} et al. [Log. Univers. 5, No. 2, 205--224 (2011; Zbl 1280.03035); J. Log. Comput. 22, No. 6, 1453--1470 (2012; Zbl 1280.03034)], on the combination of logical systems by means of the so-called meet combination, to CAAL. More specifically, in Section 2 the author defines, for an arbitrary but fixed category \(\mathbf{Sign}\), the category of signatures, an arbitrary but fixed \({\mathbf{Set}}\)-valued functor \(\mathrm{Sen}: \mathbf{Sign}\rightarrow {\text\textbf{Set}}\), the sentence functor, and an arbitrary but fixed category \(\mathbf{N}\) of natural transformations on \(\mathrm{Sen}\), the clone of all algebraic operations on \(\mathrm{Sen}\), the concepts of constant natural transformation, for natural transformations \(\sigma: \mathrm{Sen}^{n}\rightarrow \mathrm{Sen}\) in \(\mathbf{N}\), of \(\mathbf{N}\)-rule of inference (which is a pair \(((\sigma^{i})_{i\in n},\tau)\), where \(\sigma^{i}\), for every \(i\in n\), and \(\tau\) are natural transformations in \(\mathbf{N}\)), and that of \(\mathbf{N}\)-Hilbert calculus \(\mathcal{R}\) (which is a set of \(\mathbf{N}\)-rules of inference). Moreover, for functors \(\mathrm{Sen}: \mathbf{Sign}\rightarrow {\text\textbf{Set}}\) and \(\mathrm{Sen}': \mathbf{Sign}'\rightarrow {\text\textbf{Set}}\) and categories of natural transformations \(\mathbf{N}\), \(\mathbf{N}'\) on \(\mathrm{Sen}\), \(\mathrm{Sen}'\), respectively, he defines the concept of translation from \(\mathrm{Sen}\) to \(\mathrm{Sen}'\) (which is a pair \((F,\alpha)\), where \(F\) is a functor from \(\mathbf{Sign}\) to \(\mathbf{Sign}'\) and \(\alpha\) a natural transformation from \(\mathrm{Sen}\) to \(\mathrm{Sen}'\circ F\)). Next, he defines the class of \((\mathbf{N},\mathbf{N}')\)-epimorphic translations. Afterwards, the author defines the concepts of \(\mathbf{N}\)-algebraic system (which is a pair \(\mathcal{A} = (\mathrm{Sen}',(F,\alpha))\) consisting of a functor \(\mathrm{Sen}'\) from \(\mathbf{Sign}'\) to \({\mathbf{Set}}\), with a category \(\mathbf{N}'\) of natural transformations on \(\mathrm{Sen}'\), and an \((\mathbf{N},\mathbf{N}')\)-epimorphic translation \((F,\alpha)\) from \(\mathrm{Sen}\) to \(\mathrm{Sen}'\)), of \(\mathbf{N}\)-matrix system (which is a pair \(\mathfrak{A} = (\mathcal{A},T)\) consisting of an \(\mathbf{N}\)-algebraic system \(\mathcal{A} = (\mathrm{Sen}',(F,\alpha))\) and a family \(T = (T_{\Sigma})_{\Sigma\in \mathrm{Ob}(\mathbf{Sign}')}\), where, for every \(\Sigma\in \mathrm{Ob}(\mathbf{Sign}')\), \(T_{\Sigma}\subseteq \mathrm{Sen}'(\Sigma)\)), and that of \(\mathbf{N}\)-matrix semantics (which is a class \(\mathcal{M}\) of \(\mathbf{N}\)-matrices). Following this, the author defines when an \(\mathbf{N}\)-matrix system \(\mathfrak{A} = (\mathcal{A},T)\) satisfies a natural transformation \(\sigma\) from \(\mathrm{Sen}^{k}\) to \(\mathrm{Sen}\) in \(\mathbf{N}\) at \((\varphi_{j})_{j\in k}\in \mathrm{Sen}(\Sigma)^{k}\) under \(f\in \mathrm{Hom}(\Sigma,\Sigma')\), written \(\mathfrak{A}\models_{\Sigma}\sigma[(\varphi_{j})_{j\in k},f]\), and when an \(\mathbf{N}\)-rule \(((\sigma^{i})_{i\in n},\tau)\) is a rule of an \(\mathbf{N}\)-matrix semantics \(\mathcal{M}\), written \((\sigma^{i})_{i\in n}\models^{\mathcal{M}}\tau\). Lastly, in this section, he defines the concept of logical system as an ordered quintuple \(\mathcal{L} = (\mathbf{Sign},\mathrm{Sen},\mathbf{N},\mathcal{R},\mathcal{M})\), where \(\mathbf{Sign}\) is a category, \(\mathrm{Sen}\) a functor from \(\mathbf{Sign}\) to \({\mathbf{Set}}\), \(\mathbf{N}\) a category of natural transformations on \(\mathrm{Sen}\), \(\mathcal{R}\) an \(\mathbf{N}\)-Hilbert calculus, and \(\mathcal{M}\) an \(\mathbf{N}\)-matrix semantics. After this, in Section 3 the author defines, for a logical system \(\mathcal{L} = (\mathbf{Sign},\mathrm{Sen},\mathbf{N},\mathcal{R},\mathcal{M})\), the product logical system \(\mathcal{L}^{\times} = (\mathbf{Sign},\mathrm{Sen}^{\times},\mathbf{N}^{\times},\mathcal{R}^{\times},\mathcal{M}^{\times})\). I point out that the calculus \(\mathcal{R}^{\times}\) is an enrichment of \(\mathcal{R}\), i.e., it contains all rules of the form \((r,r)\) for \(r\in \mathcal{R}\), and some additional \(\mathbf{N}^{\times}\)-rules devised for dealing with the combined operations: the lifting rules and, for constant natural transformations, the special colifting rules. The reason for allowing only the special colifting rules is that, unless this restriction is imposed, the rules are not in general sound. Lastly, in this section, the author writes \(\vdash^{\times}\) and \(\models^{\times}\) for satisfaction and entailment in \(\mathcal{L}^{\times}\). In Section 4, after defining when a class of \(\mathbf{N}\)-matrix systems \(\mathcal{M}\) is a c-semantics, the author proves the following soundness theorem: Let \(\mathcal{L} = (\mathbf{Sign},\mathrm{Sen},\mathbf{N},\mathcal{R},\mathcal{M})\) be a logical system, where \(\mathcal{M}\) is a c-semantics. If \(\mathcal{L}\) is sound, then \(\mathcal{L}^{\times}\) is sound. In Section 5, after defining when a logical system is c-complete, he proves the following c-completeness theorem: If the logical system \(\mathcal{L}\) is c-complete, then \(\mathcal{L}^{\times}\) is c-complete. In Section 6, the author proves the following conservativeness theorem: Let \(\mathcal{L}\) be a logical system. Then, for every set of natural transformations \(\Delta\cup \{\sigma\}\) in \(\mathbf{N}\), if \(\{(\delta,\delta)\mid \delta\in \Delta\}\models^{\times}(\sigma,\sigma)\), then \(\Delta\models \sigma\). From here, he obtains, as an immediate corollary, the following consistency theorem: If the logical system \(\mathcal{L}\) is consistent, then so is \(\mathcal{L}^{\times}\). Finally, in Section 7, the author presents an example displaying the difference between the soundness of special colifting and the lack of soundness obtained by allowing the full power of the general colifting rule.