Combining Logics

First published Thu Sep 13, 2007; substantive revision Mon Oct 24, 2011

The subject of combinations of logics is still a young topic in contemporary logic. Besides the pure philosophical interest offered by the possibility of defining mixed logic systems in which distinct operators obey logics of different nature, as for instance erotetic logics (the logical analysis of questions) which require combining epistemic and deontic logics, there also exist many pragmatical and methodological reasons for considering combined logics. In fact, the use of formal logic as a tool for knowledge representation in Computer Science frequently requires the integration of several logic systems into a homogeneous environment.

Important questions in the philosophy of logic such as: “why are there so many logics instead of just one?” (or even, instead of none), as for instance, raised in Epstein 1995, can be naturally counterposed by several other questions: if there are indeed many logics, are they excluding alternatives, or are they compatible? Is it possible to combine different logics into coherent systems with the purpose of using them in applications and to shed some light on the properties of complex logics? Moreover, if we can compose logics, why not decompose them? And, if a logic is decomposed into elementary sublogics, is it possible to recover it by combining such fragments? What kind of properties of logics can be transferred to their combinations? Questions of this kind have been only partially tackled in the literature, and reflect challenges to be confronted in the evolution of this topic.

1. Philosophical and methodological motivations for combining logics

David Hume generated a popular controversy with his famous passages of “A Treatise of Human Nature” (cf. Hume 2000, Book 3, Part 1, Section 1, paragraph 27) where he noted that sometimes people draw conclusions involving prescriptive statements of the form ‘ought to be’ on the basis of descriptive statements of the form ‘what is’. Hume thinks that logic used in this way involves a dangerous change of subject matter. So, whether or not ‘ought’ can be derived from ‘is’ has become one of the central questions of ethical theory, and the majority of interpreters hold that, for Hume, such a derivation is impossible.

With our point of view concerning combinations of logics, it is necessary to investigate the properties of combining deontic and alethic logics: in order to perform such a jump from ‘is’ to ‘ought’ some authors propose (see e.g. Schurz 1997) that what is necessary is an explicit “bridge principle” which specifically connects ‘is’ and ‘ought’. An axiom schema X, following Schurz 1991, is a bridge principle iff X contains at least one schematic letter which has at least one occurrence within the scope of an O (the deontic “obligation” operator) and at least one occurrence outside the scope of any O. Thus, for instance,

pOp

is a bridge principle representing ‘is-ought’ that which would appease Hume's criticism. On the other hand, the much discussed moral principle ‘ought-implies-can’ (controversially attributed to I. Kant, see Baumgardt 1946) can be formalized through another bridge principle:

Op → ◊p,

where ◊ denotes the alethic “possibility” operator.

Clearly, bridge principles do not solve any philosophical questions such as the ‘is-ought problem’; nonetheless, they contribute to clarify the problem and to uncover hidden assumptions. The idea of combining logics lend clarification to questions of this kind by making clear that, for instance, ‘is’ and ‘ought’ are indeed independent notions. This is elucidated through a formal analysis of the composition of the logics involved (in this case, alethic and deontic) or by decomposition of the complex logic (in this case, bimodal) into simpler ones. In such circumstances, combining logics can be perceived as a tool for simplifying problems involving heterogeneous reasoning.

The fact that ‘ought’ is not conveyed as a predicate, but as a modal operator ranging over actions or states of affairs, was responsible for the delay of formal treatments of this centuries-old question.

Such a treatment was only possible after the development of general modal logic. Indeed, what we are dealing with here is a bimodal logic, which is properly treated only after a deeper understanding of the semantical subtleties of mixing alethic and deontic logics. Moreover, according to some philosophers who have argued that it is not possible to link ‘is’ and ‘ought’ (that is, who defend Hume's thesis that no non-trivial ‘is-ought’ deductions are possible), it is mandatory to use combinations of first-order, alethic and deontic logics (cf. e.g. Stuhlmann-Laeisz 1983 and Schurz 1997).

A. Prior (1960), using the apparatus of contemporary modal logic, tried to characterize the distinction between normative and non-normative sentences in formal terms, which enabled him to define senses of ‘descriptive content’ versus ‘normative content’. A problem, however, occurs with mixed sentences, which have both descriptive and normative components, and Prior comes up with a paradox: wherever we draw the distinction between non-normative and normative sentences, unexpected inferences from non-normative premises to normative conclusions may appear by a mere use of laws of classical propositional logic. Consider, for instance, the following two inferences:

(1) “Tea-drinking is common in England. Therefore: Either tea-drinking is common in England or all New Zealanders ought to be shot”,

formalized as:

(1′)   ddOs,

and

(2) “Tea-drinking is common in England, or all New Zealanders ought to be shot. Tea-drinking is not common in England. Therefore, all New Zealanders ought to be shot”,

formalized as:

(2′) dOs, ¬dOs.

If the mixed sentence dOs is considered to be normative, then (1) is an example of an ‘is-ought’ inference, and if it is considered to be non-normative, then (2) is an example of an ‘is-ought’ inference. So, one of them dichotomically represents a violation of Hume's thesis in Prior's terms. Prior concluded from this paradox that Hume's ‘is-ought thesis’ is simply false (cf. Prior 1960, p. 206): one can simply derive conclusions which are ethical starting from premises which have no ethical character.

Prior recognized however that the inferences involved in the paradox are ethically irrelevant or trivial, but neither he nor later authors could find a suitable definition of what it would mean by “ethical irrelevance” or “ethical triviality” attached to an inference.

Using the semantics of modal logics, objections against this conclusion can be raised, as for example in Karmo 1988, in the sense of separating statements between evaluative in some possible worlds and descriptive in others (while keeping their meaning).

By using concepts of combinations of languages and combinations of logics, G. Schurz (cf. Schurz 1991; see also Schurz 1997) was able to state a generalized Hume's thesis (GH); as observed in Subsection 4.1, this treatment is in fact a fusion of two modal logics. In (GH) a mixed sentence φ is derived from a set of purely descriptive sentences (i.e., sentences free of O) only if φ is completely O-irrelevant (that is, predicates in φ within the scope of O can be replaced by other predicates salva valididate). Moreover, it is proven that (GH) holds in an alethic-deontic first-order logic L if, and only if, L can be axiomatized without bridge principles.

The notion of bridge principle lies in the scope of combination of languages. In general, many bridge principles can be made explicit within modal logic, and will be relevant for analyzing relationships among diverse modalities. For example, if we take necessity □ and possibility ◊ as primitive operators, then

p → ¬□¬p

is an intuitionistically acceptable bridge principle, while the converse is not.

Besides Hume's problem, another example of bimodal logic with intrinsic philosophical interest where bridge principles intervene is the logic of physical and alethic modalities. In this logic, the language permits the expression of two different notions of necessity: the logical necessity, symbolized by □, and the physical necessity, symbolized by ⊡.

The simplest connection between physical necessity and logical necessity that comprises an acceptable philosophical meaning is given by the following bridge axiom:

p → ⊡p

meaning that logical necessity is stronger than physical necessity: anything that is logically necessary is physically necessary.

The resulting logic KT is axiomatized by the well-known axioms and rules of KT for both modalities in addition to the bridge axiom above, and is semantically characterized by Kripke frames with two accessibility relations, requiring that the accessibility relation for physical necessity is included in the other.

Not only bimodal, but multimodal (also called polymodal) logics, are standard in the literature: a typical case is the logic of knowledge (or epistemic logic), usually endowed with modal operators K1, K2,…, Km representing the knowledge of m agents (or “knowers”). The formula Kiα means “agent i knows α”, and the language is able to express, for instance, “i knows that j does not know that i knows p” by means of Ki¬KjKip. No additional mixing principles are mandatory for the combined logic of many agents, but bridge axioms may of course be added.

The interest of studying combinations of logics may thus be seen as a reflex of the pluralist view of contemporary logical research. Indeed, this kind of bridge axioms can, in principle, connect completely distinct logics. Van Benthem (2006) suggests that combining logics may lead to the emergence of new phenomena, depending on the mode of combination, and moreover, it may work as an inspiration (and perhaps as a model) for the study of combining epistemic notions. He even suggests that the compartmentalization of logic into subfields as ‘modal’, ‘temporal’, ‘epistemic’, ‘doxastic’, ‘erotetic’ or ‘deontic’ logic has been harmful to Philosophical Logic.

Combinations of logics go in the opposite direction of such a compartmentalization: considering that almost any conceptual task to be analyzed involves immediate reasoning concerning necessity, obligation, action, time, verbal tense, knowledge, belief, etc.; from a philosophical point of view, logical combinations may be the right way to look at philosophical issues within the theory of causation, of action, and so on.

The idea of looking at logic as an entirety avoiding fragmentation is not new, and philosophers and logicians from Ramón Lull to Gottfried W. Leibniz have thought of building schemes where different logics or logic-like mechanisms could interact and cooperate instead of competing. In contemporary terms, the first methods for combining logics were products of logics (introduced by K. Segerberg (1973) and independently by V. Sehtman (1978)), fusion (introduced by R. Thomason (1984)) and fibring (introduced by D. Gabbay (1996a)), all of them dedicated to combining only modal logics. It is worth noting that M. Fitting (1969) gave early examples of fusion of modal logics, anticipating the notion of fusion.

Other combination mechanisms followed, such as parameterization and temporalization, which were more on the side of software specification.

Most of these methods have been encompassed in the algebraic fibring introduced by A. Sernadas, C. Sernadas and C. Caleiro (1999), which notoriously improved the versatility of these techniques by means of (universal) categorial constructions, in this way making it possible to combine wider classes of logics besides modal logics.

On the other hand, making heavy use of the language of category theory, J. Goguen and R. Burstall introduced the notion of institutions as a kind of abstract model theory devoted to applications in Computer Science (see Goguen and Burstall 1984 and Goguen and Burstall 1992). Institutions are also used as a mechanism for combining logics.

However, combining logics does not only mean synthesizing or composing logics, but can also yield interesting examples that go in the opposite direction of decomposing logics (see Section 2). A paradigmatic methodology for decomposition is the possible-translations semantics, a notion proposed in Carnielli 1990 designed to help solve the problem of assigning semantic interpretations to non-classical logics. Examples of possible-translations semantics illustrate how a complex logic can be analyzed into less complex factors. Another closely related technique is the nondeterministic semantics (cf. Avron and Lev 2001 and Avron and Lev 2005), whereas direct union of matrices and plain fibring (cf. Coniglio and Fernández 2005) can be considered to be methods for both composing and decomposing.

All of these methods open the way for a new subject in the realm of combinations of logics: is it possible to decompose a given logic into elementary ones? In other words, are there prime logics which, combined in an appropriate way, may produce all (or part of) the familiar logic systems?

Results on combinations of logics may quickly become too technical when we turn to the combination of higher-order, modal, relevance logics or non-truth-functional logics, and thus refinements of the notion of algebraic fibring such as modulated fibring (cf. Sernadas et al. 2002b) or cryptofibring (cf. Caleiro and Ramos 2007) may be necessary to solve, for example, some collapsing problems within combinations of logics (see Section 5). This naturally leads to the use of category theory as a universal language and as a tool to deal with such problems. But the fact is that combinations of logics do not necessarily depend upon any highly technical methodology, and even some relatively simple examples can be really expressive. There is a recognized intersection and interaction between Philosophy and theoretical Computer Science, and techniques for combining logics are also revealed to be very apt tools for handling and thus better understanding Kripke models. Having been introduced in the domain of Philosophical Logic, Kripke models are essential in Computer Science and Artificial Intelligence as semantic structures for logics of belief, knowledge, temporal logics, logics for actions, etc. Knowledge representation and reasoning may require combining several reasoning formalisms, including combinations of temporal reasoning, reasoning in description logic, reasoning about space and distance, and so on. Logics, combining temporal and modal dimensions, are also becoming a relevant tool in agent-oriented programming languages. Other applications of combinations of logics include software specification, knowledge representation, architectures for intelligent computing and quantum computing, security protocols and authentication, secure computation and zero-knowledge proof systems, besides their connections to formal ethics and game semantics.

The Belief-Desire-Intention model of agents (BDI) is concerned with the formal representation of practical reasoning involving action, intention, belief, will, deliberation, goal-driven modeling, etc. This kind of reasoning is essential for planning (especially for artificial agents). It is then just natural to think on combining simple modal logics for knowledge, belief, obligation, capability, opportunity, etc., so as to define more robust BDI logics. Governatori et al. 2002 investigates the relationships between BDI logics and a particular case of fibring semantics (which the authors call dovetailing), showing that a (general) logical account of BDI can be handled by means of dovetailing multimodal logics.

But combinations of logics also work form another perspective: instead of directly combining logic systems and looking for the interpretation of the resulting system, one can start from a purely mathematical perspective. In van Benthem et al. 2006, for instance, the authors introduce the notion of horizontal and vertical topologies on the product of topological spaces, and show that the modal logic of products of topological spaces with horizontal and vertical topologies coincides with the fusion of S4 with itself. The resulting completeness proof has deep connections with some topological properties of the real and of the rational numbers.

2. Splitting logics versus splicing logics

It is reasonable to expect that a method for combining logics would work in two opposite directions: on the one hand, a logic that one wants to investigate could be decomposed into factors of lesser complexity; for instance, a bimodal alethic-deontic logic could be decomposed into its alethic and deontic fragments. In this case, it would be relevant to see if the logic under investigation is the least extension of its factors, or if additional bridge principles would have to be added. This approach, in which a given logic is decomposed into (possibly) simpler factors, is said to be a process of splitting logics.

On the other hand, one might be interested in creating new logic systems where different aspects are integrated, starting from given logics. This demand typically occurs in software engineering and security: knowledge representation, formal specification and verification of algorithms and protocols have a marked need for working with several logics. In a less pragmatical scenery, this would be the case if one is interested, for instance, in adding a modal dimension to an intuitionistic or a paraconsistent logic. Moreover, it is interesting to characterize which properties of the factors can be transferred to the combined logic. This direction is said to be a process of splicing logics.

The essential distinctions between splicing (in the direction of synthesis) and splitting (in the direction of analysis) take into account the intentions one may have in mind, and consequently each direction encompasses specifically designed techniques.

The paradigm of splicing logics assumes a bottom-up perspective: it combines given logics, synthesizing them, and producing a new one. The combined logic should be minimal in some sense: that is, if L is obtained from L1 and L2 by some combination process, it should be expected that: 1) L extends both L1 and L2; and 2) L is a minimal extension of both L1 and L2. For instance, some methods may require L to be the least conservative extension of both L1 and L2. This point will be discussed in Section 5.

