Fibring: Completeness preservation (Q2732291)

When we apply the technique of fibring for combining two logics we produce a logic allowing the free mixing the connectives from both logics and using the inference rules from both logics [see \textit{D. M. Gabbay}, Fibring logics, Clarendon Press, Oxford (1999; Zbl 0909.03001)]. In the general case, soundness is shown to be preserved by fibring, but the preservation of completeness remains an open problem. In this paper the authors concentrate their attention on the problem of completeness preservation and give a positive answer to this question with reasonable requirements on the two given logics with `full'\ semantics and availability of `equivalence\'. Namely, since `equivalence'\ implies `congruence'\ and the former is preserved by fibring, the preservation of strong completeness is a consequence of the completeness theorem for general semantics. NEWLINENEWLINENEWLINEAfter a brief review of Hilbert type systems and their fibrings, a general notion of interpretation systems and their fibrings are introduced in order to establish the appropriate notion of general logic system enabling to study the completeness problem. Two examples from modal logic are presented. A strong completeness theorem for logics with full general semantics and with congruence is obtained by using an adapted Henkin construction. Finally, the notion of logic with equivalence is introduced and it is shown that this class of logics is closed under fibring and is a proper subclass of the class of logics with congruence. At both the proof-theoretic and the modal-theoretic level, the authors provide a categorical characterization of fibring.