ar X iv :2 00 3. 09 52 2v 2 [ m at h. L O ] 2 8 M ar 2 02 0 Logics of Formal Inconsistency enriched with replacement: an algebraic and modal account Walter Carnielli1, Marcelo E. Coniglio1 and David Fuenmayor2 1Institute of Philosophy and the Humanities IFCH, and Centre for Logic, Epistemology and the History of Science CLE University of Campinas, Brazil Email: {walterac,coniglio}@unicamp.br 2Freie Universität Berlin Berlin, Germany Email: david.fuenmayor@fu-berlin.de Abstract One of the most expected properties of a logical system is that it can be algebraizable, in the sense that an algebraic counterpart of the deductive machinery could be found. Since the inception of da Costa's paraconsistent calculi, an algebraic equivalent for such systems have been searched. It is known that these systems are non self-extensional (i.e., they do not satisfy the replacement property). More than this, they are not algebraizable in the sense of Blok-Pigozzi. The same negative results hold for several systems of the hierarchy of paraconsistent logics known as Logics of Formal Inconsistency (LFIs). Because of this, these logics are uniquely characterized by semantics of non-deterministic kind. This paper offers a solution for two open problems in the domain of paraconsistency, in particular connected to algebraization of LFIs, by obtaining several LFIs weaker than C1, each of one is algebraizable in the standard Lindenbaum-Tarski's sense by a suitable variety of Boolean algebras extended with operators. This means that such LFIs satisfy the replacement property. The weakest LFI satisfying replacement presented here is called RmbC, which is obtained from the basic LFI called mbC. Some axiomatic extensions of RmbC are also studied, and in addition a neighborhood semantics is defined for such systems. It is shown that RmbC can be defined within the minimal bimodal non-normal logic E⊕E defined by the fusion of the non-normal modal logic E with itself. Finally, the framework is extended to first-order languages. RQmbC, the quantified extension of RmbC, is shown to be sound and complete w.r.t. BALFI semantics. 1 1 Introduction: The quest for the algebraic counterpart of paraconsistency One of the most expected properties of a logical system is that it can be algebraizable, in the sense that an algebraic counterpart of the deductive machinery could be found. When this happens, a lot of logical problems can be faithfully and conservatively translated into some given algebra, and then algebraic tools can be used to tackle them. This happens so naturally with the brotherhood between classical logic and Boolean algebra, that a similar relationship is expected to hold for non-standard logics as well. And indeed it holds for some, but not for all logics. In any case, the task of finding such an algebraic counterpart is far from trivial. The intuitive idea behind the search for algebraization for a given logic system, generalizing the pioneering proposal of Lindenbaum and Tarski, usually starts by trying to find a congruence on the set of formulas that could be used to produce a quotient algebra, defined over the algebra of formulas of the logic. Finding such an algebraization for the logics of the hierarchy Cn of da Costa, introduced in [26], constitutes a paradigmatically difficult case. One of the favorite methods to set up congruences is to check the validity of a fundamental property called replacement or (IpE) (acronym for intersubstitutivity by provable equivalents, intuitively clear, and to be formally defined in Section 2. A logic enjoying replacement is usually called self-extensional. It is known since some time that (IpE) does not hold for C1, the first logic of da Costa's family. A proof can be found in [21] (Corollary 3.65); as a consequence, a direct LindenbaumTarski algebraization for this logic is not possible. This closes the way to the other, weaker calculi of the hiearchy Cn, since when one logic is algebraizable, so are its extensions. But there are other possibilities for algebraization, and the search continued until a proof was presented by Mortensen in 1980 [34], establishing that no non-trivial quotient algebra is definable for C1, or for any logic weaker than C1. In 1991, an even more negative result, found by Lewin, Mikenberg, Schwarze (see [31]) shows that C1 is not even algebraizable in the more general sense of Blok-Pigozzi (see [9]). This result was generalized in [21, Theorem 3.83] to Cila, the presentation of C1 in the language of the Logics of Formal Inconsistency (LFIs) featuring a (primitive) consistency conective ◦. Since any deductive extension of an algebraizable logic (in the same language) is also algebraizable, we obtain as a consequence that no such algebraization is possible for any other of the LFIs weaker than Cila studied in [21, 17, 14], like mbC, mbCciw, bC and Ci. The same reasoning applies to every calculus Cn in the infinite da Costa's hierarchy, given that they are weaker than C1. Some extensions of C1 having non-trivial quotient algebras have been proposed in the literature. In [35], for instance, Mortensen has proposed an infinite number of intermediate logics between C1 and classical logic called Cn/(n+1), for n ≥ 1. Such logics were shown to enjoy non-trivial congruences defined by finite sets of equations for each n ≥ 1, being thus algebraizable in the sense of Blok-Pigozzi (though not in the traditional sense of LindenbaumTarski). Some other types of algebraic counterparts have been investigated, for instance, in [19] and [39] an algebraic variety (da Costa algebras) for the logic C1 was defined, permitting a Stone-like representation theorem. In this way, every da Costa algebra is isomorphic to a paraconsistent algebra of sets, making C1 closer to traditional mathematical objects. 2 It can be proved, however, that for some subclasses of LFIs such intersubstitutivity results is unattainable, as shown in Theorem 3.51 of [21] with respect to the logic Ci, one of the central systems of the family of LFIs which is much weaker than Cila. Some interesting results concerning three-valued self-extensional paraconsistent logics were obtained in the literature, in connection with the limitative result [21, Theorem 3.51] mentioned above. In [3] it was shown that no three-valued paraconsistent logic having an implication can be self-extensional. On the other hand, in [2] it was shown that there is exactly one self-extensional three-valued paraconsistent logic defined in a signature having conjunction, disjunction and negation. For paraconsistent logics in general, it was shown in [6] that no paraconsistent negation ¬ satisfying the law of double negation and such that the schema ¬(φ ∧ ¬φ) is valid can satisfy (IpE). Nevertheless, there was still an open question: to obtain (IpE) for extensions of Ci by the addition of weaker forms of contraposition deduction rules, as discussed in Subsection 3.7 of [21]. The challenge was to find extensions of bC and Ci which would satisfy (IpE) and still keep their paraconsistent character. In this paper we meet this challenge. We define the logic RmbC, an extension by rules of mbC, and two suitable extensions of RmbC, the logics RbC and RCi (respectively, extensions of bC and Ci) that solve the open problem. Details are given in Example 3.9 of Section 3.1 A new kind of semantic structures, the Boolean algebras with LFI operators, or BALFIs, a generalization of BAOs (Boolean algebras with operators) is introduced in Section 2, and RmbC is proved to be sound and complete w.r.t. BALFIs. The paper also investigates some other directions. Section 4 studies the limits for replacement under the conditions for paraconsistency, and Section 5 proposes neigborhood semantics forRmbC as a special class of BALFIs defined on powerset Boolean algebras. Again, RmbC is proved to be sound and complete w.r.t. such version of neigborhood models. Moreover, in Section 6 it is proved that RmbC can be defined within the minimal bimodal non-normal modal logic. This neigborhood semantics is also proposed for axiomatic extensions of RmbC in Section 7. A special problem is studied in Section 8: the BALFI semantics for RmbC, as well as its neigborhood semantics defined in Section 5, are degree-preserving instead of truth-preserving (in the sense of [10]). This requires adapting the usual definition of derivation from premises in a Hilbert calculus (cf. Definition 2.6). But it is also possible to consider global (or truthpreserving) semantics, as it is usually done with algebraic semantics. This leads us to the logic RmbC∗, which is defined by the same Hilbert calculus than the one for RmbC, but where derivations from premises are defined as in the usual Hilbert calculi. Section 9 is dedicated to extending RmbC to first-order languages, defining the logic RQmbC, which is proved, in Section 10 and Section 11, to be complete w.r.t. BALFI semantics. The proof is an adaptation to the completeness proof for QmbC w.r.t. swap structures semantics given in [24], and since BALFIs are ordinary algebras, the new completeness proof offers a great simplification when compared to previous completeness results based on non-deterministic swap structures. 1To generate heuristics and suitable models, as well as to block dead-ends by finding counter-models, we count with the help of the proof assistant Isabelle/HOL. 3 2 The logic RmbC The class of paraconsistent logics known as Logics of Formal Inconsistency (LFIs, for short) was introduced by W. Carnielli and J. Marcos in [21]. In their simplest form, they have a non-explosive negation ¬, as well as a (primitive or derived) consistency connective ◦ which allows to recover the Law of Explosion in a controlled way. Definition 2.1 Let L = 〈Θ,⊢〉 be a Tarskian, finitary and structural logic defined over a propositional signature Θ, which contains a negation ¬, and let ◦ be a (primitive or defined) unary connective. Then, L is said to be a Logic of Formal Inconsistency with respect to ¬ and ◦ if the following holds: (i) φ,¬φ 0 ψ for some φ and ψ; (ii) there are two formulas α and β such that (ii.a) ◦α, α 0 β; (ii.b) ◦α,¬α 0 β; (iii) ◦φ, φ,¬φ ⊢ ψ for every φ and ψ. Condition (ii) of the definition of LFIs is required in order to satisfy condition (iii) in a non-trivial way. The hierarchy of LFIs studied in [17] and [14] starts from a logic called mbC, which extends positive classical logic CPL+ by adding a negation ¬ and a unary consistency operator ◦ satisfying minimal requirements in order to define an LFI. Definition 2.2 From now on, the following signatures will be considered: Σ+ = {∧,∨,→}; ΣBA = {∧,∨,→, 0, 1}; Σ = {∧,∨,→,¬, ◦}; ΣC = {∧,∨,→,¬}; ΣC0 = {∧,∨,→,¬, 0}; ΣCe = {∧,∨,→,¬, 0, 1}; Σe = {∧,∨,→,¬, ◦, 0, 1}; Σm = {∧,∨,→,∼,,♦}; and Σbm = {∧,∨,→,∼,1,♦1,2,♦2}. If Θ is a propositional signature, then For(Θ) will denote the (absolutely free) algebra of formulas over Θ generated by a given denumerable set V = {pn : n ∈ N} of propositional variables. 4 Definition 2.3 (Classical Positive Logic) The classical positive logic CPL+ is defined over the language For(Σ+) by the following Hilbert calculus: Axiom schemas: α → ( β → α ) (Ax1)( α→ ( β → γ )) → (( α → β ) → ( α→ γ )) (Ax2) α → ( β → ( α ∧ β )) (Ax3) ( α ∧ β ) → α (Ax4)( α ∧ β ) → β (Ax5) α→ ( α ∨ β ) (Ax6) β → ( α ∨ β ) (Ax7)( α→ γ ) → ( (β → γ) → ( (α ∨ β) → γ )) (Ax8) ( α → β ) ∨ α (Ax9) Inference rule: α α→ β β (MP) Definition 2.4 The logic mbC, defined over signature Σ, is obtained from CPL+ by adding the following axiom schemas: α ∨ ¬α (Ax10) ◦α→ ( α→ ( ¬α → β )) (bc1) The logic mbC is an LFI. Indeed, it is the minimal LFI extending CPL+. Consider the Replacement property, namely: If α↔ β is a theorem then γ[p/α] ↔ γ[p/β] is a theorem, for every formula γ(p) (as usual, α↔ β is an abbreviation of the formula (α→ β)∧ (β → α), and γ[p/α] denotes the formula obtained from γ by replacing every occurrence of the variable p by the formula α). It is well known that mbC does not satisfy replacement in general. However, it is easy to see that replacement holds in mbC for every formula γ(p) over the signature Σ+ of CPL +. We introduce now the logic RmbC which extends mbC by adding replacement for every formula over Σ. From the previous observation, it is enough to add replacement for ¬ and ◦ as new inference rules. Namely: if α ↔ β is a theorem then ¬α↔ ¬β (is a theorem), and if α↔ β is a theorem then ◦α↔ ◦β (is a theorem). Observe, however, that replacement is in fact a metaproperty (since it states that some formula is a theorem from previous formulas which are assumed to be theorems). It is clear that the two inference rules proposed above for inducing replacement are global instead of local (see Section 8 below): in order to apply each rule, the corresponding premise must be a theorem. This is an analogous situation to the Necessitation rule in modal logics. Assuming inference rules of this kind requires changing the definition of derivation from premises in the resulting Hilbert calculus, as we shall see below. 5 Definition 2.5 The logic RmbC, defined over signature Σ, is obtained from mbC by adding the following inference rules: α↔ β ¬α ↔ ¬β (R¬) α↔ β ◦α↔ ◦β (R◦) Definition 2.6 (Derivations in RmbC) (1) A derivation of a formula φ in RmbC is a finite sequence of formulas φ1 . . . φn such that φn is φ and, for every 1 ≤ i ≤ n, either φi is an instance of an axiom of RmbC, or φi is the consequence of some inference rule of RmbC whose premises appear in the sequence φ1 . . . φi−1. (2) We say that a formula φ is derivable in RmbC, or that φ is a theorem of RmbC, denoted by ⊢RmbC φ, if there exists a derivation of φ in RmbC. (3) Let Γ∪{φ} be a set of formulas over Σ. We say that φ is derivable in RmbC from Γ, and we write Γ ⊢RmbC φ, if either φ is derivable in RmbC, or there exists a finite, non-empty subset {γ1, . . . , γn} of Γ such that the formula (γ1 ∧ (γ2 ∧ (. . . ∧ (γn−1 ∧ γn) . . .))) → φ is derivable in RmbC. Remarks 2.7 (1) From the previous definition, it follows that ∅ ⊢RmbC φ iff ⊢RmbC φ. (2) Recall that a consequence relation ⊢ is said to be Tarskian and finitary if it satisfies the following properties: (i) Γ ⊢ α whenever α ∈ Γ; (ii) if Γ ⊢ α and Γ ⊆ ∆ then ∆ ⊢ α; (iii) if Γ ⊢ ∆ and ∆ ⊢ α then Γ ⊢ α, where Γ ⊢ ∆ means that Γ ⊢ δ for every δ ∈ ∆; and (iv) Γ ⊢ α implies that Γ0 ⊢ α for some finite Γ0 contained in Γ. It can be proven that the consequence relation ⊢RmbC given in Definition 2.6(2) is Tarskian and finitary, by using a general result stated by Wójcicki in [40]. Specifically, in Section 2.10 of that book it was studied the question of characterizing a Tarskian consequence relation ⊢ in terms of theoremhood, provided that the language contains an implication ⇒ and a conjunction &. Namely, the problem is to find necessary and sufficient conditions in order to have that γ1, . . . , γn ⊢ φ iff ⊢ (γ1& (γ2& (. . . & (γn−1& γn) . . .))) ⇒ φ and still having that ⊢ is Tarskian and finitary.2 Thus, in item (ii) of Theorem 2.10.2 in [40] certain requirements were found for ⇒ and & which are necessary and sufficient to guarantee that a consequence relation defined as in Definition 2.6 is Tarskian and finitary. It is easy to prove, by using the properties of CPL+, that → and ∧ satisfy such requirements in RmbC. From this, it follows that RmbC is indeed a Tarskian and finitary logic. By the properties of ∧ and → inherited from CPL+, and by the notion of derivation in RmbC, it is easy to see that the Deduction Metatheorem holds in RmbC:3 Theorem 2.8 (Deduction Metatheorem for RmbC) Γ, φ ⊢RmbC ψ if and only if Γ ⊢RmbC φ→ ψ. 2The problem was originally presented in [40] in a more general way. We are presenting here a particular case of that problem, which is enough to our purposes. Moreover, in [40] the problem was analyzed in terms of Tarskian consequence operators instead of Tarskian consequence relations, but both formalisms are equivalent in this context. 3Of course the satisfaction of the Deduction Theorem is what lies behind the problem studied in [40] mentioned in Remark 2.7(2). 6 The semantics for RmbC will be given by means of a suitable class of Boolean algebras with additional operators.4 Because of the definition of deductions in RmbC discussed above, the semantic consequence relation will be degree preserving instead of truth preserving (see [10]). In modal terms, the semantics will be local instead of global. We will return to this point in Section 8. Definition 2.9 (BALFIs) A Boolean algebra with LFI operators (BALFI, for short) is an algebra B = 〈A,∧,∨,→,¬, ◦, 0, 1〉 over Σe such that its reduct A = 〈A,∧,∨,→, 0, 1〉 to ΣBA is a Boolean algebra and the unary operators ¬ and ◦ satisfy: a∨¬a = 1 and a∧¬a∧◦a = 0, for every a ∈ A. The variety of BALFIs will be denoted by BI. Definition 2.10 (Degree-preserving BALFI semantics) (1) A valuation over a BALFI B is a homomorphism v : For(Σ) → B. (2) Let φ be a formula in For(Θ). We say that φ is valid in BI, denoted by |=BI φ, if, for every BALFI B and every valuation v over it, v(φ) = 1. (3) Let Γ∪{φ} be a set of formulas in For(Θ). We say that φ is a local (or degree-preserving) consequence of Γ in BI, denoted by Γ |=BI φ, if either φ is valid in BI, or there exists a finite, non-empty subset {γ1, . . . , γn} of Γ such that, for every BALFI B and every valuation v over it, ∧n i=1 v(γi) ≤ v(φ). Remark 2.11 Note that Γ |=BI φ iff either φ is valid in BI, or there exists a finite, nonempty subset {γ1, . . . , γn} of Γ such that (γ1∧ (γ2∧ (. . .∧ (γn−1∧γn) . . .))) → φ is valid. This follows easily from the definitions, and from the fact that a ≤ b iff a→ b = 1 in any Boolean algebra A. Theorem 2.12 (Soundness of RmbC w.r.t. BI) Let Γ ∪ {φ} ⊆ For(Θ). Then: Γ ⊢RmbC φ implies that Γ |=BI φ. Proof. Let φ be a an instance of an axiom of RmbC. It is immediate to see that, for every B and every valuation v on it, v(φ) = 1. Now, let α, β ∈ For(Σ). If v(α → β) = 1 and v(α) = 1 then, since v(α → β) = v(α) → v(β), it follows that v(β) = 1. On the other hand, if v(α ↔ β) = 1 then v(α) = v(β) and so v(#α) = #v(α) = #v(β) = v(#β), hence it follows that v(#α ↔ #β) = 1 for # ∈ {¬, ◦}. From this, by induction on the length of a derivation of φ in RmbC, it can be easily proven that φ is valid in BI whenever φ is derivable in RmbC. Now, suppose that Γ ⊢RmbC φ. If ⊢RmbC φ then, by the observation above, φ is valid in BI and so Γ |=BI φ. On the other hand, if there exists a finite, non-empty subset {γ1, . . . , γn} of Γ such that ⊢RmbC (γ1 ∧ (γ2 ∧ (. . .∧ (γn−1 ∧ γn) . . .))) → φ then, once again by the observation above, |=BI (γ1∧ (γ2∧ (. . .∧ (γn−1∧γn) . . .))) → φ. This shows that Γ |=BI φ, by Remark 2.11. ✷ Theorem 2.13 (Completeness of RmbC w.r.t. BI) Let Γ ∪ {φ} ⊆ For(Θ). Then: Γ |=BI φ implies that Γ ⊢RmbC φ. 4It is worth noting that these operators not necessarily commute with joins. Thus, the algebras are not necessarily coincident with the so-called Boolean algebras with operators (BAOs) used as semantics for modal logics (see, for instance, [30]). 7 Proof. Define the following relation on For(Σ): α ≡ β iff ⊢RmbC α ↔ β. It is clearly an equivalence relation, by the properties of CPL+. Let Acan def = For(Σ)/≡ be the quotient set, and define over Acan the following operations: [α] # [β] def = [α#β], for # ∈ {∧,∨,→}, where [α] denotes the equivalence class of α w.r.t. ≡. Let 0 def = [α ∧ ¬α ∧ ◦α] and 1 def = [α ∨ ¬α]. These operations and constants are clearly well-defined, and so they induce a structure of Boolean algebra over the set Acan, which will be denoted by Acan. Let Bcan be its expansion to Σe by defining #[α] def = [#α], for # ∈ {¬, ◦}. These operations are well-defined, and it is immediate to see that Bcan is a BALFI. Let vcan : For(Σ) → Bcan given by vcan(α) = [α]. Clearly vcan is a valuation over Bcan such that vcan(α) = 1 iff ⊢RmbC α. Now, suppose that Γ |=BI φ, and recall Remark 2.11. If |=BI φ then, in particular, vcan(φ) = 1 and so ⊢RmbC φ. From this, Γ ⊢RmbC φ. On the other hand, if there exists a finite, non-empty subset {γ1, . . . , γn} of Γ such that |=BI (γ1∧(γ2∧(. . .∧(γn−1∧γn) . . .))) → φ then, in particular, vcan((γ1 ∧ (γ2 ∧ (. . . ∧ (γn−1 ∧ γn) . . .))) → φ) = 1. This means that ⊢RmbC (γ1 ∧ (γ2 ∧ (. . . ∧ (γn−1 ∧ γn) . . .))) → φ and so Γ ⊢RmbC φ. ✷ Definition 2.14 The pair 〈Bcan, vcan〉 defined in the proof of Theorem 2.13 is called the canonical model of RmbC. Example 2.15 (BALFIs over ℘({w1, w2})) Let A4 = ℘({w1, w2}) = {0, a, b, 1} be the powerset of W2 = {w1, w2} such that 0 = ∅, a = {w1}, b = {w2} and 1 = {w1, w2}. Then, the BALFIs defined by expanding the Boolean algebra A4 are the following (below, | separates the possible options for the values of ¬z and ◦z for every value of z, while x stands for any element of A4): z ¬z ◦z 1 0 | a | b | 1 x | (0 or b) | (0 or a) | 0 a b | 1 x | (0 or b) b a | 1 x | (0 or a) 0 1 x On each row, each choice in the ith position of the sequence of options in the column for ¬z forces a choice in the ith position of the sequence of options in the column for ◦z. For instance, if in the current BALFI we choose ¬1 = b then there are two possibilities for the value of ◦1 in that BALFI: either ◦1 = 0 or ◦1 = a. On the other hand, by choosing that ¬a = 1 it forces that either ◦a = 0 or ◦a = b. Otherwise, if ¬a = b then ◦a can be arbitrarily chosen. Remark 2.16 Observe that the rules (R¬) and (R◦) do not ensure that ⊢RmbC (α↔ β) → (¬α↔ ¬β) and ⊢RmbC (α↔ β) → (◦α↔ ◦β) in general. Consider, for instance α = p and β = q where p and q are two different propositional variables, and take the following BALFI B defined over the Boolean algebra ℘({w1, w2}), according to Example 2.15: z ¬z ◦z 1 1 0 a b a b 1 a 0 1 b 8 Now, consider a valuation v over B such that v(p) = a and v(q) = 1. Hence v(¬p) = b, v(¬q) = 1, v(◦p) = a and v(◦q) = 0. From this v(p ↔ q) = a and v(¬p ↔ ¬q) = v(◦p ↔ ◦q) = b. Therefore v((p ↔ q) → (¬p ↔ ¬q)) = v((p↔ q) → (◦p ↔ ◦q)) = b. That is, none of the last two formulas is valid in RmbC. Of course both formulas hold if ⊢RmbC (α↔ β), by (R¬) and (R◦). Clearly RmbC is an LFI: in the BALFI B we just defined above, the given valuation v shows that q,¬q 0RmbC p. Now, consider the following BALFI B ′ defined over ℘({w1, w2}), using again Example 2.15: z ¬z ◦z 1 0 1 a 1 0 b 1 0 0 1 1 Take a valuation v′ over B′ such that v′(p) = 1 and v′(q) = a. This shows that p, ◦p 0RmbC q. Now, a valuation v′′ over B′ such that v′′(p) = 0 and v′′(q) = b shows that ¬p, ◦p 0RmbC q. In addition, a valuation v′′′ over B′ such that v′′′(p) = a and v′′′(q) = b shows that p,¬p 0RmbC q. On the other hand, by Definition 2.9 it is the case that α,¬α, ◦α ⊢RmbC β for every formulas α and β. 3 Adding replacement to extensions of mbC: A solution to an open problem In [21], the first study on LFIs, the replacement property was analyzed under the name (IpE), presented in the following (equivalent) way: (IpE) if αi ⊣⊢ βi (for 1 ≤ i ≤ n) then φ(α1, . . . , αn) ⊣⊢ φ(β1, . . . , βn) for every formulas αi, βi, φ. In that article, an important question was posed: to find extensions of bC and Ci (two axiomatic extensions of mbC to be analyzed below) which satisfy (IpE) still being paraconsistent.5 In this section, we will show a solution to that open problem, obtained by extending axiomatically RmbC. In what follows, some LFIs which are axiomatic extensions of mbC (bC and Ci, among others) will be considered, and the methodology adopted for RmbC to such extensions will be adapted in a suitable way. 5In [21], page 41, we can read: "The question then would be if (IpE) could be obtained for real LFIs". On page 54, after observing that in extensions of Ci it is enough ensuring (IpE) for negation, since it implies (IpE) for ◦, it is said that "We suspect that this can be done, but we shall leave it as an open problem at this point". Finally, they observe on page 55, footnote 17 that certain 8-valued matrices presented by Urbas satisfy (IpE) for an extension of bC. However, this logic is not paraconsistent. After this, they claim that "the question is still left open as to whether there are paraconsistent such extensions of bC!". 9 Definition 3.1 (Some extensions of mbC) Consider the following axioms presented in [21] and [14]:6 ◦α ∨ (α ∧ ¬α) (ciw) ¬◦α → (α ∧ ¬α) (ci) ¬(α ∧ ¬α) → ◦α (cl) ¬¬α → α (cf) α→ ¬¬α (ce) (◦α ∧ ◦β) → ◦(α ∧ β) (ca∧) (◦α ∧ ◦β) → ◦(α ∨ β) (ca∨) (◦α ∧ ◦β) → ◦(α→ β) (ca→) Definition 3.2 Let B = 〈A,∧,∨,→,¬, ◦, 0, 1〉 be a BALFI, and let φ be a formula over Σ. We say that B is a model of φ (considered as an axiom schema), denoted by B φ, if v(σ(φ)) = 1 for every substitution for variables σ : V → For(Σ) and every valuation v over B. The proof of the following result is immediate from the definitions: Proposition 3.3 Let B = 〈A,∧,∨,→,¬, ◦, 0, 1〉 be a BALFI. Then: (1) B is a model of (ciw) iff B satisfies the equation ◦a = ∼(a ∧ ¬a) for every a ∈ A; (2) B is a model of (ci) iff B satisfies the equation ¬◦a = a ∧ ¬a for every a ∈ A; (3) B is a model of (cl) iff B satisfies the equation ◦a = ¬(a ∧ ¬a) for every a ∈ A; (4) B is a model of (cf) iff B satisfies the equation a ∧ ¬¬a = ¬¬a for every a ∈ A; (5) B is a model of (ce) iff B satisfies the equation a ∧ ¬¬a = a for every a ∈ A; (6) B is a model of (ca#) iff B satisfies the equation (◦a ∧ ◦b) ∧ ◦(a#b) = ◦a ∧ ◦b for every a, b ∈ A, for each # ∈ {∧,∨,→}. Let Ax be a set formed by one or more of the axiom schemas introduced in Definition 3.1, and let mbC(Ax) be the logic defined by the Hilbert calculus obtained from mbC by adding the set Ax of axiom schemas. Let BI(Ax) be the class of BALFIs which are models of every axiom in Ax. Clearly, BI(Ax) is a variety of algebras. Finally, let RmbC(Ax) be the logic obtained from RmbC by adding the set Ax of axiom schemas. It is simple to adapt the proofs of Theorems 2.12 and 2.13 (in particular, by defining for each logic the corresponding canonical model, as in Definition 2.14) in order to obtain the following: Theorem 3.4 (Soundness and completeness of RmbC(Ax) w.r.t. BI(Ax)) Let Γ ∪ {φ} ⊆ For(Σ). Then: Γ ⊢RmbC(Ax) φ if and only if Γ |=BI(Ax) φ. From this important result, some properties of the calculi RmbC(Ax) can be easily proven by algebraic methods, that is, by means of BALFIs. For instance: 6Axiom (ciw) was introduced by Avron in [1] by means of two axioms, (k1): ◦α∨α and (k2): ◦α∨¬α. Strictly speaking, (k1) and (k2) were presented as rules in a standard Gentzen calculus. 10 Proposition 3.5 BI({ci, cf}) = BI({cl, cf}) = BI({ci, cl, cf}). Hence, the logics RmbC({ci, cf}), RmbC({cl, cf}) and RmbC({ci, cl, cf}) coincide. Proof. (1) Since ⊢mbC (α ∧ ¬α) → ¬◦α and ⊢mbC ◦α → ¬(α ∧ ¬α) then, for every BALFI B and every a ∈ A, (a ∧ ¬a) ≤ ¬◦a and ◦a ≤ ¬(a ∧ ¬a). Let B ∈ BI({ci, cf}), and let a ∈ A. Then a ∧ ¬a = ¬◦a and so ¬(a ∧ ¬a) = ¬¬◦a ≤ ◦a. Therefore B ∈ BI({cl, cf}). Conversely, suppose that B ∈ BI({cl, cf}) and let a ∈ A. Since ◦a = ¬(a ∧ ¬a) then ¬◦a = ¬¬(a ∧ ¬a) ≤ (a ∧ ¬a). From this, B ∈ BI({ci, cf}). This shows the first part of the Proposition. The second part follows from Theorem 3.4. ✷ Example 3.6 (BALFIs for RmbCciw) The logic mbC(ciw) was considered in [14] under the name mbCciw. This logic was introduced in [1] under the name B[{(k1), (k2)}], presented by means of a standard Gentzen calculus such that B is a Gentzen calculus for mbC. The logic mbCciw is the least extension of mbC in which the consistency connective can be defined in terms of the other connectives, namely: ◦α is equivalent to ∼(α ∧ ¬α), where ∼ denotes the classical negation definable in mbC as ∼α = α→ ⊥. Here, ⊥ denotes any formula of the form β ∧ ¬β ∧ ◦β.7 Let RmbCciw be the logic RmbC(ciw). Because of the satisfaction of the replacement property, and given that the consistency connective can be defined in terms of the other connectives, the connective ◦ can be eliminated from the signature, and so we consider the logic RmbCciw defined over the signature ΣC0 (recall Definition 2.2), obtained from CPL+ by adding (Ax10), (R¬), and axiom schema (Bot): 0 → α. In such presentation of RmbCciw, the strong negation is defined by the formula ∼α = α→ 0. The algebraic models for this presentation of RmbCciw are given by BALFIs B = 〈A,∧,∨,→,¬, 0, 1〉 over ΣCe such that its reduct A = 〈A,∧,∨,→, 0, 1〉 to ΣBA is a Boolean algebra and the unary operator ¬ satisfies a∨¬a = 1 for every a ∈ A. On the other hand, the expression ◦a is an abbreviation for ∼(a ∧ ¬a) in such BALFIs. It is also interesting to observe that ◦ satisfies a sort of necessitation rule in certain extensions of RmbC: Proposition 3.7 Consider the Necessitation rule for ◦: α ◦α (Nec◦) Then, (Nec◦) is an admissible rule in RmbC({cl, ce}).8 Proof. Assume that ⊢RmbC({cl,ce}) α. By the rules of CPL + it follows that ⊢RmbC({cl,ce}) β ↔ (α ∧ β) for every formula β. In particular, ⊢RmbC({cl,ce}) ¬α ↔ (α ∧ ¬α) and so, by (R¬), ⊢RmbC({cl,ce}) ¬¬α ↔ ¬(α ∧ ¬α). On the other hand, from ⊢RmbC({cl,ce}) α it follows 7Rigorously speaking, ◦ is not defined in terms of the other connectives, since ◦ is essential on order to define ⊥. So, the right signature for mbCciw and its extensions is ΣC0 . 8Recall that a structural inference rule is admissible in a logic L if the following holds: whenever the premises of an instance of the rule are theorems of L, then the conclusion of the same instance of the rule is a theorem of L. 11 that ⊢RmbC({cl,ce}) ¬¬α, by (ce) and (MP). Then ⊢RmbC({cl,ce}) ¬(α ∧ ¬α). By (cl) and (MP) we conclude that ⊢RmbC({cl,ce}) ◦α. ✷ Now, we can provide a solution to the first open problem posed in [21]: Example 3.8 (A paraconsistent extension of bC with replacement) Consider the logic bC introduced in [21]. By using the notation proposed above, bC corresponds to mbC(cf).9 Then RbC (that is, RmbC(cf)) is an extension of bC which satisfies replacement while it is still paraconsistent. Moreover, RbC is an LFI. These facts can be easily proven by using the BALFI B′ considered in Remark 2.16. In fact, it is immediate to see that B′ is a model of (cf). It is worth noting that B′ is not a model of (ciw): 0 = ◦a 6= ∼(a ∧ ¬a) = ∼a = b. Therefore, B′ is neither a model of (ci) nor of (cl), given that any of these axioms implies (ciw). We can now offer a solution to the second open problem posed in [21]: Example 3.9 (A paraconsistent extension of Ci with replacement) Now, consider the logic Ci introduced in [21], which corresponds to mbC({cf, ci}), and let RCi=RmbC({cf, ci}). By Proposition 3.5, RCi also derives the schema (cl). It can be proven that RCi is an extension of Ci which satisfies replacement while it is still paraconsistent. In order to prove this, consider the following BALFI B′′ defined over the Boolean algebra A16 = ℘({W4}), the powerset of W4 = {w1, w2, w3, w4} (note that 0 = ∅ and 1 =W4): z ¬z ◦z {w1, w2} {w1, w3, w4} {w2, w3, w4} {w3, w4} {w1, w2, w3} {w1, w2, w4} X W4 \X W4 where X is different to {w1, w2} and {w3, w4}. It is immediate to see that B′′ is a BALFI for RCi. Hence, using this model it follows easily that RCi is a paraconsistent extension of Ci which satisfies (IpE) and (cl). Another paraconsistent model for RCi defined over A16 is the following: z ¬z ◦z {w1, w2} {w2, w3, w4} {w1, w3, w4} {w1, w3} {w2, w3, w4} {w1, w2, w4} {w1, w4} {w2, w3, w4} {w1, w2, w3} {w2, w3} {w1, w3, w4} {w1, w2, w4} {w2, w4} {w1, w3, w4} {w1, w2, w3} {w3, w4} {w1, w2, w4} {w1, w2, w3} X W4 \X W4 9We will write mbC(φ), RmbC(φ) and BI(φ) instead of mbC({φ}), RmbC({φ}) and BI({φ}), respectively. 12 where the cardinal of X is different to 2.10 Example 3.10 We can offer now a model of RmbC(cl) which does not satisfy axiom (cf). Thus, consider the following BALFI B′′′ defined over the Boolean algebra A4 = ℘({w1, w2}) = {0, a, b, 1} according to Example 2.15: z ¬z ◦z 1 a b a b 1 b a 1 0 1 1 Observe that B′′′ cl. However, B′′′ is not a model of (cf): ¬¬0 = a 6≤ 0. 4 Limits for replacement plus paraconsistency In [21, Theorem 3.51] some sufficient conditions were given to show that certain extensions of bC and Ci cannot satisfy replacement while being still paraconsistent. This result shows that there are limits, much before reaching classical logic CPL, for extending RmbC while preserving paraconsistency. This result will be applied now in order to give two important examples of LFIs which cannot be extended with replacement to the price of losing paraconsistency. The first example to be given is, in fact, a family of 8,192 examples: Example 4.1 (Three-valued LFIs) Recall the family of 8Kb three-valued LFIs introduced by Marcos in an unpublished draft, and discussed in [21, Section 3.11] and in [17, Section 5.3]. As it was observed in these references, the schema ¬(α∧¬α) is valid in all of these logics. In addition, all these logics are models of axioms (ci) and (cf) (see, for instance, [17, Theorem 130]). But in [21, Theorem 3.51(ii)] it was proved that (IpE) cannot hold in any paraconsistent extension of Ci in which the schema ¬(α ∧ ¬α) is valid. As a consequence of this, the inference rules (R¬) and (R◦) cannot be added to any of them to the price of losing paraconsistency. Indeed, if L is any of such three-valued logics, the corresponding logic RL obtained by adding both rules will derive the axiom schema ◦α (the proof of this fact can be easily adapted from the one for Theorem 3.51(ii) presented in [21]). But then, the negation ¬ is explosive in RL, by (bc1) and (MP). This shows that these three-valued LFIs, including the well-known da Costa and D'Ottaviano's logic J3 (and so all of its equivalent presentations, such as LFI1, CLuN or LPT0), as well as Sette's logic P1, if extended by the inference rules proposed here, are no longer paraconsistent. Of course this result is related to the one obtained in [3], which states that for no three-valued paraconsistent logic with implication the replacement property can hold. 10It is worth noting that with the help of the model finder Nitpick, which is part of the automated tools integrated into Isabelle/HOL [36], we carried out many of the experiments leading to the generation of the two models presented here. 13 The second example deals with the well-known logic C1, introduced by da Costa in 1963. Example 4.2 (da Costa's logic C1) In [26] da Costa introduced his famous hierarchy of paraconsistent systems Cn (for n ≥ 1), the first systematic study on paraconsistency introduced in the literature. As discussed above, da Costa's approach was generalized through the notion of LFIs. The first and stronger system in the hierarchy is C1, which is equivalent (up to language) with Cila. The logic Cila corresponds, with the notation introduced above, to mbC({ci, cl, cf , ca∧, ca∨, ca→}). If we consider now RmbC({ci, cl, cf , ca∧, ca∨, ca→}), which will be called RCila, then this logic derives (ciw). Indeed, as shown in [14, Proposition 3.1.10], axiom (ciw) is derivable from mbC plus axiom (ci). This being so, by Example 3.6 and the fact that ⊥ def = (α ∧ ¬α) ∧ ¬(α∧¬α) is a bottom formula in Cila (hence in RCila) for any α (i.e., ⊥ implies any other formula), the connective ◦ could be eliminated from the signature of RCila, and so the logic RCila could be defined over the signature ΣC (recall Definition 2.2). In that case, RCila would coincide with RC1, the extension of C1 by adding the inference rule (R¬) (and where the notion of derivation is given as in Definition 2.6). The question is to find a model of RCila (or, equivalently, of RC1) which is still paraconsistent. In [21, Theorem 3.51(iv)] it was proved that (IpE) cannot hold in any paraconsistent extension of Ci in which the schema (dm): ¬(α ∧ β) → (¬α ∨ ¬β) is valid. On the other hand, in [14, Theorem 3.6.4] it was proved that the logic obtained from mbCciw by adding (ca∧) is equivalent to the logic obtained from mbCciw by adding the schema axiom (dm). Since RCila derives (ciw) and (ca∧), it also derives the schema (dm). Given that RCila is an extension of Ci which satisfies (IpE), it is not paraconsistent, by [21, Theorem 3.51(iv)]. 5 Neighborhood semantics for RmbC Despite being very useful for finding models and countermodels, as it was shown in the previous section, BALFI semantics does not seem to produce a decision procedure for LFIs with replacement. In this section we will introduce a particular case of BALFIs based on powerset Boolean algebras, which are more amenable to being generated by computational means. These structures are in fact equivalent to neighborhood frames for non-normal modal logics, as we shall see in Section 6. Moreover, we shall prove in that Section that, with this semantics, RmbC can be defined within the bimodal version of the minimal modal logic E (a.k.a. classical modal logic, see [22, Definition 8.1]). Definition 5.1 Let W be a non-empty set. A neighborhood frame for RmbC over W is a triple F = 〈W,S¬, S◦〉 such that S¬ : ℘(W ) → ℘(W ) and S◦ : ℘(W ) → ℘(W ) are functions. A neighborhood model for RmbC over F is a pair M = 〈F , d〉 such that F is a neighborhood frame for RmbC over W and d : V → ℘(W ) is a (valuation) function. Definition 5.2 Let M = 〈F , d〉 be a neighborhood model for RmbC over F = 〈W,S¬, S◦〉. It induces a denotation function [[*]]M : For(Σ) → ℘(W ) defined recursively as follows (by simplicity, we will write [[φ]] instead of [[φ]]M when M is clear from the context): [[p]] = d(p), if p ∈ V; 14 [[φ ∧ ψ]] = [[φ]] ∩ [[ψ]]; [[φ ∨ ψ]] = [[φ]] ∪ [[ψ]]; [[φ→ ψ]] = [[φ]] → [[ψ]] = (W \ [[φ]]) ∪ [[ψ]]; [[¬φ]] = (W \ [[φ]]) ∪ S¬([[φ]]); and [[◦φ]] = (W \ ([[φ]] ∩ [[¬φ]])) ∩ S◦([[φ]]) = (W \ ([[φ]] ∩ S¬([[φ]]))) ∩ S◦([[φ]]). Clearly [[φ]] ∪ [[¬φ]] = W , but [[φ]] ∩ [[¬φ]] is not necessarily empty. In addition, [[φ]] ∩ [[¬φ]] ∩ [[◦φ]] = ∅. Definition 5.3 Let M = 〈F , d〉 be a neighborhood model for RmbC. (1) We say that a formula φ is valid (or true) in M, denoted by M φ, if [[φ]] = W . (2) We say that a formula φ is valid w.r.t. neighborhood models, denoted by |=NM φ, if M φ for every neighborhood model M for RmbC. (3) The consequence relation |=NM induced by neighborhood models for RmbC is defined as follows: Γ |=NM φ if either φ is valid w.r.t. neighborhood models for RmbC, or there exists a finite, non-empty subset {γ1, . . . , γn} of Γ such that (γ1∧ (γ2∧ (. . .∧ (γn−1∧ γn) . . .))) → φ is valid w.r.t. neighborhood models for RmbC. Cleary, Γ |=NM φ if either φ is valid w.r.t. neighborhood models for RmbC, or there exists a finite, non-empty subset {γ1, . . . , γn} of Γ such that, for every neighborhood model M for RmbC, ⋂n i=1[[γi]] ⊆ [[φ]]. Proposition 5.4 Given a neighborhood frame F = 〈W,S¬, S◦〉 for RmbC let ¬, ◦ : ℘(W ) → ℘(W ) defined as follows: ¬(X) = (W \ X) ∪ S¬(X) and ◦(X) = (W \ (X ∩ S¬(X)) ∩ S◦(X). Then BF def = 〈℘(W ),∩,∪,→, ¬, ◦, ∅,W 〉 is a BALFI. Moreover, if M = 〈F , d〉 is a neighborhood model for RmbC over F = 〈W,S¬, S◦〉 then the denotation function [[*]]M is a valuation over BF . Proof. It is immediate from the definitions. ✷ Corollary 5.5 (Soundness of RmbC w.r.t. neighborhood models) If Γ ⊢RmbC φ then Γ |=NM φ. Proof. It follows from soundness of RmbC w.r.t. BALFI semantics (Theorem 2.12) and by Proposition 5.4. ✷ Proposition 5.4 suggests the following : Definition 5.6 Let F = 〈W,S¬, S◦〉 be a neighborhood frame for RmbC. A formula φ is valid in F if M φ for every neighborhood model M = 〈F , d〉 for RmbC over F . In order to prove completeness of RmbC w.r.t. neighborhood models, Stone's representation theorem for Boolean algebras will be used. This important theorem states that every Boolean algebra is isomorphic to a Boolean subalgebra of ℘(W ), for a suitable W . This means that, given a Boolean algebra A, there exists a set W and an injective homomorphism i : A → ℘(W ) of Boolean algebras. Note that i(a) = W if and only if a = 1. 15 Theorem 5.7 (Completeness of RmbC w.r.t. neighborhood models) If Γ |=NM φ then Γ ⊢RmbC φ. Proof. Let Acan be the Boolean algebra with domain Acan = For(Σ)/≡, as defined in the proof of Theorem 2.13, and let Bcan be the corresponding expansion to Σe. Let i : Acan → ℘(W ) be an injective homomorphism of Boolean algebras, according to Stone's theorem as discussed above. Consider the neighborhood frame Fcan = 〈W,S¬, S◦〉 for RmbC such that the functions S¬ and S◦ satisfy the following: S¬(i([α])) = i([¬α]), and S◦(i([α])) = i([◦α]), for every formula α (observe that these funcions are well-defined, since every connective in RmbC is congruential and i is injective). The values of these functions outside the image of i are arbitrary. For instance, we can define S¬(X) = S◦(X) = ∅ if X /∈ i[Acan]. Now, let Mcan = 〈Fcan, dcan〉 be the neighborhood model for RmbC such that dcan(p) def = i([p]), for every propositional variable p. Fact: [[α]] = i([α]), for every formula α. The proof of the Fact will be done by induction on the complexity of the formula α. By convenience, and as it is usually done (see, for instance, [14]), the complexity of ◦α is defined to be stricty greater than the complexity of ¬α. The case for α atomic or α = β#γ for # ∈ {∧,∨,→} is clear, by the very definitions and by induction hypothesis. Now, suppose that α = ¬β. By induction hypothesis, [[β]] = i([β]). Observe that ∼[β] ≤ [¬β] in Acan (where ∼ denotes the Boolean complement in Acan), hence W \ i([β]) = i(∼[β]) ⊆ i([¬β]). Thus, [[¬β]] = (W \ [[β]]) ∪ S¬([[β]]) = (W \ i([β])) ∪ S¬(i([β])) = (W \ i([β])) ∪ i([¬β]) = i([¬β]). Finally, let α = ◦β. Since [◦β] ≤ ∼([β] ∧ [¬β]) in Acan then i([◦β]) ⊆ W \ (i([β]) ∩ i([¬β])). Hence, by induction hypothesis, [[◦β]] = (W \ (i([β]) ∩ i([¬β]))) ∩ S◦(i([β]) = (W \ (i([β]) ∩ i([¬β]))) ∩ i([◦β]) = i([◦β]). This concludes the proof of the Fact. Because of the Fact, Mcan α iff i([α]) = W iff [α] = 1 iff ⊢RmbC α. Now, suppose that Γ |=NM φ. If |=NM φ then, in particular, Mcan φ and so ⊢RmbC φ. From this, Γ ⊢RmbC φ. On the other hand, suppose that there exists a finite, non-empty subset {γ1, . . . , γn} of Γ such that |=NM (γ1 ∧ (γ2 ∧ (. . . ∧ (γn−1 ∧ γn) . . .))) → φ. By reasoning as above, it follows that ⊢RmbC (γ1 ∧ (γ2 ∧ (. . . ∧ (γn−1 ∧ γn) . . .))) → φ and so Γ ⊢RmbC φ as well. ✷ 16 6 RmbC is definable within the minimal bimodal modal logic In this section it will be shown that RmbC is definable within the bimodal version of the minimal modal logic E, also called classical modal logic in [22, Definition 8.1]). In terms of combination of modal logics, this bimodal logic is equivalent to the fusion (or, equivalently, the constrained fibring by sharing the classical connectives) of E with itself.11 This means that the minimal non-normal modal logic with two independent modalities 1 and 2, which will be denoted by E⊕E, contains RmbC, the minimal self-extensional LFI. As we shall see, both modalities are required for defining the two non-classical conectives ¬ and ◦. Firstly, the definition of modal logic E will be briefly surveyed. Definition 6.1 ([22], Definition 7.1) A minimal model is a triple N = 〈W,N, d〉 such that W is a non-empty set and N : W → ℘(℘(W )) and d : V → ℘(W ) are functions. The class of minimal models will we denoted by CM. Recall the signatures Σm = {∧,∨,→,∼,,♦} and Σbm = {∧,∨,→,∼,1,♦1,2,♦2} introduced in Definition 2.2. The class of models CM induces a modal consequence relation defined as follows: Definition 6.2 ([22], Definition 7.2) Let N be a minimal model and w ∈ W . N is said to satisfy a formula φ ∈ For(Σm) in w, denoted by |=Nw φ, according to the following recursive definition (here [[φ]]N denotes the set {w ∈ W : |=Nw φ}, the denotation of φ in N ): 1. if p is a propositional variable then |=Nw p iff w ∈ d(p); 2. |=Nw ∼α iff 6|= N w α; 3. |=Nw α ∧ β iff |= N w α and |= N w β; 4. |=Nw α ∨ β iff |= N w α or |= N w β; 5. |=Nw α→ β iff 6|= N w α or |= N w β; 6. |=Nw α iff [[α]] N ∈ N(w); 7. |=Nw ♦α iff (W \ [[α]] N ) /∈ N(w). A formula φ is true in N if [[φ]]N = W , and it is valid w.r.t. CM, denoted by |=CM φ, if it is true in every minimal model. The degree-preserving consequence w.r.t. CM can be defined analogously to the one for neighborhood semantics for RmbC given in Definition 5.3. Namely, Γ |=CM φ if either |=CM φ, or there exists a finite, non-empty subset {γ1, . . . , γn} of Γ such that |=CM (γ1∧ (γ2∧ (. . .∧ (γn−1∧ γn) . . .))) → φ. The latter is equivalent to say that⋂n i=1[[γi]] N ⊆ [[φ]]N . 11For the basic notions of combining logics the reader can consult [12, 16]. 17 Definition 6.3 ([22], Definition 8.1) The minimal modal logic (or classical modal logic) E is defined by means of a Hilbert calculus over the signature Σm obtained by adding to the Hilbert calculus for CPL+ (recall Definition 2.3) the following axiom schemas and rules: α ∨ ∼α (PEM) α→ ( ∼α→ β ) (exp) ♦α↔ ∼∼α (AxMod) α↔ β α ↔ β (R) The notion of derivations in E is defined as for RmbC, recall Definition 2.6. Note that (PEM) and (exp), together with CPL+, guarantee that E is an expansion of propositional classical logic by adding the modalities  and ♦ which are interdefinable as usual, and such that both are congruential. That is, E satisfies replacement. Theorem 6.4 ([22], Section 9.2) The logic E is sound and complete w.r.t. the semantics in CM, namely: Γ ⊢E φ iff Γ |=CM φ. Definition 6.5 (Minimal bimodal logic) The minimal bimodal logic E⊕E is defined by means of a Hilbert calculus over signature Σbm obtained by adding to the Hilbert calculus for CPL+ the following axiom schemas and rules, for i = 1, 2: α ∨ ∼α (PEM) α→ ( ∼α→ β ) (exp) ♦iα↔ ∼i∼α (AxModi) α↔ β iα↔ iβ (Ri) Observe that E ⊕ E is obtained from E by 'duplicating' the modalities. There is no relationship between 1 and 2 and so ♦1 and ♦2 are also independent. The semantics ofE⊕E is given by the class C′M of structures of the formN = 〈W,N1, N2, d〉 such that W is a non-empty set and Ni : W → ℘(℘(W )) (for i = 1, 2) and d : V → ℘(W ) are functions. The denotation [[φ]]N of a formula φ ∈ For(Σbm) in N is defined by an obvious adaptation of Definition 6.2 to For(Σbm). By defining the consequence relations ⊢E⊕E and |=C ′ M in analogy to the ones for E, it is straightforward to adapt the proof of soundness and completeness of E to the bimodal case: Theorem 6.6 The logic E⊕ E is sound and complete w.r.t. the semantics in C′M, namely: Γ ⊢E⊕E φ iff Γ |=C ′ M φ. 18 From the point of view of of combining logics, E ⊕ E is the fusion (or, equivalently, the constrained fibring by sharing the classical connectives) of E with itself.12 Finally, it will be shown thatRmbC can be defined inside E⊕E by means of the following abbreviations: ¬φ def = φ→ 1φ and ◦φ def = ∼(φ ∧1φ) ∧2φ. In order to see this, observe that any function N : W → ℘(℘(W )) induces a unique function S : ℘(W ) → ℘(W ) given by S(X) = {w ∈ W : X ∈ N(w)}. Conversely, any function S : ℘(W ) → ℘(W ) induces a function N : W → ℘(℘(W )) given by N(w) = {X ⊆ W : w ∈ S(X)}. Both functions are inverses of each other. From this, a structure (or minimal model) N = 〈W,N1, N2, d〉 for E ⊕ E can be transformed into a neighborhood model M = 〈W,S¬, S◦, d〉 for RmbC such that S¬ and S◦ are obtained, respectively, from the functions N1 and N2 as indicated above. Observe that w ∈ [[1φ]] N iff |=Nw 1φ iff [[φ]] N ∈ N1(w) iff w ∈ S¬([[φ]] N ). That is, S¬([[φ]] N ) = [[1φ]] N . Analogously, S◦([[φ]] N ) = [[2φ]] N . From this, it is easy to prove by induction on the complexity of the formula φ ∈ For(Σ) that [[φ]]M = [[φt]]N , where φt is the formula over the signature Σbm obtained from φ by replacing any ocurrence of the connectives ¬ and ◦ by the corresponding abbreviations, as indicated above. Conversely, any neighborhood model M = 〈W,S¬, S◦, d〉 for RmbC gives origin to a unique minimal model N = 〈W,N1, N2, d〉 for E⊕E such that [[φ]]M = [[φt]]N for every formula φ ∈ For(Σ). That is, the class of minimal models for E⊕E coincides (up to presentation) with the class of neighborhood models for RmbC, and both classes validate the same formulas over the signature Σ of RmbC. From this, Corollary 5.5, Theorem 5.7 and Theorem 6.6 we show that RmbC is definable within E⊕ E: Theorem 6.7 The logic RmbC is definable within E⊕E, in the following sense: Γ ⊢RmbC φ iff Γt ⊢E⊕E φt for every Γ ∪ {φ} ⊆ For(Σ), where Γt = {ψt : ψ ∈ Γ}. The main result obtained in this section, namely Theorem 6.7, establishes an interesting relation between non-normal modal logics and paraconsistent logics. Connections between modalities and paraconsistency are well-known in the literature. In [7, 8], for instance, Béziau proposes to consider a paraconsistent negation defined in the modal system S5 as ¬φ def = ♦∼φ. This way of defining a paraconsistent negation inside a modal logic has been already regarded in 1987 in [27], when a Kripke-style semantics was proposed for Sette's threevalued paraconsistent logic P1 based on Kripke frames for the modal logic T. This result was improved in [20], by showing that P1 can be interpreted in T by means of Kripke frames having at most two worlds. Moreover, in 1982 Segerberg already suggested in [38, p. 128] the possibility of studying the (unexplored at that time) modal notion of 'φ is non-necesary', namely ∼φ (which is of course equivalent in most modal systems to ♦∼φ). Several authors have explored the possibility of defining such paraconsistent negation in other modal logics such as B [4], S4 [25] and even weaker modal systems [11]. In such context, Marcos proposes in [33], besides the paraconsistent negation defined as above, the definition of a consistency connective within a modal system by means of the formula ◦φ def = φ → φ (observe the 12See [12, 16]. 19 similarity with the definition of the paraconsistent negation within E ⊕ E). In that paper it is shown that any normal modal logic in which the schema φ → φ is not valid gives origin to an LFI in this way. Moreover, it is shown that it is also possible to start from a "modal LFI", over the signature Σ of LFIs, in which the paraconsistent negation and the consistency connective enjoy a Kripke-style semantics, defining the modal necessity operator by means of the formula φ def = ∼¬φ (where ∼ is the strong negation defined as in mbC, recall Example 3.6). This shows that 'reasonable' normal modal logics and LFIs are two faces of the same coin. Our Theorem 6.7 partially extends this relationship to the realm of non-normal modal logics. The result we have obtained is partial, in the sense that the minimum bimodal non-normal modal logics gives origin to RmbC, but the converse does not seem to be true. Namely, starting from RmbC it is not obvious that the modalities 1 and 2 could be defined by means of formulas in the signature Σ. This topic deserves further investigation. 7 Neighborhood models for axiomatic extensions of RmbC Recall the axioms considered in Definition 3.1. Because of the limit to paraconsistency imposed by RCila (recall Example 4.2), in this section Ax will denote a set formed by one or more of the axiom schemas introduced in Definition 3.1 with the exception of (ca#) for # ∈ {∧,∨,→}. Let NM(Ax) the class of neighborhood frames in which every schema in Ax is valid. Define the consequence relation |=NM(Ax) in the obvious way. By adapting the previous results it is easy to prove the following: Theorem 7.1 (Soundness and completeness of RmbC(Ax) w.r.t. NM(Ax)) Let Γ ∪ {φ} ⊆ For(Σ). Then: Γ ⊢RmbC(Ax) φ if and only if Γ |=NM(Ax) φ. The class of neighborhood frames which validates each of the axioms of Ax can be easily characterized: Proposition 7.2 Let F be a neighborhood frame for RmbC. Then: (1) (ciw) is valid in F iff W \ (X ∩ S¬(X)) ⊆ S◦(X), for every X ⊆W ; (2) (ci) is valid in F iff W \ (X ∩ S¬(X)) ⊆ S◦(X) \ S¬((W \ (X ∩ S¬(X))) ∩ S◦(X)), for every X ⊆W ; (3) (cl) is valid in F iff S¬(X ∩ S¬(X)) ⊆W \ (X ∩ S¬(X)) ⊆ S◦(X), for every X ⊆ W ; (4) (cf) is valid in F iff (X \ S¬(X)) ∪ S¬(X \ S¬(X)) ⊆ X, for every X ⊆ W ; (5) (ce) is valid in F iff X ⊆ (X \ S¬(X)) ∪ S¬(X \ S¬(X)), for every X ⊆W . Recall the minimal bimodal logic E⊕E studied in Section 6. If φ is a formula in For(Σbm) then E ⊕ E(φ) will denote the extension of E ⊕ E by adding φ as an axiom schema. Let C′M(φ) be the class of structures (i.e., minimal models) N for E⊕ E such that φ is valid in N (as an axiom schema). Theorem 6.6 can be extended to prove that the logic E⊕ E(φ) is sound and complete w.r.t. the semantics in C′M(φ). From this, and taking into account the 20 representability of RmbC within E⊕E (Theorem 6.7) and the equivalence between minimal models for E⊕E and neighborhood models for RmbC discussed right before Theorem 6.7, Proposition 7.2 can be recast as follows: Corollary 7.3 (1) RmbC(ciw) is definable in E⊕E(∼(φ ∧1φ) → 2φ); (2) RmbC(ci) is definable in E ⊕ E(∼(φ ∧ 1φ) → (2φ ∧ ∼1(∼(φ ∧1φ) ∧2φ))) or, equivalenty, in E⊕ E((2φ→ 1(∼(φ ∧1φ) ∧2φ)) → (φ ∧1φ)); (3) RmbC(cl) is definable in E⊕E((1(φ∧1φ) → ∼(φ∧1φ))∧ (∼(φ∧1φ) → 2φ)); (4) RmbC(cf) is definable in E⊕E(((φ ∧ ∼1φ) ∨1(φ ∧ ∼1φ)) → φ); (5) RmbC(ce) is definable in E⊕ E(φ→ ((φ ∧ ∼1φ) ∨1(φ ∧ ∼1φ))). 8 Truth-preserving (or global) semantics As it was mentioned in Section 2, the BALFI semantics for RmbC, as well as its neighborhood semantics presented in Section 5, is degree-preserving instead of truth-preserving (using the terminology from [10]). This requires adapting, in a coherent way, the usual definition of derivation from premises in a Hilbert calculus, recall Definition 2.6. This is exactly the methodology adopted with most normal modal logics in which the semantics is local, thus recovering the deduction metatheorem. But it is also possible to consider global (or truth-preserving) semantics, as it is usually done with algebraic semantics. This leads us to consider the logic RmbC∗, which is defined by the same Hilbert calculus than the one for RmbC, but now derivations from premises in RmbC∗ are defined as usual in Hilbert calculi. Definition 8.1 The logic RmbC∗ is defined by the same Hilbert calculus over signature Σ than RmbC, that is, by adding to mbC the inference rules (R¬) and (R◦). Definition 8.2 (Derivations in RmbC∗) We say that a formula φ is derivable inRmbC∗ from Γ, and we write Γ ⊢RmbC∗ φ, if there exists a finite sequence of formulas φ1 . . . φn such that φn is φ and, for every 1 ≤ i ≤ n, either φi is an instance of an axiom of RmbC, or φi ∈ Γ, or φi is the consequence of some inference rule of RmbC whose premises appear in the sequence φ1 . . . φi−1. Now, the degree-preserving BALFI semantics for RmbC given in Definition 2.10 must be replaced by a truth-preserving consequence relation for RmbC∗: Definition 8.3 (Truth-preserving BALFI semantics) Let Γ∪ {φ} be a set of formulas in For(Θ). We say that φ is a global (or truth-preserving) consequence of Γ in BI, denoted by Γ |=g BI φ, if either φ is valid in BI, or there exists a finite, non-empty subset {γ1, . . . , γn} of Γ such that, for every BALFI B and every valuation v over it, if v(γi) = 1 for every 1 ≤ i ≤ n then v(φ) = 1. The proof of the following result follows by an easy adaptation of the proof of soundness and completeness of RmbC w.r.t. BALFI semantics: 21 Theorem 8.4 (Soundness and completeness of RmbC∗ w.r.t. truth-preserving semantics) For every Γ ∪ {φ} ⊆ For(Θ): Γ ⊢RmbC∗ φ iff Γ |= g BI φ. Remark 8.5 The definition of truth-preserving semantics restricts the number of paraconsistent models for RmbC∗. Indeed, let p and q be two different propositional variables. In order to show that p,¬p 6|=g BI q, there must be a BALFI B and a valuation v over B such that v(p) = v(¬p) = 1 but v(q) 6= 1. That is, B must be such that ¬1 = 1. Since ¬0 = 1, it follows that ¬¬0 = ¬1 = 1 6≤ 0 in B. This shows that there is no paraconsistent extension of RmbC∗ which satisfies axiom (cf). In particular, there is no paraconsistent extension of RmbC∗ satisfying axioms (cf) and (ci). Thus, the open problems solved in Examples 3.8 and 3.9 have a negative answer in this setting. This shows that the truth-preserving approach is much more restricted than the degree-preserving approach in terms of paraconsistency. In any case, there are still paraconsistent BALFIs for the truth-preserving logic RmbC∗ (namely, the ones such that ¬1 = 1). The situation is quite different in the realm of fuzzy logics: in [23, 28], among others, it was studied the degree-preserving companion of several fuzzy logics, showing that their usual truth-preserving consequence relations are never paraconsistent. The distinction between local and global reasoning has been studied by A. Sernadas and his collaborators (for a brief exposition see, for instance, [16], Section 2.3 in Chapter 2). From the proof-theoretical perspective, the Hilbert calculi (called Hilbert calculi with careful reasoning in [16, Definition 2.3.1]) are of the form H = 〈Θ, Rg, Rl〉 where Θ is a propositional signature and Rg ∪ Rl is a set of inference rules such that Rl ⊆ Rg and no element of Rg \Rl is an axiom schema. Elements of Rg and Rl are called global and local inference rules, respectively. Given Γ ∪ {φ} ⊆ For(Θ), φ is globally derivable from Γ in H , written Γ ⊢gH φ, if φ is derivable from Γ in the Hilbert calculus 〈Θ, Rg〉 by using the standard definition (see Definition 8.2). On the other hand, in local derivations, besides using the local rules and the premises, global rules can be used provided that the premises are (global) theorems. In formal terms, φ is locally derivable from Γ in H , written Γ ⊢lH φ, if there exists a finite sequence of formulas φ1 . . . φn such that φn is φ and, for every 1 ≤ i ≤ n, either φi ∈ Γ, or ⊢gH φi, or φi is the consequence of some inference rule of Rl whose premises appear in the sequence φ1 . . . φi−1 (observe that this includes the case when φi is an instance of an axiom in Rl). Obviously, local derivations are global derivations, and local and global theorems coincide. For instance, typically a Hilbert calculus for a (normal) modal logic contains, as local inference rules, (MP) and the axiom schemas, while the set of global rules is (Rl) plus the Necessitation rule. As we have seen in Section 6, the same is the case for minimal non-normal modal logics, but with Replacement for  instead of Necessitation. In this case, the deduction metatheorem only holds for local derivations. Note that, by definition, derivations in RmbC∗ lie in the scope of global derivations, while derivations in RmbC are local derivations. Hence, the extension of mbC with replacement can be recast as a Hilbert calculus with careful reasoning RmbC+ = 〈Σ, Rg, Rl〉 such that Rl contains the axiom schemas of mbC plus (MP), and Rg contains, besides this, the rules (R¬) and (R◦). Of course the same can be done with the axiomatic extensions of mbC (and so of RmbC) considered in Section 3. 22 At the semantical level, local derivations correspond to degree-preserving semantics w.r.t. a given class M of algebras, while global derivations correspond to truth-preserving semantics w.r.t. the class M. The presentation of LFIs with replacement as Hilbert calculi with careful reasoning (as the case of RmbC+) can be useful in order to combine these logics with (standard) normal modal logics by algebraic fibring: in this case, completeness of the fibring of the corresponding Hilbert calculi w.r.t. a semantics given by classes of suitable expansions of Boolean algebras would be immediate, according to the results stated in [16, Chapter 2]. By considering, as done in [41], classes M of powerset algebras (i.e., with domain of the form ℘(W ) for a nonempty setW ) induced by Kripke models (which can be generalized to neighborhood models), then the fibring of, say, RmbC+ with a given modal logic would simply be a minimal logic E with three primitive modalities (, 1, and 2), from which we derive the following modalities: ♦φ def = ∼∼φ, ¬φ def = φ → 1φ, and ◦φ def = ∼(φ ∧ 1φ) ∧ 2φ. This opens interesting opportunities for future research. 9 Extension to first-order logics The next step is extending RmbC, as well as its axiomatic extensions analyzed above, to first-order languages. In order to do this, we will adapt our previous approach to quantified LFIs, see [18], [14, Chapter 7], [24]) to this framework. To begin with, the first-order version RQmbC of RmbC will be introduced. Definition 9.1 Let V ar = {v1, v2, . . .} be a denumerable set of individual variables. A firstorder signature Ω is given as follows: a set C of individual constants; for each n ≥ 1, a set Fn of function symbols of arity n, for each n ≥ 1, a nonempty set Pn of predicate symbols of arity n. The sets of terms and formulas generated by a signature Ω (with underlying propositional signature Σ) will be denoted by Ter(Ω) and For1(Ω), respectively. The set of closed formulas (or sentences) and the set of closed terms (terms without variables) over Ω will be denoted by Sen(Ω) and CTer(Ω), respectively. The formula obtained from a given formula φ by substituting every free occurrence of a variable x by a term t will be denoted by φ[x/t]. Definition 9.2 Let Ω be a first-order signature. The logic RQmbC is obtained from RmbC by adding the following axioms and rules: Axiom Schemas: 23 (Ax∃) φ[x/t] → ∃xφ, if t is a term free for x in φ (Ax∀) ∀xφ→ φ[x/t], if t is a term free for x in φ Inference rules: (∃-In) φ→ ψ ∃xφ→ ψ , where x does not occur free in ψ (∀-In) φ→ ψ φ→ ∀xψ , where x does not occur free in φ The consequence relation of RQmbC, adapted from the one for RmbC (recall Definition 2.6) will be denoted by ⊢RQmbC. Remarks 9.3 (1) It is worth mentioning that the only difference between QmbC and RQmbC is that the latter contains the inference rules (R¬) and (R◦), which are not present in the former (besides the different notions of derivation from premisses adopted in QmbC and in RQmbC). (2) Recall that a Hilbert calculus with careful reasoning for RmbC called RmbC+ was defined at the end of Section 8. This can extended to RQmbC by considering the Hilbert calculus with careful reasoning RQmbC+ over a given first-order signature Ω, such that Rl contains the axiom schemas of QmbC (over Ω) plus (MP), and Rg contains, besides this, the rules (R¬), (R◦), (∃-In) and (∀-In) (over Ω). 10 BALFI semantics for RQmbC In [24] a semantics of first-order structures based on swap structures over complete Boolean algebras was obtained for QmbC, a first-order version of mbC proposed in [18]. Since RQmbC is self-extensional, that semantics can be drastically simplified, and so the non-deterministic swap structures will be replaced by BALFIs, which are ordinary algebras. From now on, only BALFIs over complete Boolean algebras will be considered. Definition 10.1 A complete BALFI is a BALFI such that its reduct to ΣBA is a complete Boolean algebra. Definition 10.2 Let B be a complete BALFI, and let Ω be a first-order signature. A (firstorder) structure over B and Ω (or a RQmbC-structure over Ω) is a pair A = 〈U, IA〉 such that U is a nonempty set (the domain or universe of the structure) and IA is an interpretation function which assigns: an element IA(c) of U to each individual constant c ∈ C; a function IA(f) : U n → U to each function symbol f of arity n; a function IA(P ) : U n → A to each predicate symbol P of arity n. 24 Notation 10.3 From now on, we will write cA, fA and PA instead of IA(c), IA(f) and IA(P ) to denote the interpretation of an individual constant symbol c, a function symbol f and a predicate symbol P , respectively. Definition 10.4 Given a structure A over B and Ω, an assignment over A is any function μ : V ar → U . Definition 10.5 Given a structure A over B and Ω, and given an assignment μ : V ar → U we define recursively, for each term t, an element [[t]]Aμ in U as follows: - [[c]]Aμ = c A if c is an individual constant; - [[x]]Aμ = μ(x) if x is a variable; - [[f(t1, . . . , tn)]] A μ = f A([[t1]] A μ , . . . , [[tn]] A μ) if f is a function symbol of arity n and t1, . . . , tn are terms. Definition 10.6 Let A be a structure over B and Ω. The diagram language of A is the set of formulas For1(ΩU ), where ΩU is the signature obtained from Ω by adding, for each element u ∈ U , a new individual constant ū. Definition 10.7 The structure Â = 〈U, I Â 〉 over ΩU is the structure A over Ω extended by I Â (ū) = u for every u ∈ U . It is worth noting that sÂ = sA whenever s is a symbol (individual constant, function symbol or predicate symbol) of Ω. Notation 10.8 The set of sentences or closed formulas (that is, formulas without free variables) of the diagram language For1(ΩU ) is denoted by Sen(ΩU), and the set of terms and of closed terms over ΩU will be denoted by Ter(ΩU) and CTer(ΩU), respectively. If t is a closed term we can write [[t]]A instead of [[t]]Aμ , for any assignment μ, since it does not depend on μ. Definition 10.9 (RQmbC interpretation maps) Let B be a complete BALFI, and let A be a structure over B and Ω. The interpretation map for RQmbC over A and B is a function [[*]]A : Sen(ΩU ) → A satisfying the following clauses: (i) [[P (t1, . . . , tn)]] A = PA([[t1]] Â, . . . , [[tn]] Â), if P (t1, . . . , tn) is atomic; (ii) [[#φ]]A = #[[φ]]A, for every # ∈ {¬, ◦}; (iii) [[φ#ψ]]A = [[φ]]A # [[ψ]]A, for every # ∈ {∧,∨,→}; (iv) [[∀xφ]]A = ∧ u∈U [[φ[x/ū]]] A; (v) [[∃xφ]]A = ∨ u∈U [[φ[x/ū]]] A. Recall the notation stated in Definition 10.6. The interpretation map can be extended to arbitrary formulas as follows: 25 Definition 10.10 Let B be a complete BALFI, and let A be a structure over B and Ω. Given an assignment μ over A, the extended interpretation map [[*]]Aμ : For1(ΩU ) → A is given by [[φ]]Aμ = [[φ[x1/μ(x1), . . . , xn/μ(xn)]]] A, provided that the free variables of φ occur in {x1, . . . , xn}. For every u ∈ U and every assignment μ, let μxu be the assignment such that μ x u(x) = u and μxu(y) = μ(y) if y 6= x. Then, it is immediate to see that [[φ]] A μx u = [[φ[x/ū]]]Aμ , for every formula φ. Definition 10.11 Let B be a complete BALFI, and let A be a structure over B and Ω. (1) Given a formula φ in For1(ΩU ), φ is said to be valid in (A,B), denoted by |=(A,B) φ, if [[φ]]Aμ = 1, for every assignment μ. (2) Given a set of formulas Γ∪{φ} ⊆ For1(ΩU), φ is said to be a semantical consequence of Γ w.r.t. (A,B), denoted by Γ |=(A,B) φ, if either φ is valid in (A,B), or there exists a finite, non-empty subset {γ1, . . . , γn} of Γ such that the formula (γ1∧(γ2∧(. . .∧(γn−1∧γn) . . .))) → φ is valid in (A,B). Definition 10.12 (First-order degree-preserving BALFI semantics) Let Γ ∪ {φ} ⊆ For1(Ω) be a set of formulas. Then φ is said to be a semantical consequence of Γ in RQmbC w.r.t. BALFIs, denoted by Γ |=RQmbC φ, if Γ |=(A,B) φ for every pair (A,B). As in the case of RmbC, given that RQmbC uses local reasoning, it satisfies the deduction metatheorem without any restrictions. This is different to what happens with QmbC, where this metatheorem holds with the same restrictions than in first-order classical logic. Theorem 10.13 (Deduction Metatheorem for RQmbC) Γ, φ ⊢RQmbC ψ if and only if Γ ⊢RQmbC φ→ ψ. In order to prove the soundness of RQmbC w.r.t. BALFI semantics, it is necessary to state an important result: Theorem 10.14 (Substitution Lemma) Let B be a complete BALFI, A a structure over B and Ω, and μ an assignment over A. If t is a term free for z in φ and b = [[t]]Âμ , then [[φ[z/t]]]Aμ = [[φ[z/b]]] A μ . Proof. It is proved by induction on the complexity of φ. ✷ Theorem 10.15 (Soundness of RQmbC w.r.t. BALFIs) For every set Γ ∪ {φ} ⊆ For1(Ω): Γ ⊢RQmbC φ implies that Γ |=RQmbC φ. Proof. It will be proven by extending the proof of soundness of RmbC w.r.t. BALFI semantics (Theorem 2.12). Thus, the only cases required to be analyzed are the new axioms and inference rules. By the very definitions, and taking into account Theorem 10.14, it is immediate to see that axioms (Ax∃) and (Ax∀) are valid in any (A,B). With respect to (∃-In), suppose that α → β is valid in a given (A,B), where the variable x does not occur free in β. Then [[α]]Aμ ≤ [[β]] A μ for every assignment μ. In particular, for every u ∈ U , [[α]]Aμx u ≤ [[β]]Aμx u = [[β]]Aμ , since x is not free in β. But then: [[∃xα]] A μ = ∨ u∈U [[α[x/ū]]] A μ =∨ u∈U [[α]] A μx u ≤ [[β]]Aμ . Hence, ∃xα → β is valid in (A,B). The case for (∀-In) is proved analogously. ✷ 26 11 Completeness of RQmbC w.r.t. BALFI semantics This section is devoted to prove the completeness of RQmbC w.r.t. BALFI semantics. The proof will be an adaptation to the completeness proof for QmbC w.r.t. swap structures semantics given in [24]. Definition 11.1 Consider a theory ∆ ⊆ For1(Ω) and a nonempty set C of constants of the signature Ω. Then, ∆ is called a C-Henkin theory in RQmbC if it satisfies the following: for every formula φ with (at most) a free variable x, there exists a constant c in C such that ∆ ⊢RQmbC ∃xφ → φ[x/c]. Remark 11.2 As observed in [24], it is easy to show that, if ∆ is a C-Henkin theory in QmbC and φ is a formula with (at most) a free variable x then there is a constant c in C such that ∆ ⊢QmbC φ[x/c] → ∀xφ. Of course the same result holds for RQmbC. Definition 11.3 Let ΩC be the signature obtained from Ω by adding a set C of new individual constants. The consequence relation ⊢CRQmbC is the consequence relation of RQmbC over the signature ΩC . Recall that, given a Tarskian and finitary logic L = 〈For,⊢〉 (where For is the set of formulas of L), and given a set Γ ∪ {φ} ⊆ For, the set Γ is said to be maximally non-trivial with respect to φ in L if the following holds: (i) Γ 0 φ, and (ii) Γ, ψ ⊢ φ for every ψ /∈ Γ. By straightforwardly adapting [24, Proposition 8.4] from QmbC to RQmbC, we obtain the following: Proposition 11.4 Let Γ ∪ {φ} ⊆ Sen(Ω) such that Γ 0RQmbC φ. Then, there exists a set of formulas ∆ ⊆ For1(ΩC), for some nonempty set C of new individual constants, such that Γ ⊆ ∆, ∆ is a C-Henkin theory in RQmbC and, in addition, ∆ is maximally non-trivial with respect to φ in RQmbC. Definition 11.5 Consider a set ∆ ⊆ For1(Ω) which is non-trivial in RQmbC, that is: there is some formula φ in For1(Ω) such that ∆ 0RQmbC φ. Let ≡∆ ⊆ For1(Ω)2 be the relation in For1(Ω) defined as follows: α ≡∆ β iff ∆ ⊢RQmbC α↔ β. By adapting the proof of Theorem 2.13 it follows that ≡∆ is an equivalence relation which induces a Boolean algebra A∆ def = 〈A∆,∧,∨,→, 0∆, 1∆〉, where A∆ def = For1(Ω)/≡∆ , [α]∆#[β]∆ def = [α#β]∆ for any # ∈ {∧,∨,→}, 0∆ def = [φ∧(¬φ∧◦φ)]∆ and 1∆ def = [φ∨¬φ]∆. Moreover, by defining #[α]∆ def = [#α]∆ for any # ∈ {¬, ◦} we obtain a BALFI denoted by B∆. The construction of the canonical model for RQmbC w.r.t. ∆ requires a complete BALFI, hence the Boolean algebra A∆ must be completed. Recall13 that a Boolean algebra A′ is a completion of a Boolean algebra A if: (1) A′ is complete, and (2) A′ includes A as a dense subalgebra (that is: every element in A′ is the supremum, in A′, of some subset of A). From this, A′ preserves all the existing infima and suprema in A. In formal terms: there 13See, for instance, [29, Chapter 25]. 27 exists a monomorphism of Boolean algebras (therefore an injective mapping) ∗ : A → A′ such that ∗( ∨ AX) = ∨ A′ ∗[X ] for every X ⊆ A such that the supremum ∨ AX exists, where ∗[X ] = {∗(a) : a ∈ X}. Analogously, ∗( ∧ AX) = ∧ A′ ∗[X ] for every X ⊆ A such that the infimum ∧ AX exists. By the well-known results obtained independently by MacNeille and Tarski, it follows that every Boolean algebra has a completion; moreover, the completion is unique up to isomorphisms. Based on this, let CA∆ be the completion of A∆ and let ∗ : A∆ → CA∆ be the associated monomorphism. Definition 11.6 Let CA∆ be the complete Boolean algebra defined as above. The canonical BALFI for RQmbC over ∆, denoted by B∆, is obtained from CA∆ by adding the unary operators ¬ and ◦ defined as follows: ¬b = ∗(¬a) if b = ∗(a), and ¬b = ∼b if b /∈ ∗[A∆]; ◦b = ∗(◦a) if b = ∗(a), and ◦b = 1 if b /∈ ∗[A∆]. Proposition 11.7 The operations over B∆ are well-defined, and B∆ is a complete BALFI such that ∗([α]∆) = 1 iff ∆ ⊢RQmbC α. Proof. Since ∗[A∆] is a subalgebra of CA∆, b /∈ ∗[A∆] iff ∼b /∈ ∗[A∆]. On the other hand, ∗ is injective. This shows that ¬ and ◦ are well-defined. The rest of the proof is obvious from the definitions. ✷ Definition 11.8 (Canonical Structure) Let Ω be a signature with some individual constant. Let ∆ ⊆ For1(Ω) be non-trivial in RQmbC, let B∆ be as in Definition 11.6, and let U = CTer(Ω). The canonical structure induced by ∆ is the structure A∆ = 〈U, IA∆〉 over B∆ and Ω such that: cA∆ = c, for each individual constant c; fA∆ : Un → U is such that fA∆(t1, . . . , tn) = f(t1, . . . , tn), for each function symbol f of arity n; PA∆(t1, . . . , tn) = ∗([P (t1, . . . , tn)]∆), for each predicate symbol P of arity n. Definition 11.9 Let (*)⊲ : (Ter(ΩU)∪For1(ΩU)) → (Ter(Ω)∪For1(Ω)) be the mapping such that ( s )⊲ is the expression obtained from s by substituting every occurrence of a constant t by the term t itself, for t ∈ CTer(Ω). Lemma 11.10 Let ∆ ⊆ For1(Ω) be a set of formulas over a signature Ω such that ∆ is a C-Henkin theory in RQmbC for a nonempty set C of individual constants of Ω, and ∆ is maximally non-trivial with respect to φ in RQmbC, for some sentence φ. Then, for every formula ψ(x) with (at most) a free variable x it holds: (1) [∀xψ]∆ = ∧ A∆ {[ψ[x/t]]∆ : t ∈ CTer(Ω)}, where ∧ A∆ denotes an existing infimum in the Boolean algebra A∆; (2) [∃xψ]∆ = ∨ A∆ {[ψ[x/t]]∆ : t ∈ CTer(Ω)}, where ∨ A∆ denotes an existing supremum in the Boolean algebra A∆. 28 Proof. (1) By definition, and by the rules from CPL+, [α]∆ ≤ [β]∆ in A∆ iff ∆ ⊢RQmbC α → β. Let ψ(x) be a formula with (at most) a free variable x. Then [∀xψ]∆ ≤ [ψ[x/t]]∆ for every t ∈ CTer(Ω), by (Ax∀). Let β be a formula such that [β]∆ ≤ [ψ[x/t]]∆ for every t ∈ CTer(Ω). By Remark 11.2 and the definition of order in A∆, there is a constant c in C such that [ψ[x/c]]∆ ≤ [∀xψ]∆. Since [β]∆ ≤ [ψ[x/c]]∆, it follows that [β]∆ ≤ [∀xψ]∆. This shows that [∀xψ]∆ = ∧ A∆ {[ψ[x/t]]∆ : t ∈ CTer(Ω)}. Item (2) is proved analogously. ✷ Proposition 11.11 Let ∆ ⊆ For1(Ω) be as in Lemma 11.10. Then, the interpretation map [[*]]A∆ : Sen(ΩU ) → CA∆ is such that [[ψ]]A∆ = ∗([(ψ)⊲]∆) for every sentence ψ in Sen(ΩU ). Moreover, [[ψ]]A∆ = 1∆ iff ∆ ⊢RQmbC (ψ)⊲. In particular, [[ψ]]A∆ = 1∆ iff ∆ ⊢RQmbC ψ for every ψ ∈ Sen(Ω). Proof. The proof is done by induction on the complexity of the sentence ψ in Sen(ΩU ). If ψ = P (t1, . . . , tn) is atomic then, by using Definition 10.9, the fact that [[t]] Â∆ = (t)⊲ for every t ∈ CTer(ΩU), and Definition 11.8, we have: [[ψ]]A∆ = PA∆([[t1]] Â∆ , . . . , [[tn]] Â∆) = PA∆((t1) ⊲, . . . , (tn) ⊲) = ∗([(ψ)⊲]∆). If ψ = #β for # ∈ {¬, ◦} then, by Definition 10.9 and by induction hypothesis, [[ψ]]A∆ = #[[β]]A∆ = #(∗([(β)⊲]∆)) = ∗([(#β) ⊲]∆). If ψ = α#β for # ∈ {∧,∨,→}, the proof is analogous. If ψ = ∀xβ then, by Lemma 11.10 and using that U = CTer(Ω), [∀xβ]∆ = ∧ A∆ {[β[x/t]]∆ : t ∈ U} and so ∗([∀xβ]∆) = ∧ CA∆ {∗([β[x/t]]∆) : t ∈ U}. Then, by Definition 10.9 and by induction hypothesis: [[∀xβ]]A∆ = ∧ t∈U [[β[x/t]]]A∆ = ∧ t∈U ∗([(β[x/t])⊲]∆) = ∗([(∀xβ) ⊲]∆). If ψ = ∃xβ, the proof is analogous to the previous case. This shows that [[ψ]]A∆ = ∗([(ψ)⊲]∆) for every sentence ψ. The rest of the proof follows by Proposition 11.7. ✷ Theorem 11.12 (Completeness of RQmbC w.r.t. BALFI semantics) For every Γ ∪ {φ} ⊆ Sen(Ω): if Γ |=RQmbC φ then Γ ⊢RQmbC φ. Proof. Suppose that Γ∪{φ} ⊆ Sen(Ω) is such that Γ 0RQmbC φ. By Proposition 11.4, there exists a C-Henkin theory ∆ over ΩC in RQmbC, for some nonempty set C of new individual constants, such that Γ ⊆ ∆ and, in addition, ∆ is maximally non-trivial with respect to φ in RQmbC. Consider now B∆ and A∆ as in Definitions 11.6 and 11.8, respectively. By Proposition 11.11, [[ψ]]A∆ = 1∆ iff ∆ ⊢CRQmbC ψ, for every ψ in Sen(ΩC). But then [[γ]] A∆ = 1∆ for every γ ∈ Γ and [[φ]]A∆ 6= 1∆. Now, let A the reduct of A∆ to Ω. Hence, A is a structure over B∆ and Ω such that [[γ]]A = 1∆ for every γ ∈ Γ but [[φ]]A 6= 1∆. From this, 6|=RQmbC φ. In addition, for every non-empty set {γ1, . . . , γn} ⊆ Γ it is the case that ∧n i=1[[γi]] A = 1 6≤ [[φ]]A. Therefore the formula (γ1 ∧ (γ2 ∧ (. . . ∧ (γn−1 ∧ γn) . . .))) → φ is not valid in (A,B∆). This means that Γ 6|=RQmbC φ. ✷ 29 Remark 11.13 The completeness result for RQmbC w.r.t. BALFI semantics was obtained just for sentences, and not for formulas possibly containing free variables (as it was done with the soundness Theorem 10.15). This can be easily overcome. Recall that the universal closure of a formula ψ in For1(Ω), denoted by (∀)ψ, is defined as follows: if ψ is a sentence then (∀)ψ def = ψ; and if ψ has exactly the variables x1, . . . , xn occurring free then (∀)ψ def = (∀x1) * * * (∀xn)ψ. If Γ is a set of formulas in For1(Ω) then (∀)Γ def = {(∀)ψ : ψ ∈ Γ}. It is easy to show that, for every Γ ∪ {φ} ⊆ For1(Ω): (i) Γ ⊢RQmbC φ iff (∀)Γ ⊢RQmbC (∀)φ; and (ii) Γ |=RQmbC φ iff (∀)Γ |=RQmbC (∀)φ. From this, a general completeness for RQmbC result follows from Theorem 11.12. 12 Conclusion, and significance of the results This paper offers a solution for two open problems in the domain of paraconsistency, in particular connected to algebraization of LFIs. The quest for the algebraic counterpart of paraconsistency is more than 50 years old: since the inception of da Costa's paraconsistent calculi, algebraic equivalents for such systems have been searched, with different degrees of success (and failure). Our results suggest that the new concepts and methods proposed in the present paper, in particular the neighborhood style semantics connected to BALFIs, have a good potential for applications. As suggested in [32], modal logics could alternatively be regarded as the study of a kind of modal-like contradiction-tolerant systems. In alternative to founding modal semantics in terms of belief, knowledge, tense, etc., modal logic could be regarded as a general 'theory of opposition', more akin to the Aristotelian tradition. Applications of paraconsistent logics in computer science, probability and AI, just to mention a few areas, are greatly advanced when more traditional algebraic tools pertaining to extensions of Boolean algebras and neighborhood semantics, are used to express the underlying ideas of paraconsistency. In addition, many logical systems employed in deontic logic and normative reasoning, where non-normal modal logics and neighborhood semantics play an important role, could be extended by means of our approach. Hopefully, our results may unlock new research in this direction. Finally, BALFI semantics for LFIs opens the possibility of obtaining new algebraic models for paraconsistent set theory (see [13, 15]) by generalizing the well-known Boolean-valued models for ZF (see [5]). Acknowledgements: The first and second authors acknowledge support from the National Council for Scientific and Technological Development (CNPq), Brazil under research grants 307376/2018-4 and 306530/2019-8, respectively. References [1] Avron, A., Non-deterministic matrices and modular semantics of rules. In J.-Y. Béziau, editor, Logica Universalis, pages 149–167. Basel: Birkhäuser Verlag, 2005. [2] Avron, A., Self-Extensional Three-Valued Paraconsistent Logics. Logica Universalis, 11, 297–315, 2017. 30 [3] Avron, A. and Béziau, J.-Y., Self-extensional three-valued paraconsistent logics have no implication. Logic Journal of the IGPL, 25(2):183–194, 2017. [4] Avron, A. and Zamansky, A., A paraconsistent view on B and S5. In: L. Beklemishev, S. Demri and A. Máté (eds), Advances in Modal Logic, volume 11, pages 21–37. London: College Publications, 2016. [5] Bell, J. L., Set Theory: Boolean-Valued Models and Independence Proofs, Third edition. Volume 47 of the Oxford Logic Guides Series. Oxford University Press, 2005. [6] Béziau, J.-Y., Idempotent Full Paraconsistent Negations are not Algebraizable. Notre Dame Journal of Formal Logic, 39(1):135–139, 1998. [7] Béziau, J.-Y., S5 is a paraconsistent logic and so is first-order classical logic. Logical Studies, 9:301–309, 2002. [8] Béziau, J.-Y., Paraconsistent logic from a modal viewpoint. Journal of Applied Logic, 3:7–14, 2005. [9] Blok, W J. and Pigozzi, D., Algebraizable Logics. Volume 77(396) of Memoirs of the American Mathematical Society. Providence: American Mathematical Society, 1989. [10] Bou, F., Esteva, F., Font, J. M., Gil, A., Godo, L., Torrens A. and Verdú, V., Logics preserving degrees of truth from varieties of residuated lattices. Journal of Logic and Computation, 19(6)1031–1069, 2009. [11] Bueno-Soler, J. and Carnielli W., Experimenting with Consistency. In: V. Markin and D. Zaitsev (eds.), The Logical Legacy of Nikolai Vasiliev and Modern Logic, pages 199– 221. Synthese Library (Studies in Epistemology, Logic, Methodology, and Philosophy of Science), vol 387. Cham: Springer, 2017. [12] Carnielli, W. A. and Coniglio, M. E., Combining Logics. In: E.N. Zalta (ed.), The Stanford Encyclopedia of Philosophy, 2007. URL: http://plato.stanford.edu/entries/logic-combining/ [13] Carnielli, W. A. and Coniglio, M. E., Paraconsistent set theory by predicating on consistency. Journal of Logic and Computation 26(1):97–116, 2016. First published online: 09 July 2013. [14] Carnielli, W. A. and Coniglio, M. E., Paraconsistent Logic: Consistency, Contradiction and Negation. Volume 40 of Logic, Epistemology, and the Unity of Science series. Cham: Springer, 2016. [15] Carnielli, W. A. and Coniglio, M. E., Twist-Valued Models for Three-valued Paraconsistent Set Theory. arXiv:1911.11833 [math.LO], 2019. [16] Carnielli, W. A., Coniglio, M. E., Gabbay, D., Gouveira, P. and Sernadas, C., Analysis and Synthesis of Logics: How to Cut and Paste Reasoning Systems. Volume 35 of Applied Logic series. Dordrecht: Springer, 2008. 31 [17] Carnielli, W. A., Coniglio, M. E. and Marcos, J., Logics of Formal Inconsistency. In: D. M. Gabbay and F. Guenthner, editors, Handbook of Philosophical Logic (2nd. edition), volume 14, pages 1–93. Dordrecht: Springer, 2007. [18] Carnielli, W. A., Coniglio, M. E., Podiacki, R. and Rodrigues, T., On the way to a wider model theory: Completeness theorems for first-order logics of formal inconsistency. The Review of Symbolic Logic, 7(3):548–578, 2014. [19] Carnielli, W. A. and de Alcantara, L. P., Paraconsistent Algebras. Studia Logica 43(1/2):79–88, 1984 [20] Carnielli, W.A. and Lima-Marques, M., Society semantics for multiple-valued logics. In: W.A. Carnielli and I.M.L. D'Ottaviano (eds.), Advances in Contemporary Logic and Computer Science, pages 33-52. Volume 235 of Contemporary Mathematics Series. Providence: American Mathematical Society, 1999. [21] Carnielli, W. A. and Marcos, J., A taxonomy of C-systems. In: W. A. Carnielli, M. E. Coniglio, and I. M. L. D'Ottaviano, editors, Paraconsistency: The Logical Way to the Inconsistent, volume 228 of Lecture Notes in Pure and Applied Mathematics, pages 1–94. New York: Marcel Dekker, 2002. [22] Chellas, B.F., Modal Logic: An Introduction. New York: Cambridge University Press, 1980. [23] Coniglio, M. E., Esteva, F. and Godo, L., Logics of formal inconsistency arising from systems of fuzzy logic. Logic Journal of the IGPL, 22(6):880–904, 2014. [24] Coniglio, M.E., Figallo-Orellano A. and Golzio, A. C., First-order swap structures semantics for some Logics of Formal Inconsistency. Journal of Logic and Computation, to appear, 2020. Preprint available at arXiv:1912.10277 [math.LO]. [25] Coniglio, M.E. and Prieto-Sanabria, L., Modal logic S4 as a paraconsistent logic with a topological semantics. In: P. Gouveia, C. Caleiro and F. Donisio (eds.), Logic and Computation: Essays in Honour of Amilcar Sernadas, pages 171–196. Volume 33 of Tributes Series. London: College Publications, 2017. [26] da Costa. N. C. A., Sistemas formais inconsistentes (Inconsistent formal systems, in Portuguese). Habilitation thesis, Universidade Federal do Paraná, Curitiba, Brazil, 1963. Republished by Editora UFPR, Curitiba, Brazil,1993. [27] de Araújo, A. L., Alves, E. H. and Guerzoni, J. A. D., Some relations between modal and paraconsistent logic. The Journal of Non-Classical Logic, 4(2):33–44, 1987. Available at http://www.cle.unicamp.br/jancl/. [28] Ertola, R., Esteva, F., Flaminio, T, Godo, L. and and Noguera, C., Exploring paraconsistency in degree-preserving fuzzy logics. Soft Computing, 19(3):531–546, 2015. [29] Givant, S. and Halmos, P., Introduction to Boolean Algebras. New York: Springer, 2009. 32 [30] Jónsson, B., A Survey of Boolean Algebras with Operators. In: I.G. Rosenberg and G. Sabidussi, editors, Algebras and Orders, volume 389 of NATO ASI Series (Series C: Mathematical and Physical Sciences), pages 239–286. Dordrecht: Springer, 1993. [31] Lewin, R. A., Mikenberg, I. F. and Schwarze, M. G., C1 is not algebraizable. Notre Dame Journal of Formal Logic, 32(4):609–611, 1991. [32] Marcos, J., Modality and paraconsistency. In M. Bilkova and L. Behounek, editors. The Logica Yearbook 2004, Proceedings of the XVIII International Symposium promoted by the Institute of Philosophy of the Academy of Sciences of the Czech Republic. Filosofia, Prague, 2005. [33] Marcos, J., Nearly every normal modal logic is paranormal. Logique et Analyse, 48(189192):279–300, 2005. [34] Mortensen, C., Every quotient algebra for C1 is trivial. Notre Dame Journal of Formal Logic, 21(4):694–700, 1980. [35] Mortensen, C., Paraconsistency and C1. In G. Priest and R. Routley and J. Norman (eds), Paraconsistent Logic: Essays on the Inconsistent, pages 289–305. Munich: Philosophia Verlag, 1989. [36] Nipkow, T., Paulson, L. C. and Wenzel, M., Isabelle/HOL: a proof assistant for higherorder logic. Volume 2283 of Springer Science & Business Media. Springer, 2002. [37] Pacuit, E., Neighborhood semantics for modal logic. Springer, 2017. [38] Segerberg, K., Classical Propositional Operators: An exercise in the foundations of logic. Volume 5 of Oxford Logic Guides. Oxford: Clarendon Press, 1982 [39] Seoane, J. and de Alcantara, L. P., On da Costa algebras. The Journal of Non-Classical Logic 8(2):41–66, 1991. [40] Wójcicki, R., Theory of logical calculi: Basic theory of consequence operations. Volume 199 of Synthese Library. Dordrecht: Reidel, 1988. [41] Zanardo, A., Sernadas, A. and Sernadas, C., Fibring: Completeness preservation. Journal of Symbolic Logic, 66(1):414–439, 2001.