On the other hand, splitting a logic L assumes a top-down perspective: logics are decomposed into (presumably simpler) factors.

It should be stressed that most of the methods for combining logics found in the literature are better understood from the splicing perspective, placing prominence on the creation of a logic system from familiar logics. However, some splicing methods such as fusion (see Subsection 4.1) are more usefully regarded as a method of decomposition of logics into simpler fragments, and in this way also work in the splitting direction. Possible-translations semantics (see Subsection 4.4), on the other hand, constitute a typical method within the splitting perspective.

3. The importance of language and the presentation of logics

Suppose that two given logics L1 and L2 are to be combined using some technique. It should be obvious that any method applied to combine L1 and L2 will create a new logic L which contains the signature (logic symbols such as connectives, quantifiers, propositional variables etc.) of both logics: L will be defined in a mixed language, which allows combinations of symbols of the underlying languages. That is, a combination of logic systems presupposes the previous combination of the respective signatures. This is why the choice of the signature of the combined system is as important as the logic itself. For instance, the definition of the language of parameterization is fundamental in order to obtain the intended combined logic (see Subsection 4.5). Another example is found in Schurz 1991, where the formal treatment of Hume's ‘is-ought problem’ (recall Section 1) presupposes careful handling of subtle combinations of languages.

Besides the definition of the appropriate language for the combined logic, another important question that immediately arises is: should the logics L1 and L2 (to be combined) be presented in the same way? In other words: is it possible to combine logics defined by different paradigms? For instance, how could one combine a logic L1, defined by a sequent calculus, with a logic L2, represented by a (Hilbert-style) axiomatic system? How should the resulting logic L be represented: as a sequent calculus, as an axiomatic system or as a mixed proof system? Consider now another (even worse) situation: the logic L1 is described by semantical means (that is, through semantic structures such as valuations or Kripke models) whereas the logic L2 is presented through a syntactical proof system, such as a natural deduction system, sequent calculus or a Hilbert-style axiomatization. Could the resulting (combined) logic be better presented semantically or syntactically?

This annoyance does not occur in the majority of cases, where the logics being combined are complete with respect to some kind of semantics and are syntactically presented in an homogeneous way. However, it may happen that the logics are found in peculiar ways; for instance, linear logic and other substructural logics have no usual consequence relations because derivations are exclusively displayed by using multisets or sequences of formulas. Combinations of such logics with usual modal logics, for instance, are not so obvious, although both are complete.

Still, there are logics which are only reasonably presented by syntactical means, or exclusively by semantical means. Such is the case, e.g., of the first-order theory of torsion groups, known to be non-axiomatizable, and of incomplete modal logics which are only presented in syntactical (proof-theoretical) terms.

A possible solution to the problem of combining heterogeneous logics, which naturally leads us to the deeper question of “what is a logic?”, is to consider a common component of the majority of logics (but still excluding certain substructural logics): their respective consequence relations. Thus, given L1 and L2 presented in different ways, it is always possible to extract the respective consequence relations and then combine them (taking, for instance their supremum in an appropriate lattice of consequence relations). But in this way, the resulting logic L is presented in a very abstract way: the only information available from L is its consequence relation, and so the characteristics and particularities of each logic component are definitively lost.

Returning to the first example (combining a sequent calculus with an axiomatic system), a better solution was proposed in Cruz-Filipe et al. 2008: the idea is to define an abstract formalism for proof systems, general enough as to encode the main proof mechanisms found in the literature. Thus, after reformulating L1 and L2 as abstract proof systems of this kind, the resulting combined logic L is an abstract proof system in which it is possible to recognize the ‘genetic traces’ of the original inference rules of each components within derivations in L.

