An initiative of SQIG at IT, following the previous GTF initiative, partially supported by FCT and EU FEDER, namely via the project AMDSC UTAustin/MAT/0057/2008.
Since the pioneering works by Thomason 1984 and Konolidge 1986, the problem of combining logics (and proving transference results about the combination mechanisms) has attracted growing attention. The practical motivation is clear: in applications (e.g. software engineering and artificial intelligence), the need to work with several logics at the same time is the rule rather than the exception. Ideally, the practitioner instead of developing from zero a new logic with the envisaged features would combine well known logics and use the transference results on the adopted combination mechanism to infer the properties (e.g. completeness) of the resulting logic from those of the combined logics. Several combination mechanisms have been proposed, namely fusion (Kracht and Wolter 1991), temporalization (Finger and Gabbay 1992), combination of institutions (Tarlecki 1995), fibring (Gabbay 1996), synchronization (Sernadas et al 1997), product (Gabbay and Shehtman 1998) and modalization (Fajardo and Finger 2003). A few transference results have been established, namely: preservation of weak completeness and decidability by modalization; weak completeness, finite model property and Craig interpolation by fusion; weak and strong completeness, Craig interpolation and finite model property by fibring. Several efforts have been made to enlarge the domain of applicability of the combination mechanisms to a wider class of logics: for instance, fibring subsumes fusion and it is applicable well beyond the realm of modal logics. In this vein, the graph-theoretic account of fibring recently proposed by Sernadas et al 2009 further extends its domain of applicability to substructural logics, including linear and paraconsistent logics. Some work has been dedicated to applying the categorical imperative to this field, namely setting up an appropriate category of logics where fibring appears as a universal construction, as initially advocated by Sernadas et al 1999. However, the required morphisms are rather awkward. Recently, we proposed to recover Winskel's idea (1984) of using partial morphisms for the parallel composition of processes. This idea when applied to logics led us to yet another mechanism for combining logics (parallel composition) that turned out to subsume fibring as a special case and stressed the importance of combining connectives (and other language constructors). Basing the combination of logics on such combined constructors opened the way towards a truly conservative combination mechanism (meet-combination), by endowing each combined constructor only with the common logical properties of its components.
The MCL initiative aims at further exploration of the properties of meet-combination of logics (establishing further transference results) and extending its domain of applicability to other logics (beyond those of propositional nature endowed with a matrix semantics and a Hilbert calculus). The initiative will also address further development of the idea of combining connectives (and other language constructors), namely concerning probabilistic combinations and quantum superpositions. Applications are expected to the verification of classical, probabilistic and quantum protocols.
AMS-MSC 03B62 Combined logics