Borrowing interpolation (Q2893323)

It seems appropriate to begin this review by recalling Craig's interpolation theorem for first-order logic: For any language \(L\), any \(L\)-theory \(T\), and two extensions \(L_{0}\) and \(L_{1}\) of \(L\) whose common symbols are all symbols of \(L\) and any \(L_{0}\)-formula \(\varphi\) and \(L_{1}\)-formula \(\psi\), if \(T\models \varphi\rightarrow\psi\), then there exists an \(L\)-formula \(\theta\) such that \(T\models \varphi\rightarrow\theta\) and \(T\models \theta\rightarrow\psi\). \(\theta\) is called a Craig interpolant for \(\varphi\) and \(\psi\). This theorem, which involves the elimination of superfluous notions, has applications in mathematical logic, e.g., in the theory of definition (Beth's theorem) and to show that every theory is independently axiomatizable, in philosophy of science, e.g., for the eliminability of theoretical terms, and in some branches of computer science, e.g., in formal specification theory, data bases, automated reasoning, type checking, model checking, and structured theorem proving. However, this theorem should be generalized, as argued, among others, by R. Diaconescu, in terms of sets of sentences (see below) to cover some interesting logics that, in principle, do not fulfill the above Craig interpolation theorem (i.e., in the single sentences version). NEWLINENEWLINENEWLINE In the article under review, which is part of a series of earlier articles by the author devoted to the `institution-independent' program, he states, at the level of the theory of institutions of Goguen-Burstall, in the main theorem of his article, Theorem 3.1 (Borrowing interpolation), a generic method for transporting backwards interpolation properties along institution comorphisms. I point out that this theorem is a generalization of Proposition 9.30 stated in [\textit{R. Diaconescu}, Institution-independent model theory. Studies in Universal Logic. Basel: Birkhäuser (2008; Zbl 1144.03001)]. Moreover, as the author says: ``We have illustrated the applicability power of our method(s) by deriving interpolation results for partial algebra, preordered algebra and its Horn clause fragment, for universal sentences, and for higher order logic (with Henkin's semantics), from interpolation properties of many-sorted first-order logic with equality and its Horn clause fragment.'' Once more, I notice that most of these illustrations can be found in the author's book [loc. cit., pp. 219--220]. NEWLINENEWLINENEWLINE Next we proceed to explain more fully the contents of the article under consideration. In Section 2, the author, after stating notations and conventions about category theory, recalls the definition of institution, introduces the examples of institutions he is going to use in the development of the applications, the Galois connexion between sets of sentences and sets of models, the semantic Boolean connectives in an institution, the concept of compact institution, and the notion of conservative signature morphism. After this, he recalls the concepts of comorphism between institutions, of conservative comorphism between institutions, and the construction of the institution of the presentations over a given institution. In Section 3, he formulates the notion of Craig interpolation square -- from the standpoint of institution-independent model theory -- in terms of sets of sentences and argues that it is more natural because some institutions, not having conjunctions, lack Craig's interpolation theorem in the single sentences version, but have it in the sets of sentences formulation. Typical examples for this situation are equational logic and Horn clause logic. After having done that for any sets of signature morphisms \(\mathcal{L}\), \({\mathcal{R}}\) in any institution \(\mathcal{I}\), he defines, on the basis of the notion of Craig interpolation square, the concept of Craig \((\mathcal{L},\mathcal{R})\)-interpolation. Next, since the method of borrowing interpolation along institution comorphisms requires some special interpolation properties of the comorphisms, the author recalls, for a set of signature morphisms \(\mathcal{S}\) in any institution \(\mathcal{I}\), when an institution comorphism has the so-called Craig \(\mathcal{S}\)-left interpolation property and its counterpart, the Craig \(\mathcal{S}\)-right interpolation property. Then he defines, for an institution with pushouts of signatures, the notion of quasi-pushout in terms of conservative signature morphisms. Finally, he states the main result of the article: Let \((\Phi,\alpha,\beta): \mathcal{I}\rightarrow\mathcal{I}'\) be a conservative institution morphism such that \(\Phi\) maps pushouts to quasi-pushout (in order to capture also the interpolation for higher-order logic), and let \(\mathcal{L}\), \({\mathcal{R}}\) be sets of signature morphisms such that \(\mathcal{I}'\) has the Craig \((\Phi(\mathcal{L}),\Phi(\mathcal{R}))\)-interpolation. Then \(\mathcal{I}\) has [the] Craig \((\mathcal{L},\mathcal{R})\)-interpolation. Sections 4 to 6 are devoted to illustrate the applicability power of his generic method for establishing interpolation properties by `borrowing' across logical systems. I notice, in particular, that, in Section 4, to obtain interpolation in partial and preordered algebra, the author, among others things, defines the notion of Craig-Robinson interpolation square (which is stronger than the notion of Craig interpolation square), indicates that the Craig \((\mathcal{L},\mathcal{R})\)-interpolation can be extended to the Craig-Robinson \((\mathcal{L},\mathcal{R})\)-interpolation, and gives a general result for lifting interpolation from an institution \(\mathcal{I}\) to the institution of its presentations \(\mathcal{I}^{\mathrm{pres}}\). In the remaining Section 7, the author states his conclusions.NEWLINENEWLINENEWLINE Reviewer's remarks: On p. 564, the author says the following: ``In order to avoid the existence of empty interpretations of the sorts, which may complicate unnecessarily our presentation, we assume that each signature has at least one \textit{constant} (i.e., function symbol with empty arity) for each sort.'' And on p. 565, he says yet again: ``In order to avoid empty carriers, like in the case of \textbf{FOL} (the institution canonically associated to first-order logic, I add), we assume [that] there exists at least one \textit{total} constant for each sort.'' In this connection I think it is suitable to recall what \textit{J. Schmidt} says in [Math. Jap. 6, 77--112 (1962; Zbl 0119.25903)], talking about single-sorted algebras (but being also applicable, with appropriate modifications, when talking about many-sorted algebras): ``Let us still note the discussion of the particular rôle of the algebras of very low cardinal number, i.e., of cardinals \(0\) or \(1\), to be found in this paper. Thus, the empty algebra (if it exists), and the one-element algebras of a certain similarity type are defined (somehow analogously to the definition of subalgebras etc.) as the unique algebraic structures in which obvious conditions hold. But the discussion of the algebras of very low cardinal number, especially of the empty algebra, is not a purely dogmatic affair as some authors and reviewers seem to assume. Thus, many theorems of General Algebra do not hold for these algebras of very low cardinal number, at least not for the empty algebra, a failure which remains unnoticed by some authors. Other authors try to escape the situation by not admitting the empty or one-element algebra; unfortunately, they sometimes forget their own special convention, because it appears inconvenient at other places, e.g., when speaking of subalgebras. Still other authors do not even admit the subalgebra generated by the empty set; the futility of doing so becomes almost evident by the remark that one can consider any arbitrary algebra \(A\) -- by a more or less unessential change of the algebraic structure -- as generated by the empty set. The last remark seems to make evident that -- notwithstanding all possible conventions concerning the special treatment of the empty and the one-element set according to convenience and individual taste -- there are mathematical facts connected with the low cardinal numbers which as inconvenient as the[y] may be in the very nature of things: one can not avoid them.''