Despite these results on combining heterogeneous logics, it seems more reasonable to combine logics defined in an homogeneous way, and, in fact, this is the case with most of the proposals in the literature. For instance, the usual combinations of modal logics (as fusion, product and fibring) are performed between systems presented axiomatically, or between classes of Kripke models. It is frequent, therefore, to define different categories of logic systems (consequence relations, Hilbert calculi, algebraizable logics etc.) with appropriate morphisms between them, in which the combination (or decomposition) of logics appear as universal constructions. Algebraic fibring, to be described in Subsection 4.3, is a good example of this approach.

4. Methods for combining and decomposing logics

4.1 Fusion and Products

The method of fusion of normal modal logics was introduced by R. Thomason (1984), and constitutes one of the first general methods for combining logics. In the original formulation, it combines normal modal logics presented syntactically and semantically (through Hilbert-style axioms and Kripke semantics, respectively). The main characteristics of the method are described in the following paragraphs.

Consider Kripke models of the form

W, R, V

such that W is a non-empty set (the set of worlds), RW×W is a binary relation (the accessibility relation) and V: P → ℘(W) from the set P of propositional variables into the power set of W is a valuation map. Let L1 and L2 be two propositional normal modal logics defined over the same classical signature which contains the connectives ¬ (negation) and → (implication). Denote by □1 and □2 the necessity operators of L1 and L2, respectively. Let M1 and M2 be the classes of Kripke models for L1 and L2, respectively. Since both logics are normal, it is granted that both modalities □1 and □2 satisfy the normality axiom K and the necessitation rule. The fusion of L1 and L2 is then defined to be the normal bimodal logic L with two independent boxes □1 and □2 together with the connectives ¬ (negation) and → (implication). The semantics of L is given by the class M of Kripke structures of the form

W, R1, R2, V

such that ⟨W, R1, V⟩ and ⟨W, R2, V⟩ belong to M1 and M2, respectively. In other words, each structure of the fusion corresponds to a pair of models: a model ⟨W, R1, V⟩ for L1 and a model ⟨W, R2, V⟩ for L2 sharing the same set of worlds W. Technically speaking, each structure of the fusion has, as a reduct, a model of L1 and a model of L2.

Given a structure M = ⟨W, R1, R2, V⟩, the accessibility relation R1 is used to evaluate the box □1, whereas R2 is used to evaluate □2. Since the language of L is freely generated by the union of the signatures of L1 and L2, it contains mixed formulas such as φ = □1(□2pp). Now, the structure M satisfies φ above at a world wW if and only if, for every w1W such that w R1 w1, M satisfies (□2pp) at w1. But this means that, either there exists w2 such that w1 R2 w2 and w2V(p), or w1V(p).

As concerns axiomatics, a Hilbert calculus for L is obtained by joining up the (schema) axioms of both systems. Thus, L has, among others, two K axioms, two necessitation rules and just one Modus Ponens (because implication → is shared). Considering that the language of L has mixed formulas (as φ above), schema variables occurring in the schema rules of the given logics can now be replaced in L by mixed formulas. For instance, φ can be derived in L from the formula (□2pp) by an application of the necessitation rule for the box □1.

An interesting example of fusion appears in Schurz 1991, when an alethic-deontic logic is defined by fusing a pure alethic logic with a pure deontic logic. This combination is used to analyze Hume's ‘is-ought thesis’ (see Section 1 above) in formal terms. Other intuitively appealing examples of fusion are given in the pioneering paper Fitting 1969, where alethic and deontic modalities are fused (before the concept of fusion had ever been introduced).

Since then fusion has been a much worked theme. Important results are the applications of fusion to simulations and to the question of transfer of properties among modal logics. Simulations make the strength of normal monomodal logics explicit, as they can, in a sense, simulate all modal logics (see Kracht and Wolter 1999). With respect to transfers, the preservation of properties such as completeness, finite modal property, decidability and interpolation by fusion of modal logics was extensively studied in Fine and Schurz 1996. More general and deeper results in the same spirit were obtained in Kracht and Wolter 1991, and a survey of most of those results can be found in Kracht and Wolter 1997. These results show the robustness of fusion as a combination method within the scope of modal logics, for fulfilling the requirement of preserving the properties of the logics being combined.

The question of how completeness results (and other model-theoretical properties) can be transferred from a propositional modal logic to its quantificational counterpart, and from a monomodal quantified modal logic to their multimodal combinations by means of fusion, is investigated in Schurz 2010. The paper also deals with the question on how completeness can be transferred from quantified modal logic with rigid designators to the ones with non-rigid designators.

Rasga et al. 2010 defines a categorical approach of fusion for modal logic systems labelled with truth values, and it is shown that the preservation of completeness requires some careful assumptions, while soundness is preserved without further provisos. A wide variety of logics (besides modal logics) including several non-classical logics can be treated in this way.

An interesting note is that there is a notable difference between combining logics from the syntactical and from the semantical perspective. For instance, the joining of two Hilbert calculi should be intuitively obtained by simply putting together the axioms and rules of both logics, while the semantical counterpart is not so obviously determined. Regarding this, an alternative to fusion is the fibred semantics (see Subsection 4.2).

Fusion, even if it is a very natural method for combining modal logics, however, is not obviously extendable to combinations of non-normal modal logics with normal modal logics. Moreover, fusion is specifically designed for combining modal logics, and cannot be extended in an obvious way to logics of a different nature. Algebraic fibring, described in Subsection 4.3 below, constitutes a generalization of fusion (at the propositional level), and generally solves the question of combining logics.

Another early method for combining (modal) logics is the so-called product of modal logics. This mechanism, independently introduced in Segerberg 1973 and in Shehtman 1978, is appropriate to represent time-space information. Given two modal logics L1 and L2 as above, the product L1 ×L2 is the bimodal logic over the mixed signature (endowed with two boxes) characterized by the class of Kripke structures of the form

W1×W2, S1, S2, V1×V2

defined from Kripke models ⟨W1, R1, V1⟩ and ⟨W2, R2, V2⟩ for L1 and L2, respectively. The accessibility relations S1, S2 ⊆ (W1 ×W2) × (W1 ×W2) are defined as follows:

  • u1, u2S1w1, w2⟩ iff u1 R1 w1 and u2=w2;
  • u1, u2S2w1, w2⟩ iff u2 R2 w2 and u1=w1;
  • (V1×V2)(p) = V1(p) × V2(p).

A somewhat surprising feature of the product of modal logics is that some new interactions between modalities arise. These new valid formulas are a kind of bridge principles (recall Section 1). Using the standard notation ◊1φ for ¬□1¬φ (and analogously for ◊2) for the possibility operator, the following bridge principles are always valid in the product logic:

12p → ◊21p Commutativity 1
21p → ◊12p Commutativity 2
12p → □21p Church-Rosser property 1
21p → □12p Church-Rosser property 2

Due to such interactions it is not possible to directly obtain the Hilbert calculus for the product of two modal logics, as in the case of fusion. The bridge principles must be explicitly added to the union of the original axiomatics in order to ensure completeness.

As in the case of fusion, this technique does not allow a direct generalization to logics other than modal ones.

4.2 Fibring

The fibred semantics of modal logics was originally proposed by D. Gabbay (1996a and 1996b) (see also Gabbay 1999). As in the case of fusion and products, the mechanism of fibring also applies to modal logics only. Assume the same notation as in Subsection 4.1. Thus, given L1 and L2, we start by defining the fibred language (or the fibring of the languages), which is the language generated by □1, □2, ¬ and → from the propositional variables. The basic idea is to consider Kripke models with distinguished (actual) worlds together with two transfer mappings: h1 from the set of worlds of the class of models M1 of L1 into the class of models M2 of L2, and h2 from the set of worlds of the class of models M2 of L2 into the class of models M1 of L1. When a Kripke model of L1 has to evaluate a formula of the form □2φ at the actual world w1, the validity checking is then transferred to the validity checking of □2φ within the Kripke model h1(w1) at its actual world. The evaluation of a formula of the form □1φ within a Kripke model of L2 at the actual world w2 is performed analogously, but now using the map h2.

Thus, the fibring by functions of L1 and L2 is a normal bimodal logic characterized semantically as follows: let

h1: mM1 WmmM2 {⟨m, w⟩ : wWm}

and

h2: mM2 WmmM1 {⟨m, w⟩ : wWm}

be a pair of transfer mappings. For simplicity, we assume that the sets of worlds Wm of mM1 are pairwise disjoint, and the same holds for M2. Given mM1M2, wWm and a formula φ in the fibred language, the satisfaction of φ in ⟨h1, h2, m, w⟩, denoted by ⟨h1, h2, m, w⟩ ⊩ φ, is defined recursively as usual whenever the main connective of φ is Boolean (¬ or →), or when φ is atomic. For the modalities, satisfaction is defined as follows: suppose (without loss of generality) that mM1, and let h1(w) = ⟨m2, w2⟩, with m = ⟨Wm, Rm, Vm⟩ and m2=⟨Wm2, Rm2, Vm2⟩. Then:

  • h1, h2, m, w⟩ ⊩ □1φ
    iff ⟨h1, h2, m, w1⟩ ⊩ φ, for every w1 such that w Rm w1;
  • h1, h2, m, w⟩ ⊩ □2φ
    iff ⟨h1, h2, m2, w2⟩ ⊩ □2φ
    iff ⟨h1, h2, m2, w3⟩ ⊩ φ, for every w3 such that w2 Rm2 w3.

The definition of ⟨h1, h2, m, w⟩ ⊩ □iφ for i=1,2 and mM2 is analogous.

Then, ⟨h1, h2⟩ satisfies φ, denoted by ⟨h1, h2⟩ ⊩ φ, if ⟨h1, h2, m, w⟩ ⊩ φ for every mM1M2 and wWm. Finally, φ is valid in the fibred semantics whenever ⟨h1, h2⟩ ⊩ φ for every pair ⟨h1, h2⟩ as above.

For instance, given h1, h2 as above, let ⟨W2, R2, V2⟩ ∈ M2 and w2W2 such that h2(w2) = ⟨⟨W1, R1, V1⟩, w1⟩. Then:

h1, h2, ⟨W2, R2, V2⟩, w2⟩ ⊩ □12¬p
iff h1, h2, ⟨W1, R1, V1⟩, w1⟩ ⊩ □12¬p
iff h1, h2, ⟨W1, R1, V1⟩, w1⟩ ⊩ □2¬p, for every w1 such that w1R1w1.

Suppose that h1(w1) = ⟨⟨W2, R2, V2⟩, w2⟩. Then, the latter is valid iff ⟨h1, h2, ⟨W2, R2, V2⟩, w2⟩ ⊩ □2¬p, for every w1 such that w1R1w1; i.e., for every w1 such that w1R1w1 and for every w2 such that w2R2w2, ⟨h1, h2, ⟨W2, R2, V2⟩, w2⟩ ⊩ ¬p. This is equivalent to say that, for every w1 such that w1R1w1 and for every w2 such that w2R2w2, w2V ′2(p).

With respect to axiomatics, the logics obtained by fibring (or by a variant of fibring called dovetailing) can, in some cases, be axiomatized by the union of the (schema) axioms of the given logics. But some logics may require the addition of some new bridge principles (mixing rules and axioms) in order to ensure the preservation of completeness. This may explain some discrepancy between the approaches of fusion and fibring; the completeness of fibring as exposed in Gabbay 1999 does not work exactly as a substitute for more technically intricate completeness proofs as in Kracht and Wolter 1991 and in Fine and Schurz 1996. For more on this discussion, see Kracht 2004.

The technique of fibring by functions is an interesting alternative to fusion and products, but, as much as its competitors, it cannot be extended to non-modal logics in any obvious way (see Coniglio and Fernández 2005 for an adaptation of the method of fibring by functions to matrix logics). One reason for the failure of fibring by functions to what concerns generalizations is that it is not a universal construction (in categorial terms). Moreover, the lack of a systematic definition of the axiomatization for the logics obtained by fibring is another negative aspect of this technique. The next subsection describes a categorial generalization of fibring which solves all the mentioned problems.

4.3 Algebraic Fibring

In order to overcome the limitations of the original method of fibring as exposed in the last subsection, A. Sernadas and collaborators propose, in Sernadas et al. 1999, a general definition of fibring using the conceptual tools of category theory. The central idea of the generalization is simple: suppose that L1 and L2 are two propositional logics which are to be combined. Suppose, for simplicity, that no connectives are to be shared, that is, the language of the logic L to be obtained is the free combination of the connectives of both logics. In categorial terms, the signature C of L is the coproduct (disjoint union) of the signatures, C1 of L1 and C2 of L2, in the underlying category of signatures. Then L, which is the least logic defined over C which extends simultaneously L1 and L2, is defined as the coproduct of L1 and L2 in the underlying category of logics. The minimality of L attends a criterion expressed in Gabbay 1999 (see also Section 5) and also conforms to the ideal of fusing logics, cf. Kracht and Wolter 1991. This combination process, called unconstrained fibring, can be generalized, by allowing C1 and C2 to share some connectives. Thus, the logic obtained by this second kind of fibring is defined in a language such that some connectives of L1 and L2 are identified. The logic produced by this operation, called constrained fibring, starts by considering two logics L1 and L2 over signatures C1 and C2, respectively, and a signature C0 contained in both C1 and C2. This signature contains exactly the connectives of L1 and L2 which are to be identified (or shared) throughout the combination process. After computing the unconstrained fibring (that is, the coproduct) L1L2 of L1 and L2, which is defined over the signature C1C2 (the coproduct of C1 and C2), a new logic L is obtained. This logic, the fibring of L1 and L2 by sharing (or constrained to) C0, is obtained from L1L2 by identifying two connectives (of the same arity) iff both come from the same connective in C0. In terms of category theory, it is required that the forgetful functor N from the category of logics to the category of signatures be a cofibration. Then, if ij : C0Cj is the inclusion morphism (for j=1,2), hj : CjC1C2 is the canonical injection of the coproduct (for j=1,2) and q : C1C2C is the coequalizer of h1i1 and h2i2, then the constrained fibring L is the codomain of the cocartesian lifting of q by N.

In order to exemplify the technique of categorial fibring (without entering into technical details), suppose that L1 and L2 are two modal logics defined through Hilbert calculi over the same signatures C1 and C2 of Subsections 4.1 and 4.2, respectively, such that both logics contain the rules of Modus Ponens and necessitation. Then C1C2 consists of two negations ¬1 and ¬2, two implications →1 and →2 and two boxes □1 and □2. The unconstrained fibring L1L2 of L1 and L2 is therefore the Hilbert calculus over C1C2 defined by joining up the axiom schemas and inference rules of both calculi. This logic has, among other axioms and inference rules, two versions of Modus Ponens (one for each implication) as well as two versions of the necessitation rule (one for each box). It should be noted that, by using a fixed set of schema variables for writing the axioms and rules of every calculus, the calculi obtained by fibring are also formed by schematic axioms and inference rules. Thus, for instance, in the rule of Modus Ponens in L:

ξ1       (ξ11 ξ2)
ξ2

the schema variables ξ1 and ξ2 can be replaced by mixed formulas. Instances such as

¬2 p      ¬2 p12(q21r)
2(q21r)

are new, because the formulas ¬2 p and □2(q21r) do not belong to the language of L1. Analogous replacements apply, of course, to other inference rules and axioms of L1L2.

Continuing with this example, suppose now that we want to share (or identify) both negations, as well as both implications: this is a reasonable move when, for instance, these connectives are classic. In such a case (φ →1 ¬2 ψ) would represent the same proposition as (φ →2 ¬1 ψ).

In order to do this, the signature C0 just containing ¬ and → is taken into consideration, and so ¬1 is identified with ¬2 in C1C2, as well as →1 is identified with →2. The resulting signature is C, which just contains the connectives ¬, →, □1 and □2. In the resulting logic L, defined over C, there is now just one rule of Modus Ponens:

ξ1       (ξ1 → ξ2)
ξ2

However, there remain two necessitation rules, since there are still two boxes in C. The resulting L is thus the fibring of L1 and L2 constrained by C0. This procedure precisely coincides with fusion of modal logics. The novelty here is that this technique applies to a broad class of logics, which are not necessarily restricted to (normal) modal logics, as in the case of fusion.

Constrained and unconstrained fibring, being categorial, are universal constructions, and so enjoy well-defined and theoretically predictable formal properties. Profiting from universal constructions, in order to handle algebraic fibring, it is enough to define appropriate categories of signatures and logic systems. Indeed, the same fibring construction (coproduct or cocartesian lifting) can be performed in different categories of logic systems. This is a remarkable advantage of the categorial perspective for fibring. There are several proposals in the literature devoted to combining logics presented in different ways by means of algebraic fibring: propositional Hilbert calculi, first-order modal logics, higher-order modal logics, non-truth-functional logics, logics semantically presented through ordered algebras (encompassing generalized Kripke models) etc.

An important question connected to combination of logics (and, in particular, to algebraic fibring) is the preservation of metaproperties such as completeness, interpolation etc. For instance, when L1 and L2 are complete logic systems presented both semantically and syntactically, under which condition is their fibring also complete? In this regard, Zanardo et al. 2001 and Sernadas et al. 2002a give a partial solution to this question. On the other hand, transfer results have been extensively studied in the case of fusion of modal logics, as already mentioned in Subsection 4.1.

The relationship between fusion and algebraic fibring deserves some comments. When restricted to modal propositional logics, fusion is a particular case of algebraic fibring in the category of interpretation systems, where logics are presented through ordered algebras: it is enough to consider interpretation systems defined over power set algebras induced by Kripke models. At the syntactical level, fusion is also a particular case of algebraic fibring in the category of Hilbert calculi, in the realm of propositional signatures. As much as first-order modal logics are concerned, the approaches diverge, mainly because there are different semantical accounts for treating first-order modalities. For instance, the semantical approach to modal first-order logics by Sernadas et al., 2002a in the context of algebraic fibring differs to that of Kracht and Kutz 2002 in the context of fusion.

The fact that algebraic fibring generalizes (at least at the propositional level) the fusion of modal logics makes the former method become very natural and useful. Moreover, the universality of the construction allows one to define algebraic fibring in very different logical contexts (categories of logics), such as non-truth-functional logics, higher-order logics, sequent calculi etc. As it will be shown in Section 5, the different notions of morphisms between logics affect the strength of the logics obtained by algebraic fibring in the different categories of logic systems. For general accounts of algebraic fibring see, for instance, Caleiro et al. 2005 and Carnielli et al. 2008.

4.4 Possible-Translations Semantics

The methods for combining logics described above adhere to the splicing methodology: they are used to combine logics creating new systems which extend the given logics.

As mentioned in Section 2, there is a converse direction: the splitting methodology in which a given logic system is decomposed into other systems. The possible-translations semantics (in short, PTS), introduced in Carnielli 1990 (see also Carnielli 2000), is one of the few supporters of this viewpoint.

The notion of PTS was originally defined as an attempt to endow certain logics with recursive and palatable semantic interpretations. Actually, several paraconsistent logics which are not characterizable by finite matrices can be characterized by suitable combinations of many-valued logics. The idea of the decomposition is quite natural: given a logic L, presented as a pair L = ⟨C, ⊢L⟩ in which C is a signature and ⊢L is a consequence relation, a family of translations f i : L(C) → L(Ci) (for iI) is taken into consideration. Here, L(C) and L(Ci) denote the algebra of formulas defined by the signature C and Ci, respectively. Recall that a translation from a logic L into a logic L′ is a mapping f between the respective sets of formulas which preserves derivability, that is: Γ⊢Lφ (in the source logic L) implies that f( Γ) ⊢Lf(φ) (in the target logic L′).

A pair P = ⟨{Li}iI, {f i}iI⟩ as above is called a possible-translations frame for L. We say that P is a possible-translations semantics for L if, for every Γ∪{φ} ⊆ L(C),

Γ⊢L φ iff  fi(Γ) ⊢Li f i(φ), for every iI.

This means that checking derivability in L is equivalent to checking derivability in every factor logic Li through the translations. In many cases, the factor logics Li are presented by finite matrices. Since the length of a formula is finite, it is enough to test a finite number of translations in order to determine if a formula of L is valid in L. Thus, checking the validity of a formula of L is equivalent to performing a finite number of finitary tests. This decidability property is of real advantage when the original logic L is not characterizable by finite matrices. For instance, in Carnielli 2000 (see also Marcos 1999) the well-known hierarchy {Cn}n ∈ ℕ of paraconsistent logics, formed by logics which cannot be characterized by finite matrices, is represented by means of a PTS whose factors are presented through finite matrices; this grants a decision procedure for each logic Cn.

In order to exemplify the concept of PTS as a splitting methodology, consider the paraconsistent logic bC, introduced in Carnielli and Marcos 2002. This logic is, in particular, a logic of formal inconsistency, in the sense that there exists a unary connective ○ expressing the consistency of a formula. Thus, from φ and ¬φ does not follow, in general, an arbitrary formula ψ. However, {φ,¬φ, ○φ} entails any formula ψ. The signature C of bC consists of a paraconsistent negation ¬, a consistency operator ○, and classical connectives ∧,∨,→. It was proved in Carnielli et al. 2007 that bC, and many other logics of formal inconsistency extending it, cannot be characterized by finite matrices. Nonetheless, bC is decomposed into several copies of a three-valued logic by means of possible-translations as follows: consider the signature C1 = {¬12, ○1, ○2, ○3, ∧, ∨, →} consisting of two negations, three consistency operators, a conjunction, a disjunction and an implication. Let M be the matrix over C1 with domain {T, t, F} displayed below, where {T, t} is the set of designated values.

T t F
T t t F
t t t F
F F F F
T t F
T t t t
t t t t
F t t F
T t F
T t t F
t t t F
F t t t
¬1 ¬2
T F F
t F t
F T T
1 2 3
T T t F
t F t F
F T t F

Let {f i}iI be the family of all the mappings f : L(C) → L(C1) satisfying clauses (tr0), (tr1), (tr2), (tr3) and (tr4) below.

(tr0) f(p) = p, for p a propositional variable;
(tr1) f(¬φ) ∈ {¬1 f(φ), ¬2 f(φ)}
(tr2) f(φ#ψ) = (f(φ)#f(ψ)), for # ∈ {∧, ∨, →}
(tr3) f(○φ) ∈ {○1 f(φ),○2 f(φ), ○3 f(φ)}
(tr4) if f(¬φ) = ¬2 f(φ), then f(○φ) = ○1 f(φ)

The family of mappings {f i}iI can be shown to define a PTS which characterizes bC in a decidable way (cf. Carnielli et al. 2008). As an example, it can be easily checked that φ∧¬φ → ¬○φ is a theorem of bC: just consider all its finitely many translations and test all of them to verify that they are three-valued tautologies. On the other hand, φ∧¬φ → ○φ is not a theorem of bC, which can be promptly verified by showing that at least one of its translations is not a tautology using the three-valued tables above. For an alternative PTS characterization of bC and related logics see Marcos 2008.

This example shows that a non-truth functional connective, such as the paraconsistent negation ¬ or the consistency operator ○ of bC, can be mimicked by interpreting it (via translations) into different truth-functional connectives. This is the idea behind A. Avron and I. Lev's non-deterministic semantics introduced in Avron and Lev 2001 (see also Avron and Lev 2005). This semantics generalizes logical matrices by considering that multifunctions (rather than functions) interpret the connectives.

As a matter of fact, non-deterministic semantics can be simulated by appropriate possible-translations semantics (cf. Carnielli and Coniglio 2005). In particular, the familiar matrix semantics are a specific case of possible-translations semantics, as well as the historical examples of translations between logics found in the literature. These facts provide evidence that possible-translations semantics are a widely applicable conceptual tool for decomposing logics.

4.5 Temporalization, Parameterization and Institutions

Apart from the logical and philosophical import of combining logics, a genuine interest exists in developing applications based on these techniques. One of the main areas interested in the methods for combining logics is software specification. Certain techniques for combining logics were developed almost exclusively with the aim of applying them to this area. In this section some of these methods will be briefly mentioned: temporalization, parameterization and institutions.

Temporalization was introduced in Finger and Gabbay 1992 (see also Finger and Gabbay 1996), and generalized in Caleiro et al. 1999 towards the method called parameterization.

Parameterization, in rough terms, consists of replacing the atomic part of a given logic L by another logic L′. Thus, the logic L is the parameterized logic; the atomic part is the formal parameter and the logic L′ is the parameter logic. Formally, a mixed signature based on the signature of L is considered, to which the formulas of L′ are added as constants. In the particular case of temporalization, the parameter logic is a temporal logic. In turn, it can be proven that parameterization is a particular case of constrained fibring (recall Subsection 4.3).

The method can be explained by means of a simple example taken from Carnielli et al. 2008: consider a propositional modal logic L, to be parameterized with first-order logic Lfol in order to describe the dynamics of data bases. The resulting logic is defined in a language whose formulas are obtained by replacing propositional constants in formulas of L by first-order formulas. That is, modalities can be freely used, but quantifiers cannot be applied to modal formulas (other propositional connectives such as negation and implication are shared).

The semantic structures for the new logic are Kripke structures where the valuation for propositional constants is replaced by a kind of “zooming in” mapping (in the sense of Blackburn and de Rijke 1997) associating a first-order semantic structure together with a fixed assignment for individual variables to each state.

The deductive system for the new logic is formed by the rules of both logics. The rules of L can be instantiated with formulas of the parameterized language, but the rules of first-order logic can only be applied to pure first-order formulas.

One important difference between parameterization (in particular, temporalization) and constrained fibring is the degree of symmetry: the parameterized language and inference rules are intrinsically asymmetric, while this is not the case for constrained fibring.

Institutions were introduced by J. Goguen and R. Burstall (see Goguen and Burstall 1984 and Goguen and Burstall 1992) as a kind of “abstract model theory” for Computer Science, and are adequate for developing concepts of specification languages such as structuring of specifications and implementation.

The theory of institutions is mainly applicable to software specification defined by multiple logical systems (see, for instance, Diaconescu and Futatsugi 2002). Thus, under an abstract view of software development, different components of the same program can be specified using different formalism in an heterogeneous setting. This is formalized by the use of institutions and morphisms between them (see, for instance, Tarlecki 2000). A problem concerning institution morphisms is that formulas involving connectives from different logics being combined are not allowed. A solution to this problem was proposed in Goguen and Burstall 1986 and Mossakowski 1996 by using the so-called parchments and parchment morphisms.

4.6 New perspectives: representing and combining logics by means of multi-graphs

Despite the fact that algebraic fibring is suitable for combining an ample class of logic systems, some kinds of logics, namely substructural logics such as linear logic, and logics equipped with a nondeterministic semantics, lie outside the scope of this combination method. Morever, at the semantical level, algebraic fibring, by its own nature, does not make possible to keep representatives of all the models of the original logics (which leads to the collapsing problem of fibring, see Section 5).

With the aim of still enlarging the range of application of algebraic fibring, so as to make it able to deal with subestructural logics and with logics endowed with nondeterministic semantics, as well as to combine pointwise models of each logic, a formalism for representing logics and their combinations based on the general notion of multi-graphs (or, for short, m-graphs) was proposed by A. Sernadas and his collaborators (cf. Sernadas et al. 2009a and Sernadas et al. 2009b). Multi-graphs are graphs where the source of each edge is a finite sequence of nodes (instead of a unique node). Concerning signatures, the nodes of the m-graph are seen as sorts and the m-edges are seen as language constructors. From the semantical viewpoint, nodes are truth-values and m-edges are relations between truth-values. Finally, concerning deductive systems, nodes are language expressions, and m-edges are inference rules. The fibring of logics described by m-graphs (a.k.a. graph-theoretic fibring) is defined by pointwise combining models of each combined logic, in contrast to the usual notion of semantic fibring in which entire classes of models are combined. This allows one to avoid the collapsing problem (see the next section) in a very natural way.

As an immediate application of this graph-theoretic setting, the preservation of the finite-model property by graph-theoretic fibring was proved in Coniglio et al. 2011. Since (under reasonable conditions) the finite model property entails decidability, this result is particularly useful.

Another application to the graph-theoretic account of logic is the definition of an asymmetric combination technique called importing logics (cf. Rasga et al. 2011). Temporalization, as well as its generalization, modalization (see Fajardo and Finger 2003 and Finger and Weiss 2002), are particular cases of importing logics. Under this approach, the combined language is endowed with an explicit constructor called importing connective which transforms formulas of the imported logic into formulas of the importing logic. This is the main difference between the technique of importing logics and the related technique of parameterization (which also generalizes temporalization). Semantically, each model of the resulting logic obtained by the method of importing logics is a pair composed of a model of the importing logic and a model of the imported logic, plus the interpretation of the importing connective.

5. Lack or excess of interaction: perplexities when combining logics

Up to this point, several techniques for composing logics have been described and exemplified. Are these processes appropriate for composing, without surprises, any pair of logics? In other words, given a pair of logics (presented in an homogeneous way), are they composable in a meaningful way? Does the composition make philosophical sense? As pointed by Schurz 1991, it is conceivable that some multimodal logics obtained as combination of modal logics by adding arbitrarily chosen bridge principles could be meaningless.

From the technical point of view, there is an important problem concerning composition of logics known as the collapsing problem, first identified in Gabbay 1996b, and later formalized in del Cerro and Herzig 1996. In the latter paper, it is shown that, by freely combining classical propositional logic and intuitionistic propositional logic at the semantical level (technically: by computing their unconstrained fibring in the category of interpretation systems, recall Subsection 4.3), the resulting logic collapses to classical logic. More precisely, the resulting logic will consist of two twin copies of classical propositional logic having two negations, two implications and so on. Clearly, the respective copies of each connective will be proved to be inter-derivable in the resulting logic: ¬1 φ will be equivalent to ¬2φ, (φ →1 ψ) will be equivalent to (φ →2 ψ) and so on. The collapse only happens when considering the algebraic fibring at the semantical level: in Caleiro and Ramos 2007 was shown that the collapse does not occur when computing the algebraic fibring of the respective Hilbert calculi.

Basically, the phenomenon arises because both implications collapse, and then intuitionistic implication becomes classic. From the semantical point of view, it happens that the models of the fibred logic are Heyting algebras which are simultaneously Boolean algebras: evidently, the algebras collapse to the Boolean ones. From the point of view of proof theory, the problem appears as a consequence of the metaproperty called Deduction Metatheorem (DMT): let →1 and →2 be the intuitionistic and the classical implications, respectively. Then

Γ,φ⊢ψ iff Γ⊢(φ→1ψ)
Γ,φ⊢ψ iff Γ⊢(φ→2ψ).

Thus, the following argument applies (cf. Gabbay 1996b):

(φ →1 ψ) ⊢ (φ→1ψ)    Axiom
(φ →1 ψ), φ ⊢ ψ    DMT for →1
(φ →1 ψ) ⊢ (φ →2 ψ)    DMT for →2

A similar argument shows that (φ →2 ψ) ⊢ (φ →1 ψ). That is, classical and intuitionistic implications collapse in the combined logic.

It is worth noting that the previous arguments depart from a very strong assumption: that the metaproperty DMT is preserved in the combined logic. As we shall see below, this is not the case for algebraic fibring, unless a stronger notion of morphism between logics is adopted.

In Sernadas et al. 2002b, other examples of collapse were presented, and a solution to the problem was proposed by means of a controlled notion of algebraic fibring called modulated fibring. An apparently simpler solution to the collapsing problem appeared in Caleiro and Ramos 2007, using a variant of the algebraic fibring technique called cryptofibring. As mentioned in Subsection 4.6, the graph-theoretic fibring leads to an additional solution to this problem. More recently, another solution to the collapsing problem was obtained by means of a new technique called meet combination of logics (cf. Sernadas et al. 2011b), based on the idea of melding the connectives of two given logics being combined. The melded connectives of the resulting logic inherit the common properties enjoyed in both logics, instead of the union of their properties, as it occurs in the case of the shared connectives of constrained fibring. A particular case of this technique was presented in Sernadas et al. 2011a.

Independently, in Béziau 2004, it was observed that by putting together the sequent rules for classical conjunction and the rules for classical disjunction, the resulting sequent calculus will (unexpectedly) prove the distributivity between conjunction and disjunction. The same phenomenon occurs if we join the (two-valued) valuation clauses for classical conjunction with the valuation clauses for classical disjunction. However, this is avoided by considering algebraic fibring in the usual categories (Hilbert calculi or consequence relations) with translations between logics as morphisms: the logic obtained is the logic of lattices, which does not satisfy distributivity (see Béziau and Coniglio 2011).

This situation, in which new interaction rules between the connectives arise, is arguably undesirable. In fact, it contradicts a basic criterion of fibring (and also of fusion), as expressed in Gabbay 1999: given logic systems L1 and L2, the combination of L1 and L2 should be the smallest logic system in the combined language which is a conservative extension of both L1 and L2.

Indeed, the distributivity problem and the collapsing problem are two instances of the same phenomenon of emergence of unexpected interactions (such as bridge principles) between connectives caused by combination processes. In the case of combination of conjunction with disjunction, the distributive law emerges: this interaction is due to the combination process and appears without any apparent reason. In turn, the collapsing problem is a limit case of interactions: the interderivability between classical and intuitionistic implications (nothing else than two interaction laws between different connectives) is also spontaneously created by the combination process.

It can be argued that the combined logics are excessively strong in such cases, because they derive too many propositions in the new combined language.

On the other hand, the opposite (or dual) situation may also be problematic: suppose, to help intuition, that the logic of classical negation is combined with the logic of classical disjunction. These logics can be presented, for instance, axiomatically (through Hilbert calculi) or semantically, say, through valuations over {0,1} (that is, by means of classical truth-tables). The semantical presentation of the logic of classical negation consists of the set of all valuations over {0,1} satisfying the following clause:

v(¬φ) = 0 iff v(φ) = 1.

On the other hand, the logic of classical disjunction can be characterized by the set of all valuations over {0,1} such that:

v(φ ∨ ψ) = 0 iff v(φ) = 0 and v(ψ) = 0.

As a consequence, the combined logic of negation and disjunction (which can be defined as the logic over ¬ and ∨ characterized by the valuations over {0,1} satisfying both clauses above) validates (φ∨¬φ), and so classical logic is recovered. This is the result obtained by the combination method called direct union of matrices, introduced in Coniglio and Fernández 2005. However, if algebraic fibring is considered in categories such as those of Hilbert calculi or consequence relations, the combination between the logic of negation and the logic of disjunction results in a logic defined over ¬ and ∨, which is weaker than classical logic: the interaction law (φ∨¬φ) is no longer valid. That is, an arguably desirable interaction between the connectives is lost in the combination process, and classical logic over ¬ and ∨ cannot be recovered from its fragments, as long as algebraic fibring in these categories of logics is used.

Another example of the same kind is the following: the algebraic fibring between the logic of classical negation ¬ and the logic of classical implication → performed in the categories above does not recover classical logic over ¬ and →. Indeed, the resulting logic system, defined over ¬ and →, cannot validate Ex Contradictione Sequitur Quodlibet when presented as an axiom:

⊬(φ → (¬φ → ψ)).

Interestingly enough, Ex Contradictione Sequitur Quodlibet, presented as a derivation, holds in the fibred logic:

φ, ¬φ ⊢ ψ.

Observe that (φ → (¬φ → ψ)) is an interaction rule between the connectives of the logics being combined which cannot be obtained by algebraic fibring in the categories under consideration (however, this principle can be recovered, e.g., by direct union of matrices). If one is interested in recovering a logic from its fragments, this result is disappointing.

These examples as well as others along the same lines suggest a problem dual to that of collapsing and distributivity between conjunction and disjunction: some expected interaction laws fail to be created by some combination processes.

In such cases, it could be said that the combined logics are too weak, because they are unable to derive certain intended propositions in the new combined language.

What could be expected when combining logics? Strong logics (guaranteeing, for instance, that a logic can be recovered from its fragments) or weaker ones (in which undesirable interactions between connectives are blocked)?

The examples above are evidence against and in favor of both situations: in order to avoid the collapsing problem, a careful splicing process should be expected (and so the interaction between both implications would disappear). On the other hand, if one wants to recover, say, classical logics from its fragments, a more liberal splicing process would be more appropriate, as some intended interactions between connectives of both logics would be recovered.

With respect to the distributivity problem when combining conjunction and disjunction, the choice of method is also not determined: distributivity could be a desired feature if we adopted the viewpoint of recovering a logic from its fragments. In this case, a combination method defining a stronger logic (such as direct union of matrices) would be more appropriate than, for instance, algebraic fibring of Hilbert calculi. If, as argued in Béziau 2004, distributivity is regarded as an intruder, then a more careful process would be recommended: algebraic fibring would be more appropriate in this case. To sum up: the choice of the more adequate combining process depends upon what one wants to obtain.

At this point, it is convenient to notice that the question about whether or not interactive principles are generated when combining modal logics is intrinsically related to Hume's ‘is-ought problem’ discussed in Section 1. Indeed, as proven in Schurz 1991, it is possible to obtain nontrivial ‘is-ought’ deductions in the combination of alethic and deontic logics provided that some bridge principles are allowed. Bridge principles as Oφ → ◊φ are nothing else than interaction rules between connectives of the logics being combined. Such principles enjoy a similar conceptual status as the distributivity laws between conjunction and disjunction, or as the collapsing example mentioned above. Thus, in order to satisfy Hume's thesis, a combination process generating logics without interactions should be preferred. On the other hand, a combination process allowing the creation of interactions between the connectives could grant bridge principles violating Hume's thesis.

Finally, it is noteworthy to observe that algebraic fibring does not intrinsically forbid the emergence of interactions between connectives of the logics being combined. In fact, the notion of morphism in the category of logic systems being employed is the key to create or to block interactions. In order to exemplify this assertion, consider the case of the failure to recover classical logic from its {¬}-fragment and {∨}-fragment by algebraic fibring. The key reason for this failure is that the rule

(*) Γ, φ ⊢ ψ           Δ, ¬φ ⊢ ψ
Γ, Δ ⊢ ψ

of the logic of classical negation is not preserved by algebraic fibring in the categories of logic systems having translations between logics as morphisms (recall Subsection 4.4), such as the category of Hilbert calculi or consequence relations.

When considering algebraic fibring of classical implication with classical negation in those categories, the missing rule is the Deduction Metatheorem:

(**) Γ , φ ⊢ ψ
Γ ⊢ (φ → ψ)

Categories of logic systems having logic translations as morphisms are such that the canonical injections of the coproduct are just inclusion mappings. Then, given two logics L1 and L2, the only rules of these logics which are preserved by their algebraic fibring are those of the form:

Γ ⊢ φ

On the other hand, suppose a category of logic systems in which the preservation of rules such as (*) or (**) above is required by the very notion of morphism. Thus, if a logic L is obtained as a combination of two other systems L1 and L2 then the rules of L1 and L2 would be faithfully transferred to L. This is the proposal of Coniglio 2007, in which algebraic fibring in categories of sequent calculi is investigated, taking into account a notion of morphism which preserves logical rules of the form

If Γ1 ⊢ φ1 and … and Γn ⊢ φn, then Γ ⊢ φ.

In such categories, when a logic system is embedded into a larger one by algebraic fibring, any rule as above, which can be considered as a meta-theorem of the logic, is preserved by the canonical injections. This is why this process is called meta-fibring. From the categorial point of view, the process is the same as for algebraic fibring, the only difference being that the notion of morphism is stronger. This illustrates the advantages of using category theory and its tools for defining combination procedures as universal constructions: the same construction (in this case, algebraic fibring) can be performed in categories of logic systems with different features obtaining, as a consequence of this, stronger or weaker logic systems.

Bibliography

  • Avron, A. and Lev, I., 2001, “Canonical propositional Gentzen-type systems”, in Proceedings of the 1st International Joint Conference on Automated Reasoning (IJCAR 2001), volume 2083 of Lecture Notes in Artificial Intelligence, pp. 529–544, Springer Verlag.
  • Avron, A. and Lev, I., 2005, “Non-deterministic multiple-valued structures”, Journal of Logic and Computation, 15(3): 241–261.
  • Baumgardt, D., 1946, “Legendary quotations and lack of references”, Journal of the History of Ideas, 7(1): 99–102.
  • Béziau, J.-Y., 2004, “A paradox in the combination of logics”, in Carnielli, W., Dionísio, F., and Mateus, P., editors, Proceedings of CombLog'04 – Workshop on Combination of Logics: Theory and Applications, Lisbon (Portugal), pp. 76–77, Departamento de Matemática, Instituto Superior Técnico, Lisbon (Portugal).
  • Béziau, J.-Y. and Coniglio, M., 2011, “To Distribute or not to Distribute?”, Logic Journal of the IGPL, 19(4): 566–583.
  • Blackburn, P. and de Rijke, M., 1997, “Zooming in, zooming out”, Journal of Logic, Language and Information, 6(1): 5–31.
  • Caleiro, C., Carnielli, W., Rasga, J., and Sernadas, C., 2005, “Fibring of logics as a universal construction”, Volume 13 of Handbook of Philosophical Logic, 2nd Edition, pp. 123–187, Springer.
  • Caleiro, C. and Ramos, J., 2007, From fibring to cryptofibring: A solution to the collapsing problem. Logica Universalis, 1(1): 71–92.
  • Caleiro, C., Sernadas, C., and Sernadas, A., 1999, “Parameterisation of logics”, in Fiadeiro, J., editor, Recent Trends in Algebraic Development Techniques, volume 1589 of Lecture Notes in Computer Science, pp. 48–62. Springer.
  • Carnielli, W., 1990, “Many-valued logics and plausible reasoning”, in Proceedings of the XX International Congress on Many-Valued Logics, University of Charlotte, USA, pp. 328–335, IEEE Computer Society.
  • Carnielli, W., 2000, “Possible-Translations Semantics for Paraconsistent Logics”, in Batens, D., Mortensen, C., Priest, G., and Van Bendegem, J. P., editors, Frontiers of Paraconsistent Logic: Proceedings of the I World Congress on Paraconsistency, Logic and Computation Series, pp. 149–163. Baldock: Research Studies Press, King's College Publications.
  • Carnielli, W., Coniglio, M., Gabbay, D., Gouveia, P., and Sernadas, C., 2008, Analysis and Synthesis of Logics. Volume 35 of Applied Logic Series. Springer.
  • Carnielli, W., Coniglio, M., and Marcos, J., 2007, “Logics of Formal Inconsistency”, Volume 14 of Handbook of Philosophical Logic, 2nd Edition, pp 15–107. Springer. Preliminary version available at CLE e-Prints, 5(1), 2005, URL = http://www.cle.unicamp.br/e-prints/vol_5,n_1,2005.html.
  • Carnielli, W. and Coniglio, M., 2005, “Splitting logics”, in Artemov, S., Barringer, H., d'Avila Garcez, A. S., Lamb, L. C., and Woods, J., editors, We Will Show Them: Essays in Honour of Dov Gabbay, volume 1, pp. 389–414. College Publications.
  • Carnielli, W. and Marcos, J., 2002, “A taxonomy of C-systems”, in Carnielli, W., Coniglio, M., and D'Ottaviano, I., editors, Paraconsistency: the logical way to the inconsistent, Proceedings of WCP'2000, volume 228 of Lecture Notes in Pure and Applied Mathematics, Marcel Dekker.
  • Coniglio, M., 2007, “Recovering a logic from its fragments by meta-fibring”, Logica Universalis, 1(2): 1–39. Preliminary version available at CLE e-Prints, 5(4), 2005, URL = http://www.cle.unicamp.br/e-prints/vol_5,n_4,2005.html.
  • Coniglio, M. and Fernández, V., 2005, “Plain fibring and direct union of logics with matrix semantics”, in Prasad, B., editor, Proceedings of the 2nd Indian International Conference on Artificial Intelligence (IICAI 2005), Pune, India, pp. 1590–1608, IICAI.
  • Coniglio, M.E., Sernadas, A., and Sernadas, C., 2011, “Preservation a logic by fibring of the finite model property”, Journal of Logic and Computation, 21(2): 375–402.
  • Cruz-Filipe, L., Sernadas, A., and Sernadas, C., 2008, “Heterogeneous fibring of deductive systems via abstract proof systems”, Logic Journal of the IGPL, 16(2): 121–153.
  • del Cerro, L. F. and Herzig, A., 1996, Combining classical and intuitionistic logic, or: Intuitionistic implication as a conditional, in Baader, F. and Schulz, K., editors, Frontiers of Combining Systems: Proceedings of the 1st International Workshop, Munich (Germany), volume 3 of Applied Logic Series, pp. 93–102, Kluwer Academic Publishers.
  • Diaconescu, R. and Futatsugi, K., 2002, “Logical foundations of CAFEOBJ”, Theoretical Computer Science, 285(2): 289–318.
  • Epstein, R., 1995, The Semantic Foundations of Logic, Oxford University Press, 2nd edition, volume 1: Propositional logics, With the assistance and collaboration of W. Carnielli, I. D'Ottaviano, S. Krajewski and R. Maddux.
  • Fajardo, R. A. S. and Finger, M., 2003, “Non-normal modalisation”, in Balbiani, Ph., Suzuki, N.-Y., Wolter, F. and Zakharyaschev, M., editors, Advances in Modal Logic, Volume 4, pp. 83–95, King's College Publications.
  • Fine, K. and Schurz, G., 1996, “Transfer theorems for multimodal logics”, in Copeland, J., editor, Logic and Reality: Essays on the Legacy of Arthur Prior, Oxford, pp. 169–213, Oxford University Press.
  • Finger, M. and Gabbay, D., 1992, “Adding a temporal dimension to a logic system”, Journal of Logic, Language and Information, 1(3): 203–233.
  • Finger, M. and Gabbay, D., 1996, “Combining temporal logic systems”, Notre Dame Journal of Formal Logic, 37(2): 204–232.
  • Finger, M. and Weiss, M. A., 2002, “The unrestricted combination of temporal logic systems”, Logic Journal of the IGPL, 10(2): 165–189.
  • Fitting, M., 1969, “Logics with several modal operators”, Theoria, 35: 259–266.
  • Gabbay, D., 1996a, “Fibred semantics and the weaving of logics: Part 1”, Journal of Symbolic Logic, 61(4): 1057–1120.
  • Gabbay, D., 1996b, “An overview of fibred semantics and the combination of logics”, in F. Baader and K.U. Schulz, editors, Frontiers of Combining Systems: Proceedings of the 1st International Workshop FroCos'96, Munich (Germany), volume 3 of Applied Logic, pp. 1–55. Kluwer Academic Publishers.
  • Gabbay, D., 1999, Fibring Logics, volume 38 of Oxford Logic Guides, Oxford University Press, New York.
  • Goguen, J. and Burstall, R., 1986, “A study in the foundations of programming methodology: specifications, institutions, charters and parchments”, in Category Theory and Computer Programming, volume 240 of Lecture Notes in Computer Science, pp. 313–333, Springer.
  • Goguen, J. and Burstall, R., 1984, “Introducing institutions”, in Logics of Programs (Carnegie-Mellon University, June 1983), volume 164 of Lecture Notes in Computer Science, pp. 221–256, Springer.
  • Goguen, J. and Burstall, R., 1992, “Institutions: Abstract model theory for specification and programming”, Journal of the ACM, 39(1): 95–146.
  • Governatori, G., Padmanabhan, V. and Sattar, A., 2002, “On Fibring Semantics for BDI Logics”, in S. Flesca, S. Greco, N. Leone and G. Ianni, editors, Logics in Artificial Intelligence: European Conference – JELIA 2002, Volume 2424 of Lecture Notes in Computer Science, pp. 198–209, Springer.
  • Hume, D., 2000, In Norton, D. F. and Norton, M. J., editors, David Hume: A Treatise of Human Nature, Oxford University Press.
  • Karmo, T., 1988, “Some valid (but no sound) arguments trivially span the ‘Is’–‘Ought’ gap”, Mind, 97(386): 252–257.
  • Kracht, M., 2004, Review of Fibring Logics, by Dov Gabbay, Oxford Logic Guides, vol. 38, Oxford University Press, 1998, The Bulletin of Symbolic Logic 10(2): 209–211.
  • Kracht, M. and Kutz, O., 2002, “The semantics of modal predicate logic I: Counterpart-frames”, in F. Wolter, H. Wansing, M. de Rijke, and M. Zakharyaschev, editors, Advances in Modal Logic, Volume 3, pp. 299–320. World Scientific.
  • Kracht, M. and Wolter, F., 1991, “Properties of Independently Axiomatizable Bimodal Logics”, Journal of Symbolic Logic 56(4): 1469–1485.
  • Kracht, M. and Wolter, F., 1997, “Simulation and Transfer Results in Modal Logic – A Survey”, Studia Logica, 59(2): 149–177.
  • Kracht, M. and Wolter, F., 1999, “Normal monomodal logics can simulate all others”, Journal of Symbolic Logic, 64(1): 99–138.
  • Marcos, J., 1999, Semânticas de Traduções Possíveis (Possible-Translations Semantics, in Portuguese), Master's thesis, IFCH-UNICAMP, Campinas, Brazil.
  • Marcos, J., 2008, “Possible-translations semantics for some weak classically-based paraconsistent logics”, Journal of Applied Non-Classical Logics, 18(1): 7–28.
  • Mossakowski, T., 1996, “Using limits of parchments to systematically construct institutions of partial algebras”, in Haveraaen, M., Owe, O., and Dahl, O.-J., editors, Recent Trends in Data Type Specifications, volume 1130 of Lecture Notes in Computer Science, pp. 379–393, Springer.
  • Prior, A. N., 1960, “The autonomy of ethics”, Australasian Journal of Philosophy, 38(3): 199–206.
  • Rasga, J., Roggia, K., Sernadas, C., 2010, “Fusion of sequent modal logic systems labelled with truth values”, Logic Journal of the IGPL, 18(6): 893–920.
  • Rasga, J., Sernadas, A., and Sernadas, C., 2011, “Importing logics”, Studia Logica, in press.
  • Schurz, G., 1991, “How far can Hume's is-ought-thesis be generalized? An investigation in alethic-deontic modal predicate logic”, Journal of Philosophical Logic, 20: 37–95.
  • Schurz, G., 1997, The Is-Ought Problem: An Investigation in Philosophical Logic, Dordrecht: Kluwer.
  • Schurz, G., 2010, “Combinations and completeness transfer for quantified modal logics”, Logic Journal of IGPL, Advance Access, doi: 10.1093/jigpal/jzp085.
  • Segerberg, K., 1973, “Two-dimensional modal logic”, Journal of Philosophical Logic, 2(1): 77–96.
  • Shehtman, V., 1978, “Two-dimensional modal logics”, Akademiya Nauk SSSR. Matematicheskie Zametki, 23(5): 759–772.
  • Sernadas, A., Sernadas, C., and Caleiro, C., 1999, “Fibring of logics as a categorial construction”, Journal of Logic and Computation, 9(2): 149–179.
  • Sernadas, A., Sernadas, C. and Rasga, J., 2011a, “On combined connectives”, Logica Universalis, Advance Access, doi: 10.1007/s11787-011-0032-7.
  • Sernadas, A., Sernadas, C. and Rasga, J., 2011b, “On meet-combination of logics”, to appear.
  • Sernadas, A., Sernadas, C., Rasga, J. and Coniglio, M., 2009a, “A graph-theoretic account of logics”, Journal of Logic and Computation, 19(6): 1281–1320.
  • Sernadas, A., Sernadas, C., Rasga, J. and Coniglio, M., 2009b, “On graph-theoretic Fibring of logics”, Journal of Logic and Computation, 19(6): 1321–1357.
  • Sernadas, A., Sernadas, C., and Zanardo, A., 2002a, “Fibring modal first-order logics: Completeness preservation”, Logic Journal of the IGPL, 10(4): 413–451.
  • Sernadas, C., Rasga, J., and Carnielli, W., 2002b, “Modulated fibring and the collapsing problem”, Journal of Symbolic Logic, 67(4): 1541–1569.
  • Stuhlmann-Laeisz, R., 1983, Das Sein-Sollen-Problem. Eine modallogische Studie (problemata 96), Frommann-Holzboog, Stuttgart.
  • Tarlecki, A., 2000, “Towards heterogeneous specifications”, in Gabbay, D. and Rijke, M. D., editors, Frontiers of Combining Systems 2, Research Studies Press/Wiley.
  • Thomason, R., 1984, “Combinations of tense and modality”, volume 2 of Handbook of Philosophical Logic, pp. 135–165, Reidel.
  • van Benthem, J., 2006, “Epistemic logic and epistemology: the state of their affairs”, Philosophical Studies, 128(1): 49–76.
  • van Benthem, J., Bezhanishvili, G. ten Cate, B. and Sarenac, D., 2006, “Multimodal Logics of Products of Topologies”, Studia Logica, 84(3): 369–392.
  • Zanardo, A., Sernadas, A., and Sernadas, C., 2001, “Fibring: Completeness preservation”, Journal of Symbolic Logic, 66(1): 414–439.

Copyright © 2011 by
Walter Carnielli <walter.carnielli@cle.unicamp.br>
Marcelo Esteban Coniglio <coniglio@cle.unicamp.br>