Recovery operators, paraconsistency and duality Walter Carnielli∗ Marcelo Esteban Coniglio∗ Abilio Rodrigues∗∗ ∗Department of Philosophy and Centre for Logic, Epistemology and the History of Science University of Campinas, Brazil Email: {walter.carnielli, coniglio}@cle.unicamp.br ∗∗Departament of Philosophy Federal University of Minas Gerais, Brazil Email: abilio@ufmg.br Abstract There are two foundational, but not fully developed, ideas in paraconsistency, namely, the duality between paraconsistent and intuitionistic paradigms, and the introduction of logical operators that express meta-logical notions in the object language. The aim of this paper is to show how these two ideas can be adequately accomplished by the Logics of Formal Inconsistency (LFIs) and by the Logics of Formal Undeterminedness (LFUs). LFIs recover the validity of the principle of explosion in a paraconsistent scenario, while LFUs recover the validity of the principle of excluded middle in a paracomplete scenario. We introduce definitions of duality between inference rules and connectives that allow comparing rules and connectives that belong to different logics. Two formal systems are studied, the logics mbC and mbD, that display the duality between paraconsistency and paracompleteness as a duality between inference rules added to a common core – in the case studied here, this common core is classical positive propositional logic (CPL+). The logics mbC and mbD are equipped with 1 recovery operators that restore classical logic for, respectively, consistent and determined propositions. These two logics are then combined obtaining a pair of logics of formal inconsistency and undeterminedness (LFIUs), namely, mbCD and mbCDE. The logic mbCDE exhibits some nice duality properties. Besides, it is simultaneously paraconsistent and paracomplete, and able to recover the principles of excluded middle and explosion at once. The last sections offer an algebraic account for such logics by adapting the swap-structures semantics framework of the LFIs the LFUs. This semantics highlights some subtle aspects of these logics, and allows us to prove decidability by means of finite non-deterministic matrices. 1 Introduction Although paraconsistent logics have not been invented by da Costa, it is fairly certain that in 1963 da Costa [17] not only presented the broadest formal study of paraconsistency proposed up to that time but also established a fruitful research program in logic and philosophy of logic.1 The role of da Costa's work in establishing paraconsistency as an area of study is undisputed. There are two foundational ideas in da Costa's approach to paraconsistency. The first is the division of propositions into two groups: those for which explosion does not hold and those for which explosion holds. The latter are called 'well-behaved', which means that the principle of non-contradiction holds for them. It is safe to employ classical logic only for well-behaved propositions, while the others demand a non-explosive logic. The second idea is the duality between da Costa's logic C1 and intuitionistic logic. It is clear that some kind of duality between paraconsistent and intuitionistic logic has had an important role as a motivation for the axioms da Costa chose for C1. However, we argue here that da Costa not only missed the point regarding the duality but also mistakenly emphasized the invalidity of non-contradiction instead of explosion as the central feature of paraconsistent logics. The aim of this paper is to show how these two ideas can be developed by Logics of Formal Inconsistency (LFIs) and Logics of Formal 1The concept of a logic without an explosive negation can be traced back to 1910, in the work of Vasiliev (see [26] pp. 307ff), while the first non-explosive logic has been presented in 1948 by Jaśkowski in [28]. For a comprehensive account of the history of paraconsistency, see Gomes [26] 2 Undeterminedness (LFUs). The former recovers the validity of the principle of explosion in a paraconsistent scenario, while the latter recovers the validity of the excluded middle in a paracomplete scenario. The remainder of this paper is organized as follows. Section 2 examines how da Costa presented the well-behavedness operator and the 'duality' between C1 and intuitionistic logic. In Section 3 we present the consistency and determinedness connectives ◦ and 9 as recovery operators that restore, respectively, explosion and excluded middle. Section 4 presents two formal systems, the logics mbC and mbD, that display the duality between paraconsistency and paracompleteness as a duality between inference rules added to a common core – in the case studied here, classical positive propositional logic (CPL+). mbC andmbD are equipped with recovery operators that restore classical logic for, respectively, consistent and determined propositions. These two logics are then combined obtaining the logics of formal inconsistency and undeterminedness (LFIUs), mbCD and mbCDE. Finally, the swap structures semantics framework for LFIs, introduced by Carnielli and Coniglio in [7, chapter 6], is adapted here for LFUs and LFIUs. This semantics allows us to prove the decidability of the proposed systems by means of finite non-deterministic matrices. 2 Well-behavedness and 'duality' in da Costa's Cn hierarchy 2.1 da Costa's well-behavedness operator We begin by defining da Costa's Cn hierarchy. Definition 1 (Intuitionistic Positive Logic) The intuitionistic positive logic IPL+ is defined over the signature Σ+ = {∧,∨,→} by the following Hilbert calculus: 3 Axiom schemas: α→ ( β → α ) (AX1 )( α→ ( β → γ )) → (( α→ β ) → ( α→ γ )) (AX2 ) α→ ( β → ( α ∧ β )) (AX3 )( α ∧ β ) → α (AX4 )( α ∧ β ) → β (AX5 ) α→ ( α ∨ β ) (AX6 ) β → ( α ∨ β ) (AX7 )( α→ γ ) → ( (β → γ)→ ( (α ∨ β)→ γ )) (AX8 ) Inference rule: α α→ β β (MP) Definition 2 (da Costa's Cn hierarchy) Let 1 ≤ n < ω. The system Cn is defined over the signature ΣC = {∧,∨,→,¬} by adding to the axioms of intuitionistic positive logic IPL+ the following axiom schemas (see [17]): α ∨ ¬α (AxPEM ) ¬¬α→ α (AxDN ) β(n) → ((α→ β)→ ((α→ ¬β)→ ¬α)) (AxCn1 )( α(n) ∧ β(n) ) → ( (α ∧ β)(n) ∧ (α ∨ β)(n) ∧ (α→ β)(n) ) (AxCn2 ) Notice that the Cn hierarchy is defined as an extension of IPL+ but it is also an extension of Classical Positive Logic CPL+, since (α → β) ∨ α (AX9 in Definition 14) can be proved in it. Each calculus of da Costa's Cn hierarchy has its own 'well-behavedness' operator, defined inductively such that, for each n, 1 ≤ n < ω, α,¬α 0Cn β, while α(n), α,¬α `Cn β. In formal terms: Definition 3 Let α be a formula in the signature ΣC and consider the following abbreviations: (1) α◦ def= ¬(α ∧ ¬α); 4 (2) α0 def= α, and αn+1 def= (αn)◦, for 0 ≤ n < ω; (3) α(1) def= α◦, and α(n+1) def= α(n) ∧ αn+1, for 1 ≤ n < ω. For instance, α1 = α(1) = α◦; α2 = α◦◦ and α(2) = α◦ ∧ α◦◦; while α3 = α◦◦◦ and α(3) = (α◦ ∧ α◦◦) ∧ α◦◦◦. Thus, a proposition α behaves classically: in C1, when α(1) = α◦ = ¬(α ∧ ¬α) holds, in C2, when α(2) = α◦ ∧ α◦◦ holds, in C3, when α(3) = (α◦ ∧ α◦◦) ∧ α◦◦◦ holds, and so on. As the value of n grows, the negation gets weaker, and a monotonic hierarchy of logics is obtained. However, until now, this idea of increasingly weaker logics has not been as successful as the introduction of an operator capable of expressing metalogical notions in the object language.2 A not well-behaved proposition α does not cause any harm in C1, if it is contradictory. On the other hand, α ∧ ¬α and ¬(α ∧ ¬α) cannot hold simultaneously: the latter by definition is α◦, and so, together with α ∧ ¬α, triviality follows. Thus, α ∧ ¬α is 'axiomatically well-behaved' in C1. This seems strange: the point is not that in a paraconsistent logic α∧¬α and ¬(α∧ ¬α) must always be allowed to hold simultaneously. The point, rather, is that α∧¬α and ¬(α∧¬α) should not be prohibited to hold simultaneously. So, it should be possible to devise paraconsistent logics such that the consistency of α is logically independent of ¬(α ∧ ¬α). The Logics of Formal Inconsistency (LFIs, see [7], [8] and [9]) are paraconsistent logics that develop da Costa's approach further by internalizing the concept of consistency within the object language using the connective ◦. In LFIs ◦α means that α is consistent, but ◦ is introduced in such a way that ◦α is logically independent of ¬(α ∧ ¬α). Analogously to the Cn hierarchy, α,¬α 0LFI β, while ◦α, α,¬α `LFI β. Splitting propositions into two classes, consistent and the inconsistent, is in accordance with the fact that in a paraconsistent logic it cannot be that all contradictions are logically equivalent, otherwise the principle of explosion holds. The proof of this fact is straightforward. If all contradictions are 2Instead of a hierarchy in which negations get weaker, a hierarchy of logics in which consistency gets stronger will be presented in Section 4.2. 5 equivalent, then α ∧ ¬α ` β ∧ ¬β, for any α and β. Hence, by elimination of conjunction, α ∧ ¬α ` β. So, if a logic is paraconsistent, then it has some pairs of non-equivalent contradictions. This fact fits the idea that in real-life contexts of reasoning some contradictions are more relevant than others. Thus, it is natural to devise a connective that is able to distinguish between different kinds of contradictions – and this is precisely the feature of da Costa's approach that has led to the introduction of LFIs. At first glance, it may seem that the consistency operator of LFIs and the well-behavedness operator of da Costa's Cn hierarchy (recall that α◦ means that α is well-behaved) are the same thing when applied to a proposition α. This view, however, is mistaken. LFIs are a generalization of da Costa's idea of expressing the meta-logical notion of consistency inside the object language. Even though the logics of Cn hierarchy (for 1 ≤ n < ω) end up being a special case of LFIs, an important point distinguishes LFIs from da Costa's Cn. In the latter, as we have just seen, α◦ is an abbreviation of ¬(α∧¬α), while in LFIs the unary connective ◦ may be primitive and logically independent from non-contradiction. So, in some LFIs, the equivalence between ◦α and ¬(α ∧ ¬α) does not hold.3 2.2 'Duality' in da Costa's logics We now turn to the role of the duality between paraconsistent and intuitionistic logics in da Costa's Cn hierarchy. Although the central feature of paraconsistent logics is the invalidity of the principle of explosion, da Costa in [17] and [18], emphasizes the invalidity of the principle of non-contradiction and takes a path longer than would be necessary to recover classical logic. Let us restrict ourselves to C1, what is enough to establish our point. In C1 (see Definition 2), classical logic is recovered for well-behaved formulas by means of the following axiom: α◦ → ((β → α)→ ((β → ¬α)→ ¬β)) 3The operator ◦ as a primitive operator, not definable in terms of non-contradiction, appears for the first time in Carnielli and Marcos [9], where the logics of formal inconsistency (LFIs) have been introduced. For more precise historical details, LFIs appeared for the first time in the II World Congress on Paraconsistency, held in Juquehy, SP, Brazil, in May, 2000, dedicated to the 70th birthday of Newton da Costa. 'A taxonomy of C-systems' [9], was published in the proceedings of this event. 6 where α◦ is defined as ¬(α ∧ ¬α) and means that α is 'well-behaved'. Since the emphasis is put on the invalidity of non-contradiction, explosion is recovered through an unnecessary roundabout.4 On the other hand, in LFIs the principle of explosion is recovered directly, by the axiom ◦α→ (α→ (¬α→ β)) or an equivalent inference rule. Thus, the emphasis is not on the principle of non-contradiction, but rather on the principle of explosion, i.e. on an inference that concludes anything from a contradiction. It seems to us that what impelled da Costa in placing the emphasis on non-contradiction was a misunderstanding of the nature of the duality between paraconsistent and intuitionistic logics. Indeed, if we take a look at how da Costa devises C1, the first logic of his Cn hierarchy (see Definition 2), it is not difficult to see that there is a sort of 'duality' between C1 and intuitionistic logic. Let us consider the formulas below: (i) ¬(α ∧ ¬α), (ii) α→ ¬¬α, (iii) α ∨ ¬α, (iv) ¬¬α→ α. Formulas (i) and (ii), non-contradiction and double negation introduction, hold in intuitionistic logic but do not hold in C1. On the other hand, formulas (iii) and (iv), excluded middle and double negation elimination, thought by da Costa to be a kind of 'dual' to (i) and (ii), hold in C1 but do not hold in intuitionistic logic.5 In [17, p. 9], he presents an argument to justify the validity of (iv) as an axiom of C1 that runs as follows.6 4Suppose α◦, α and ¬α. So, ¬β → α and ¬β → ¬α. From the axiom above we get ¬¬β. Since double negation elimination holds, we obtain β. 5Actually, the invalidity of the principle of non-contradiction is not an essential feature of paraconsistent logics. An example of a paraconsistent logic where explosion does not hold but non-contradiction is a valid formula is the logic of paradox (see [33]). 6In the original [17, p. 9]: "ou A é 'bem comportada', no sentido de que não são simultaneamente verdadeiras A e ¬A, sendo, então, de se esperar que se aplique a lógica clássica, donde ¬¬A→ A; ou A é 'mal comportada' e tem-se A e ¬A, advindo que qualquer proposição deve implicar A e, em particular, que ¬¬A→ A". 7 Either α is well-behaved, in the sense that α and ¬α do not hold simultaneously, or α is not well-behaved. (i) Suppose α is well-behaved. In this case, da Costa claims that 'classical logic may be applied', which means, as far as we can see, that classical reasoning holds for α. So, ¬¬α → α. Let us make clear what is going on in this step of the argument: classical reasoning holds for α; in classical reasoning, ¬¬α implies α; therefore, ¬¬α→ α holds. Notice that this argument holds in the metatheory. (ii) Now, suppose α is not well-behaved and both α and ¬α hold. So, anything implies α, in particular ¬¬α→ α. This step of the argument is not metatheorical but holds in the object language, since α→ (β → α) is an axiom in C1. It seems, however, that an analogous argument would also justify α→ ¬¬α. Either ¬¬α is well-behaved or it is not. (i) Suppose ¬¬α is wellbehaved and classical reasoning holds for ¬¬α. So, since α implies ¬¬α in classical logic, α → ¬¬α should hold. (ii) Suppose, on the other hand, that ¬¬α is not well-behaved, and both ¬¬α and ¬¬¬α hold. As above, any proposition implies ¬¬α, in particular α→ ¬¬α. The central point here is step (i) of both arguments. If classical logic holds for α, and the fact that ¬¬α implies α in classical logic is sufficient to conclude that ¬¬α → α holds, then, when classical logic holds for ¬¬α, the fact that α implies ¬¬α in classical logic should be sufficient to conclude that α→ ¬¬α holds. Our conclusion, therefore, is that da Costa's argument does not justify the validity of double negation elimination in C1. It is worth noting that, moreover, rejecting (ii) is strange because its invalidity does not fit with da Costa's claim in [17] that in C1 as many schemas and rules of classical logic as possible should be valid. In fact, double negation introduction can be added to C1 without affecting its paraconsistent properties. Let us call the system so obtained C ′1. An adequate semantics for C ′1 is obtained just by adding the clause v(α) = 1 =⇒ v(¬¬α) = 1 to the semantics presented in [20] and [30]. Clearly, such semantics does not validate explosion, and it can easily be proved that C ′1 has no trivial models. The paraconsistent logic C¬¬1 , stronger than C ′1, has been presented in [4]. C¬¬1 is obtained by adding to C1 double negation introduction plus the 8 axiom ¬(¬α ∧ α) → ¬(α ∧ ¬α). The paraconsistent negation of C¬¬1 is still closer to classical negation. So, da Costa's claim that C1 should contain 'the maximum possible number of schemes and deduction rules of the classical calculus' [17, p. 7] is not really pursued by him. In the original presentation of C1, it already seems clear that the main motivation for adopting the formulas (iii) and (iv), and rejecting (i) and (ii), was to establish a 'duality' with intuitionistic logic. But a conclusive piece of evidence for the above claim can be found in [21] where da Costa and Marconi present the hierarchy of propositional paracomplete logics Pn. There, we read: [in this paper] we describe a hierarchy of paracomplete logics and mention the possibility of extending it to others [i.e. to some paracomplete predicate calculi, [21, p. 508]] which are, in a certain sense, "dual" of the hierarchies [presented in [17], [18] et al. – i.e. Cn]. The first logic of the Pn hierarchy is P1, obtained by adding to classical positive logic CPL+ (see Definition 14 below) the following axioms (α∗ is defined as α ∨ ¬α): 1. α∗ → ((α→ β)→ ((α→ ¬β)→ ¬α)), 2. (α∗ ∧ β∗)→ [(α ∧ β)∗ ∧ (α ∨ β)∗ ∧ (α→ β)∗ ∧ ¬α∗], 3. ¬(α ∧ ¬α), 4. α→ (¬α→ β), 5. α→ ¬¬α. Marconi and da Costa do not explain exactly why Cn and Pn are "in a certain sense dual" to each other. There is no precise characterization of duality between logics in that paper, nor in [17], [18] and [19].7 P1 has axioms 3 and 5 above, precisely the formulas (i) and (ii) whose 'dual' formulas have been adopted in C1. So, it is clear that da Costa erroneously conceived the duality 7Although da Costa says in [19] p. 29 that "a hierarchy of paracomplete logics was introduced [in [21]], that are «dual», in a precise sense, of some paraconsistent logics studied in [see [17] and [18]]", we have not found an explanation of the duality between the logics of Cn and Pn hierarchies. 9 between paraconsistency and paracompleteness as a duality between noncontradiction and excluded middle as formulas, and not between explosion and excluded middle as rules of inference. Notice also that axiom 4, the principle of explosion, had to be added to the system, together with 3 and 5, which is not surprising, since non-contradiction and explosion are logically independent (regarding Pn hierarchy, see also Remark 19 below). Indeed, there is a duality between paraconsistent and paracomplete (so, intuitionistic) logics that gives some interesting insights and provides philosophical motivations for both (see [12]). But the central point is not that the logics are dual, nor that the formulas excluded middle and non-contradiction are dual. The point is that excluded middle and explosion are dual inferences. In the next section we will take a closer look at this point and show, based on the duality between paraconsistency and paracompleteness, how the idea of internalizing metatheoretical notions in the object language may be further developed. 3 Duality and recovery operators in LFIs and LFUs We begin by defining duality between connectives in classical logic. Definition 4 Two n-ary logical connectives κ1 and κ2 are said to be dual if ∼κ1(α1, ..., αn) and κ2(∼α1, ...,∼αn) are materially equivalent, where ∼ is classical negation. Thus, classical negation ∼ is the dual of itself and ∧ and ∨ are dual of each other. The idea of duality may also be applied to inference rules. But in order to do that we have to move to sequent calculus and multiple-conclusion logic. The symmetry displayed by the rules of Gentzen's sequent calculus LK [23] is well known. Gentzen remarks that: If [the rules] →-IS and →-IA are excluded, the calculus LK is dual in the following sense: If we reverse all sequents of an LK derivation (in which the →-symbol does not occur), i.e., if for α1...αm ⇒ β1...βn we put β1...βn ⇒ α1...αm, and if we exchange, in inference figures with two upper sequents, the rightand lefthand upper sequents, including their derivations, and also replace every occurrence of ∧ by ∨, ∀ by ∃, ∨ by ∧, and ∃ by ∀ (in the case 10 of ∧ and ∨ we also have to interchange the respective scopes of the symbols, e.g., for β∨α we have to put α∧β, then another LK derivation results. This can be seen at once from the schemata. (Special care was taken to arrange them in such a way as to bring out their symmetry.) (Cf. H.-A.'s duality principle, p. 62.) [23, p. 86]. Except for the implication rules R→ and L→, all the other rules, including the structural ones, have dual in LK. So, we may define: Definition 5 Two sequent calculi rules R1 and R2 are dual if one is obtained from the other as follows: 1. For each one of the premises, and for the conclusion, put the succedent in the place of the antecedent and vice-versa – i.e. change each α1...αm ⇒ β1...βn with β1...βn ⇒ α1...αm; 2. Change the connective of the main formula of the rule with its dual. Gentzen is also concerned with the order of the formulas, but this does not matter when we work with multisets. An R∗ rule, yields an L∗d rule (and vice-versa), with ∗d being the connective dual of ∗. The rules R∨ and L∧ are dual to each other, as well as the rules L∨ and R∧. R¬ is the dual of L¬, and vice-versa. The right rules of weakening, contraction and interchange are dual of the corresponding left rules (and vice-versa), and cut is the dual of itself. Even the axiom, α ⇒ α, considered as a rule from no premise, is the dual of itself. So, the sense in which Gentzen says that the system LK is 'dual' is that it has dual inference rules. Remark 6 The basic idea of multiple-conclusion logic appeared for the first time in 1935 (see Gentzen [23]). Indeed, multiple-conclusion framework is suitable for expressing duality between both rules and connectives, but this is because multiple-conclusion is already duality. Dealing with premises and conclusions in an uniform way, as multiple-conclusion does, also allows us to deal uniformly with truth and falsehood: from the point of view of the preservation of truth, an argument goes from premises to conclusion, but from the point of view of the preservation of falsity, an argument goes the other way, from conclusion to premises. Since multiple-conclusion considers sets of premises and sets of conclusions, it acquires a symmetry that is missing in 11 the single-conclusion logic. The intuitive, pretheoretical idea of logical consequence is expressed, in multiple-conclusion, in terms of sets: Γ ∆ holds when it is not possible that the propositions in Γ are true and the propositions in ∆ are false. So, if all propositions in Γ are true, some proposition in ∆ is true, and if all propositions in ∆ are false, some proposition in Γ is false. But in the latter formulation the duality between the quantifiers all and some, and also between conjunction and disjunction, is already present. It is worth noting that Gentzen in 1935 [23, see quotation above] says that "Special care was taken to arrange them [the sequent rules of LK] in such a way as to bring out their symmetry" and immediately mentions the principle of duality presented in the first edition (1928) of Hilbert and Ackermann's book Grundzüge der Theoretischen Logik. We do not have access to the first edition of this book, but in [27, §5, p. 16] (translation of the second edition, 1938) such principle reads: "From a formula α ↔ β which is logically true, and both of whose sides are formed from elementary sentences and their negations by conjunction and disjunction only, there results another true equation by the interchange of ∧ and ∨". Such principle shows, for example, that the formulas α∨(β∧γ)↔ (α∨β)∧(α∨γ) and α∧(β∨γ)↔ (α∧β)∨(α∧γ) are dual to each other and logically true. It is clear then, that Hilbert and Ackermann's principle of duality (1928) already had the basic idea of Gentzen's sequent calculus LK (1935) and, moreover, this fact is acknowledged by Gentzen. Now, consider the negation rules of LK : Γ⇒ ∆, α ¬α,Γ⇒ ∆ L¬, Γ, α⇒ ∆ Γ⇒ ¬α,∆ R¬. Together, they characterize classical negation: in just one step from the axiom, L¬ and R¬ yield the following sequents α,¬α⇒ and ⇒ α,¬α which means that one and at most one between α and ¬α holds. The rules L¬ and R¬, respectively, are equivalent to explosion and excluded middle in the sense that a system equivalent to LK can be defined by adding to the positive fragment of LK the rules below, Γ, α,¬α⇒ ∆ EXP Γ⇒ α,¬α,∆ PEM. Let us call LK ′ the positive fragment of LK plus PEM and EXP. In LK ′, L¬ is obtained by EXP and one application of cut, and R¬ is obtained by 12 PEM and one application of cut. EXP and PEM are proved in LK by one application, respectively, of L¬ and R¬. We prefer to call EXP and PEM rules with zero premises, rather than axioms, in order to emphasize that EXP works like a negation-left rule and PEM like a negation-right rule. These rules are 'mirror images' of each other and express the fact that, classically, anything follows from α ∧ ¬α, and α ∨ ¬α follows from anything. There are two points about Definition 5 that we want to call attention to. First, given a certain connective, it provides the dual of that connective and the rule that governs it. Second, it provides a general criterion that establishes the duality between connectives and rules that may belong to different logics. In a paraconsistent logic, the principle of explosion does not hold in general. In an LFI, EXP holds only for 'consistent' propositions, i.e. Γ, ◦α, α,¬α⇒ ∆ EXP ◦. EXP ◦ says that if a proposition α is marked as consistent, there can be no contradiction w.r.t. α, on pain of triviality. Now, according to Definition 5, EXP ◦ can be dualized obtaining the rule: Γ⇒ 8α, α,¬α,∆ PEM 8. Notice that by dualizing the rule EXP ◦ we obtain not only the connective 8, the dual of ◦, but also a paracomplete negation that is the dual of the original paraconsistent negation (see Proposition 40 below). This is because ◦ and 8 'work together' with their respective negations (see Section 4.5). Let us take a look at the undeterminedness connective 8. If both α and ¬α do not hold, then 8α holds. 8α thus means that α is undetermined. Now, a recovery operator of determinedness 9 may be obtained from 8 if we look at 9α as the classical negation of 8α, and this is very plausible, since from the metatheoretical viewpoint, a proposition α is either determined or undetermined, and not both (we return to this point below), that is: Γ, 9α⇒ α,¬α,∆ PEM 9. The rule PEM9 recovers the validity of excluded middle for formulas we call determined. Notice that the operator 9, in turn, is the dual of an inconsistency operator •, given by the following rule: Γ, α,¬α⇒ •α,∆ EXP •. 13 The four rules EXP •, PEM9, EXP ◦ and PEM8 above (together with the positive fragment of LK ) are provably equivalent to the more convenient rules (proofs left to the reader), as follows: ◦α,Γ⇒ ∆, α ◦α,¬α,Γ⇒ ∆ L¬ ◦ Γ, α⇒ 8α,∆ Γ⇒ ¬α, 8α,∆ R¬ 8 Γ⇒ ∆, α, •α ¬α,Γ⇒ •α,∆ L¬ • Γ, 9α, α⇒ ∆ 9α,Γ⇒ ¬α,∆ R¬ 9 The operators 9 and ◦ are recovery operators in the sense that they recover a logical property (respectively excluded middle and explosion) for a proposition in their scope. From an intuitive and metatheorical viewpoint, the connectives ◦ and •, that represent respectively consistency and inconsistency, behave classically w.r.t. each other in the sense that 'α is inconsistent iff it is not the case that α is consistent'. Analogous reasoning applies to the connectives 9 and 8: 'α is undetermined iff it is not the case that α is determined'. Of course, it is presupposed that the metalogical notions that are being expressed in the object language are such that, given a proposition α, one and at most one among ◦α and •α holds (mutatis mutandis for 9α and 8α). So, if classical negation is available, we may define •α as the classical negation of ◦α, and 8α as the classical negation of 9α (see Section 4.3.1 below). 4 The systems mbC, mbD, mbCD and mbCDE This section reviews the logicsmbC andmbCD proposed respectively in [9] and [11], and introduces their new variants mbD and mbCDE. We begin by defining the languages to be used in the remainder of this paper. Besides the signatures Σ+ and ΣC (Definitions 1 and 2), the following propositional signatures will be employed: Definition 7 (Additional signatures) 14 Σ◦ = {∧,∨,→,¬, ◦} Σ9 = {∧,∨,→,¬, 9} Σ~ = {∧,∨,→,¬,~} Σ◦9 = {∧,∨,→,¬, ◦, 9} where ◦, 9 and ~ are unary connectives. 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. Let us recall from [35] the following useful notions: Definition 8 (Tarskian logics) Let L = 〈For,`〉 be a logic defined over a set of formulas For, which has a consequence relation `. (1) L is said to be Tarskian if it satisfies the following properties, for every Γ ∪∆ ∪ {α} ⊆ For: (P1) if α ∈ Γ then Γ ` α (Reflexivity); (P2) if Γ ` α and Γ ⊆ ∆ then ∆ ` α (Monotonicity); (P3) if ∆ ` α and Γ ` β for every β ∈ ∆ then Γ ` α (Cut). (2) L is said to be finitary if it satisfies the following: (P4) if Γ ` α then there exists a finite subset Γ0 of Γ such that Γ0 ` α. (3) L is said to be structural if For = For(Θ) for a propositional signature Θ such that the following property holds: (P5) if Γ ` α then σ[Γ] ` σ(α), for every substitution σ of formulas for variables. As mentioned above, LFIs are paraconsistent logics enriched with a primitive or defined consistency connective ◦ which allows recovering from the explosion in a 'controlled way'. Formally: 15 Definition 9 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 a Logic of Formal Inconsistency (LFI) 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 β. Note that condition (ii) of the definition of LFIs is required in order to satisfy condition (iii) in a non-trivial way. Remark 10 The definition of an LFI presented above, in which consistency is defined by means of a single connective (Definition 9 above), is a simplified version of the general definition of LFIs. In the general case, consistency can be defined by means of a nonempty set of formulas (see [8, p. 21] and [7, p. 31-33]). However, Definition 9, although characterizing a particular case of LFIs as defined in [9] (see also [8]), comprises all the logics studied in [8] and [7], and also the logics called C-systems [9]. Actually, our definition of LFI here is closer to the definition of C-system [8, p. 23]. It is worth noting that the LFUs defined below, analogously, could be called D-systems. The basic idea of LFIs may be extended: excluded middle may be recovered in paracomplete logics analogously to the way in which explosion is recovered in LFIs. Definition 11 Let L = 〈Θ,`〉 be a Tarskian, finitary and structural logic defined over a propositional signature Θ, which contains a negation ¬. Assume that L has a (primitive or defined) disjunction ∨ which enjoys the standard property, namely: for every set of formulas Γ∪{α, β}, Cn(Γ∪{α})∩Cn(Γ∪ {β}) = Cn(Γ ∪ {α ∨ β}), where Cn(∆) def= {γ : ∆ ` γ}, for every ∆. Let 9 be a (primitive or defined) unary connective in Θ. Then, L is said to be a Logic of Formal Undeterminedness (LFU) with respect to ¬ and 9 if the following holds: 16 (i) 0 α ∨ ¬α for some α; (ii) there is a formula α such that (ii.a) 9α 0 α; (ii.b) 9α 0 ¬α; (iii) 9α ` α ∨ ¬α for every α. If ∨ and ∨′ are two disjunctions in L then α ∨ β and α ∨′ β are interderivable, for every α and β. Thus, the definition of LFUs does not depend on a particular choice of a (standard) disjunction in L. On the other hand, condition (ii) is required in order to satisfy condition (iii) in a non-trivial way. Notice, however, that disjunctions in Definition 11 could be completely dispensed with, had we defined LFUs in the framework of multiple-conclusion logics. Remark 12 The concept of Logics of Formal Undeterminedness has been introduced by Marcos in [31], but the idea of recovering excluded middle analogously to how non-contradiction and explosion are recovered in Cn and LFIs, as we have seen in Section 2.2, can be traced back to da Costa and Marconi in [21]. Carnielli and Rodrigues in [12] presented a conceptual approach to the duality, arguing that from an epistemic viewpoint paracomplete and paraconsistent logics may be understood, respectively, as dealing with a notion stronger and weaker than truth. Some ideas presented by Marcos in [31] matches our interest in the duality between paraconsistency and paracompleteness, and we have tried to develop these ideas further in this paper However, Marcos approaches the duality from a different viewpoint to ours: he is concerned with paracomplete and paraconsistent negations defined in modal terms, respectively, as _α def= 2∼α and ^α def= 3∼α [31, p. 292]. We have adopted the same symbols for consistency, inconsistency, determinedness and undeterminedness connectives (respectively, ◦, •, 9 and 8) [31, p. 290], but we do not define them in terms of other connectives because we are interested mainly in ◦ and 9 as primitive recovery operators. As an aside, it seems strange to us, though, why Marcos defines undeterminedness, 8α as α ∨_α, since determinedness, 9α, should be so defined. Now, we combine the features of LFIs and LFUs to define a class of paracomplete and paraconsistent logics in which explosion and excluded middle may be recovered, at once or one at a time. 17 Definition 13 Let L = 〈Θ,`〉 be a Tarskian, finitary and structural logic defined over a propositional signature Θ, which contains a negation ¬. Assume that L has a (primitive or defined) disjunction ∨ which is standard in the sense of Definition 11. Let 9 and ◦ be two (primitive or defined, possibly equal) unary connectives. Then, L is said to be a Logic of Formal Inconsistency and Undeterminedness (LFIU) with respect to ¬, 9 and ◦ if the following holds:8 (i) α,¬α 0 β for some α and β; (ii) 0 α ∨ ¬α for some α; (iii) there is a formula α such that (iii.a) 9α 0 α; (iii.b) 9α 0 ¬α; (iv) there are two formulas α and β such that (iv.a) ◦α, α 0 β; (iv.b) ◦α,¬α 0 β; (v) For every formula α and β: (v.a) 9α ` α ∨ ¬α; (v.b) ◦α, α,¬α ` β. If L is an LFIU such that 9α and ◦α are interderivable for every formula α (and in particular if 9 = ◦), then L is said to be a strict LFIU. As in the case of LFUs, the definition of LFIUs does not depend on a particular choice of standard disjunction in L. On the other hand, conditions (iii) and (iv) are required in order to satisfy condition (v) in a non-trivial way. Now, we define the basic LFIs, LFUs and LFIUs as extensions of classical positive logic. Following the usual presentation of LFIs, these systems will be introduced by means of Hilbert calculi (below each one of these logics L will be reintroduced by means of a sequent calculus LS). 8Logic systems with a negation simultaneously paraconsistent and paracomplete are called paranormal by some authors. 18 Definition 14 (Classical Positive Logic) The classical positive logic CPL+, defined over the language For(Σ+), is obtained from intuitionistic positive logic IPL+ (Definition 1) by adding the following axiom:( α→ β ) ∨ α (AX9 ) Definition 15 (Paraconsistent logic mbC) The logicmbC, defined over the language For(Σ◦), is obtained from CPL+ by adding the following (see [9]): α ∨ ¬α (AxPEM ) ◦α→ ( α→ ( ¬α→ β )) (GEXP) As is well-known, the logic mbC is an LFI. It is paraconsistent and the unary operator ◦ recovers explosion by means of the axiom GEXP (also called 'gentle explosion principle', tantamount here to EXP ◦). We now define a paracomplete logic where the operator 9 recovers the excluded middle by means of the axiom GPEM ('gentle excluded middle', tantamount here to PEM9). Definition 16 (The paracomplete logic mbD) The logic mbD, defined over the language For(Σ9), is obtained from CPL+ by adding the following: 9α→ ( α ∨ ¬α ) (GPEM ) α→ ( ¬α→ β ) (AxEXP) Both properties of negation can be recovered simultaneously in a paracomplete and paraconsistent system which combines the previous ones: Definition 17 (Paraconsistent and paracomplete logic mbCD) The logicmbCD, defined over the language For(Σ~), is obtained from CPL+ by adding the following (see [11]): ~α→ ( α ∨ ¬α ) (GPEM ) ~α→ ( α→ ( ¬α→ β )) (GEXP) 19 The logic mbCD is a strict LFIU based on CPL+, in which ~ can be seen as a classicality operator, where ~α indicates that α behaves classically, and so α obeys the laws of classical logic. Of course, the two properties of classical negation mentioned in Definition 17 could be recovered separately by means of a specific connective, that is, by means of a non-strict LFIU. This motivates the following: Definition 18 (Paraconsistent and paracomplete logic mbCDE) The logic mbCDE, defined over the language For(Σ◦9), is obtained from CPL+ by adding the following: 9α→ ( α ∨ ¬α ) (GPEM ) ◦α→ ( α→ ( ¬α→ β )) (GEXP) Remark 19 In 1986 da Costa and Marconi introduced in [21] a hierarchy Pn (for 1 ≤ n < ω) of paracomplete logics intended to be 'dual' to the hierarchy Cn (for 1 ≤ n < ω) of paraconsistent logics (see Section 2, p. 9 above). Notice that this approach is analogous to mbD, and P1 and mbD have the same relationship that holds between C1 and mbC. Additionally, in 1989 da Costa proposed in [19] a hierarchy Nn (for 1 ≤ n < ω) of paraconsistent and paracomplete logics based on CPL+, called 'nonalethic', intended to simultaneously generalize the hierarchies Cn and Pn. The system N1, the first logic of the Nn hierarchy, has some analogy with the system mbCDE. In [19], the system obtained from N1 by adding the axiom schema α◦ is P1; the system obtained from N1 by adding the axiom schema α∗ is C1; and the system obtained from N1 by simultaneously adding the axiom schemas α◦ and α∗ is CPL. These features are analogous to the ones described for mbCDE in Remark 37 below. We could say that the relationship between N1 and mbCDE is the same as the one between C1 and mbC and the one between P1 and mbD. Now, in order to emphasize the duality between their connectives and rules, the same logics will be presented by means of sequent calculi. The equivalence between both presentations will be obtained in Corollary 32 below. 20 Definition 20 (Sequent calculus for Classical Positive Logic) Let CPL+S be the sequent calculus for classical positive propositional logic CPL+ defined over the language For(Σ+) by the following rules: α⇒ α Axiom Γ⇒ ∆ α,Γ⇒ ∆ L-Weak Γ⇒ ∆ Γ⇒ ∆, α R-Weak α, α,Γ⇒ ∆ α,Γ⇒ ∆ L-Cont Γ⇒ α, α,∆ Γ⇒ ∆, α R-Cont α, β,Γ⇒ ∆ α ∧ β,Γ⇒ ∆ L∧ Γ⇒ α,∆ Γ⇒ β,∆ Γ⇒ α ∧ β,∆ R∧ Γ, α⇒ ∆ Γ, β ⇒ ∆ Γ, α ∨ β ⇒ ∆ L∨ Γ⇒ α, β,∆ Γ⇒ α ∨ β,∆ R∨ Γ⇒ ∆, α β,Γ⇒ ∆ α→ β,Γ⇒ ∆ L→ Γ, α⇒ β,∆ Γ⇒ α→ β,∆ R→ Γ⇒ A,∆ Γ′, A⇒ ∆′ Γ,Γ′ ⇒ ∆′,∆ Cut ConcerningmbC the following calculus was proposed by T. Rodrigues in [34]: Definition 21 (Sequent calculus for mbC) LetmbCS be the sequent calculus for mbC over the language For(Σ◦) defined by adding to CPL+S the following rules: ◦α,Γ⇒ ∆, α ◦α,¬α,Γ⇒ ∆ L¬ ◦ Γ, α⇒ ∆ Γ⇒ ¬α,∆ R¬ Note that the rules L¬◦ and R¬ correspond to the axiomsGEXP and AxPEM of Definition 15, respectively. 21 Definition 22 (Sequent calculus for mbD) LetmbDS be the sequent calculus for mbD over the language For(Σ9) defined by adding to CPL+S the following rules: Γ⇒ ∆, α ¬α,Γ⇒ ∆ L¬ Γ, 9α, α⇒ ∆ 9α,Γ⇒ ¬α,∆ R¬ 9 Note that the rules L¬ and R¬9 correspond to the axioms AxEXP and GPEM of Definition 16, respectively. Definition 23 (Sequent calculus for mbCD) LetmbCDS be the sequent calculus for mbCD defined over the language For(Σ~) defined by adding to CPL+S the following rules: ~α,Γ⇒ ∆, α ~α,¬α,Γ⇒ ∆ L¬ ~ Γ,~α, α⇒ ∆ ~α,Γ⇒ ¬α,∆ R¬ ~ Definition 24 (Sequent calculus for mbCDE) Let mbCDES be the sequent calculus for mbCDE defined over the language For(Σ◦9) defined by adding to CPL+S the following rules: ◦α,Γ⇒ ∆, α ◦α,¬α,Γ⇒ ∆ L¬ ◦ Γ, 9α, α⇒ ∆ 9α,Γ⇒ ¬α,∆ R¬ 9 In order to deal with similar logics in an homogeneous way, we now define the following collections of formal systems: Definition 25 L def= { mbC,mbD,mbCD,mbCDE } LS def = { mbCS,mbDS,mbCDS,mbCDES } L+ def= { CPL+,mbC,mbD,mbCD,mbCDE } L+S def = { CPL+S ,mbCS,mbDS,mbCDS,mbCDES } . Note that each L in L (resp. in L+) has a corresponding element LS in LS (resp. in L+S ). 22 4.1 Valuation semantics As was done with several LFIs, in particular withmbC (see [8, 7]), valuation semantics over { 0, 1 } are now defined so as to characterize the formal systems presented in the previous section. Definition 26 (Valuations) (1) A function v : For(Σ+)→ { 0, 1 } is a valuation for CPL+ and CPL+S if it satisfies the following: (vAnd) v(α ∧ β) = 1 ⇐⇒ v(α) = 1 and v(β) = 1 (vOr) v(α ∨ β) = 1 ⇐⇒ v(α) = 1 or v(β) = 1 (vImp) v(α→ β) = 1 ⇐⇒ v(α) = 0 or v(β) = 1 (2) A function v : For(Σ◦) → { 0, 1 } is a valuation for mbC and mbCS if it satisfies the clauses for a CPL+-valuation, plus the following: (vNeg) v(¬α) = 0 =⇒ v(α) = 1 (vCon) v(◦α) = 1 =⇒ ( v(α) = 0 or v(¬α) = 0 ) . (3) A function v : For(Σ9)→ { 0, 1 } is a valuation for mbD and mbDS, if it satisfies the clauses for a CPL+-valuation, plus the following: (vNegD) v(¬α) = 1 =⇒ v(α) = 0 (vConD) v(9α) = 1 =⇒ ( v(α) = 1 or v(¬α) = 1 ) . (4) A function v : For(Σ~)→ { 0, 1 } is a valuation formbCD andmbCDS, if it satisfies the clauses for a CPL+-valuation, plus the following: (vConCD) v(~α) = 1 =⇒ ( v(α) = 1 iff v(¬α) = 0 ) . (5) A function v : For(Σ◦9) → { 0, 1 } is a valuation for mbCDE and mbCDES, if it satisfies the clauses for a CPL+-valuation, plus the following: (vConD) v(9α) = 1 =⇒ ( v(α) = 1 or v(¬α) = 1 ) (vCon) v(◦α) = 1 =⇒ ( v(α) = 0 or v(¬α) = 0 ) . For every logic L ∈ L+ ∪ L+S (recall Definition 25) let `L and L be the consequence relation of L w.r.t. derivations (in the corresponding calculus) and w.r.t. its valuations, respectively. As specified in Definition 26, L = LS 23 for every L ∈ L+. To give a uniform treatment in the framework of Tarskian logics, we define: Γ `LS φ iff the sequent Γ ⇒ φ is derivable in the sequent calculus LS. Theorem 27 (Soundness) Let L ∈ L+ ∪ L+S . For every set Γ ∪ {φ} of formulas of L: Γ `L φ implies Γ L φ. Proof. Straightforward. 2 As an immediate application of the soundness for each L, it is easy to prove the following: Proposition 28 (1) The logic mbD (resp. mbDS) is an LFU. (2) The logic mbCD (resp. mbCDS) is a strict LFIU. (3) The logic mbCDE (resp. mbCDES) is a non-strict LFIU. Proof. (1) Let p be a propositional variable, and consider a valuation v for mbD and mbDS such that v(p) = v(¬p) = 0. From this, 6|=mbD p ∨ ¬p and so 0mbD p∨¬p and 0mbDS p∨¬p, by soundness. Now, let v′ be a valuation for mbD such that v′(p) = 0 and v′(9p) = v′(¬p) = 1. Then 9p 6|=mbD p and so 9p 6`mbD p and 9p 6`mbDS p, by soundness. Analogously it is shown that 9p 6`mbD ¬p and 9p 6`mbDD ¬p. Finally, condition (iii) of Definition 11 follows by axiom (GPEM ) and (MP) (in the case of mbD) and from PEM9 that, as we have seen in Section 3, holds in mbDS. Items (2) and (3): the proof is analogous, and is left to the reader. 2 In order to prove completeness, first it is necessary to recall some notions. A set of formulas Γ of a (Tarskian) logic L is maximal relative to a formula α in L if Γ 0L α, but Γ, β `L α whenever β 6∈ Γ. If Γ is maximal relative to α in L then it is a closed theory in L, that is: Γ `L β iff β ∈ Γ, for every formula β. Recall the following classical result: Theorem 29 (Lindenbaum-Łos) Let L be a Tarskian and finitary logic over a language For, and let Γ ∪ {α} ⊆ For such that Γ 0L α. Then there exists a set ∆ such that Γ ⊆ ∆ ⊆ For and ∆ is maximal relative to α in L. Proof. See [35, Theorem 22.2]. 2 The proof of the following result is straightforward: 24 Proposition 30 Let L ∈ L+∪L+S , and let Γ be a set of formulas of L which is maximal relative to a formula φ of L. Let α and β be formulas of L. Then: (1) α ∧ β ∈ Γ iff α ∈ Γ and β ∈ Γ. (2) α ∨ β ∈ Γ iff α ∈ Γ or β ∈ Γ. (3) α→ β ∈ Γ iff α 6∈ Γ or β ∈ Γ. (4) If L = mbC then: (4.1) If ¬α 6∈ Γ then α ∈ Γ. (4.2) If ◦α ∈ Γ then ¬α 6∈ Γ or α 6∈ Γ. (5) If L = mbD then: (5.1) If ¬α ∈ Γ then α 6∈ Γ. (5.2) If 9α ∈ Γ then ¬α ∈ Γ or α ∈ Γ. (6) If L = mbCD and ~α ∈ Γ then: ¬α ∈ Γ iff α 6∈ Γ. (7) If L = mbCDE then: (7.1) If 9α ∈ Γ then ¬α ∈ Γ or α ∈ Γ. (7.2) If ◦α ∈ Γ then ¬α 6∈ Γ or α 6∈ Γ. It is easy to see that every logic L ∈ L+ ∪ L+S is Tarskian, finitary and structural (recall Definition 8). Thus, Theorem 29 holds for all of them and so completeness follows easily: Theorem 31 (Completeness) Let L ∈ L+ ∪L+S . For every set Γ∪{φ} of formulas of L: Γ L φ implies Γ `L φ. Proof. Suppose that Γ 0L φ, and let ∆ be a set of formulas of L such that Γ ⊆ ∆ and ∆ is maximal relative to φ in L (Theorem 29). Let v be the mapping from the set of formulas of L to { 0, 1 } defined as follows: v(φ) = 1 iff φ ∈ ∆, for every φ. By using Proposition 30, it is easy to see that v is a valuation for L such that v[Γ] ⊆ {1} but v(φ) = 0. Thus Γ 2L φ. 2 Corollary 32 Let L ∈ L+. Then `L = `LS . That is, for every set Γ ∪ {φ} of formulas of L: Γ `L φ iff Γ `LS φ. 4.2 A hierarchy based on stronger notions of consistency As we have said in Section 2, up to now the idea of a hierarchy of increasingly weaker logics, proposed by da Costa, has not been as successful as 25 the introduction of an operator capable of expressing meta-logical notions in the object language. This section proposes a hierarchy of logics based on mbC, called mbCn (1 ≤ n < ω), in which consistency (i.e. the condition for recovering explosion in mbCn) gets stronger as n grows up. It might be instructive to make an analogy with tribunal systems in many countries, with their own structure for dealing with cases and appeals. As we made clear, the decision about consistency of a judgment is always performed outside the formal system, and thus it becomes determined from outside whether ◦α is true or not. This procedure may be regarded as being produced by a trial court (or a district court). However, a second, higher level court, may decide whether that mechanism is itself consistent, in the sense that it does not produce ◦α and ¬ ◦ α. If so, this court establishes that ◦(◦α) is true. So it may be that ◦α, α,¬α 0 β, while ◦◦α, ◦α, α,¬α ` β, or in general, for ◦nα = ◦(◦n−1α), ◦nα, ◦n−1α, * * * , ◦1α, α,¬α 0 β, while ◦n+1α, ◦nα, * * * , ◦1α, α,¬α ` β. The general case would correspond to a hierarchy of higher and higher level courts, which might end up in a Kafkian chain of appellation courts in the limit case – but of course, one may envisage practical situations in which two or three levels could suffice. The idea is that it should be possible to express degrees of consistency and to establish a point in which classical reasoning is restored. The simplest hierarchy may be obtained just by iterating the unary consistency operator ◦. The hierarchy mbCn is thus defined by replacing GEXP (see Definition 15) with the axiom GEXP n (iterated gentle explosion principle), ◦nα→ (◦n−1α→ * * * → (◦1α→ (α→ (¬α→ β) * * * ) (GEXP n) for each n, where ◦nα = ◦(◦n−1α). In this case, there is only one connective ◦, that may be primitive or defined. As much as for mbC, each mbCn is an LFI, and explosion is recovered by means of the axiom GEXP n. Note that we need all the premises ◦nα, ◦n−1α, * * * , ◦1α because each statement of the form ◦iβ is a guarantee that β will never be contradictory, but not that β is asserted. In other words, a statement of the form ◦β is a negative stipulation, or a clause which expressly prevents contradictions, not a positive utterance. 26 Simple iteration, although illustrative, is not the only possible way to formulate an axiomatization for mbCn. Alternatively, primitive or defined connectives ◦1, ◦2, ◦3, * * * , ◦n may be conceived independently of each other. They may express, for example, different and independent criteria that together constitute conclusive evidence for a proposition α. So, ◦1α, ◦2α, ◦3α, * * * , ◦nα are, together, a sufficient condition and each ◦iα is a necessary condition for establishing α conclusively, and the fact that the truth of α has been conclusively established is expressed by the validity of explosion w.r.t. α. In this case, the premises could be represented by a set, }α = {◦1α, ◦2α, ◦3α, * * * ◦nα}, such that for any }α′ proper subset of }α, }α′, α,¬α 0 β, while } α, α,¬α ` β. Analogous approaches may be applied to mbD and mbCD, in order to produce hierarchies of determinedness and classicality, and the swap structures semantics framework can also be adapted for those logics. Remark 33 In [15], Ciuciura presents a hierarchy of LFIs called mbCn (1 ≤ n < ω), in which the consistency operator ◦n of mbCn is given by ¬2α∧¬3α∧* * *∧¬n+1α. Thus, ◦α = ◦1α def = ¬¬α expresses the consistency operator in mbC1. Since the consistency operators ◦n are expressed in terms of the others (namely, negation ¬ and conjunction ∧), these systems are in fact dC-systems, a sub-class of LFIs as defined in [9, Subsection 3.8] (see also [8, Definition 32] and [7, Section 3.3]). The author claims that mbC1 "essentially coincides with mbC" ([15, pag. 174]). However, this is not the case: just note that adding ¬¬α → α to mbC1 yields classical logic CPL, while adding α → ¬¬α to mbC1 yields a logic which is not really paraconsistent, that is, a logic controllably explosive w.r.t. the formula schema ¬p0, i.e. ¬α,¬¬α ` β for every α and β (see [8, Definition 9]). On the other hand, it is well-known that mbC can be expanded either by ¬¬α → α, by α → ¬¬α or by both without crashing into CPL or into a controllably explosive logic. Moreover, in the abstract of [15] it is claimed that the construction of the hierarchy mbCn "makes the connective of consistency redundant". Indeed, the consistency operator in mbCn is innocuous, since it is a defined notion (as in da Costa's Cn), but in general LFIs consistency operators are by no means redundant. 27 4.3 Recovering classical logic Classical logic may be recovered in the logics of the family L (and so in the family LS) in two ways: by defining a classical negation, and by means of a derivability adjustment theorem (DAT ). 4.3.1 Defining classical negation Recall, from the discussion after Remark 6, that a classical negation, in a given sequent calculus, is a unary connective ∼ (primitive or defined) satisfying the rules EXP and PEM (resp. L∼ and R∼, see Section 3). In a Hilbert calculus, this is equivalent to saying that ∼ satisfies, respectively, the schemas AxPEM and AxEXP (see Definitions 15 and 16). Proposition 34 For L ∈ LS, a classical negation is definable in L. Proof. In mbCS and mbCDES, define: ⊥ def = ◦α ∧ (α ∧ ¬α) for any formula α. In mbCDS define: ⊥ def = ~α ∧ (α ∧ ¬α) for any formula α. In mbDS, define: ⊥ def = α ∧ ¬α for any formula α. In L ∈ LS, define ∼α def= α→ ⊥. Now, we prove that Γ⇒ ∆, α ∼α,Γ⇒ ∆ L∼ and Γ, α⇒ ∆ Γ⇒ ∼α,∆ R∼ hold in L ∈ LS. (i) L∼ holds in mbCS and mbCDES: Γ⇒ ∆, α Γ, ◦α, α,⇒ α,∆ Γ, ◦α, α,¬α⇒ ∆ L¬ ◦ Γ, ◦α ∧ α ∧ ¬α⇒ ∆ L∧ Γ,⊥ ⇒ ∆ Def⊥ α→ ⊥,Γ⇒ ∆ L→ (ii) L∼ holds in mbCDS: the proof is analogous to that given in item (i), but now using the rules for ~. (iii) L∼ holds in mbDS: 28 Γ⇒ ∆, α Γ, α,⇒ α,∆ Γ, α,¬α⇒ ∆ L¬ Γ, α ∧ ¬α⇒ ∆ L∧ Γ,⊥ ⇒ ∆ Def⊥ α→ ⊥,Γ⇒ ∆ L→ (iv) R∼ holds in L ∈ LS. Γ, α⇒ ∆ Γ, α⇒ ⊥,∆ R-Weak Γ⇒ α→ ⊥,∆ R→ So, ∼ is a classical negation in L ∈ LS by the considerations given in Section 3. 2 Remark 35 The logics here presented are said to be 'minimal' in the sense that they have minimum resources to define a classical negation inside them. This is the meaning of the 'm' in the names mbC, mbD etc. 'bC' and 'bD' mean, respectively, 'basic property of consistency' and 'basic property of determinedness'. Proposition 34 shows that all the logics studied here are able to express every classical inference, as well as having additional resources to deal with contradictory and incomplete scenarios. So, they may be seen as extensions of classical logic. From this point of view, what is accomplished by mbC, mbD, mbCD and mbCDE is nothing but adding resources to classical logic in order to deal with paraconsistent and paracomplete scenarios. Thus, although they reject some classical inferences w.r.t. inconsistent and/or undetermined propositions, in fact, they are not weaker than classical logic. 4.3.2 A derivability adjustment theorem – DAT The basic idea of Derivability Adjustment Theorems (DATs) is that we have to 'add some information' to the premises in order to restore the inferences that are lacking. DAT s are especially interesting because they show what is needed in order to restore classical consequence in non-classical contexts. It will now be shown that CPL, classical propositional logic defined over the signature ΣC (see Definition 2), can be recovered from mbD, mbCD and mbCDE by adding a suitable set of hypothesis of the form 9α, ~α, or 29 ◦α and 9β in the case, respectively, of mbD, mbCD and mbCDE. This result holds for the LFIs studied in [9, 8, 7] (including mbC). Given a set of formulas ∆ let #∆ def= {#α : α ∈ ∆}, for # ∈ {◦, 9,~}. Theorem 36 (DAT) (1) Let Γ ∪ {α} be a set of formulas in For(ΣC). Then: Γ `CPL α iff 9∆,Γ `mbD α for some ∆ ⊆ For(ΣC). (2) Let Γ ∪ {α} be a set of formulas in For(ΣC). Then: Γ `CPL α iff ~∆,Γ `mbCD α for some ∆ ⊆ For(ΣC). (3) Let Γ ∪ {α} be a set of formulas in For(ΣC). Then: Γ `CPL α iff ◦∆, 9∆′,Γ `mbCDE α for some ∆ ∪∆′ ⊆ For(ΣC). Proof. (1) Suppose that Γ `CPL α. Observe that any derivation of α from Γ in CPL can be seen as a derivation in CPL+ in which some instances of axioms (AxPEM ) and (AxEXP) are (possibly) used as additional hypothesis. Given a derivation α1 . . . αn = α of α from Γ in CPL, replace any instance αi = ( βi∨¬βi ) of (AxPEM ) by the sequence ( 9βi → ( βi∨¬βi )) 9βi ( βi∨¬βi ) . The resulting sequence of formulas is a derivation in mbD of α from Γ∪9∆, where 9∆ is the set of formulas of the form 9βi added by the process described above. Observe that every βi is in For(ΣC). Now, assume that 9∆,Γ `mbD α for some ∆ ⊆ For(ΣC). Then, by Theorem 27 it follows that 9∆,Γ |=mbD α. Let v be a valuation for CPL over ΣC such that v[Γ] ⊆ {1}, and extend v to a maping v′ : For(Σ9) → { 0, 1 } by defining v′(9β) = 1 for every β ∈ For(Σ9). Then, v′ is a valuation for mbD such that v′[Γ ∪ 9∆] ⊆ {1} and so v′(α) = 1. But v′ extends v, thus v(α) = 1. Hence, Γ |=CPL α. By completeness of CPL w.r.t. valuations it follows that Γ `CPL α. (2) 'Only if' part: it is proven analogously to item (1). However, besides processing the instances αi = ( βi∨¬βi ) of (AxPEM ) as described in item (1) (but now using the connective ~), any instance αk = ( δk → ( ¬δk → γk )) of (AxEXP) must be replaced by ( ~δk → ( δk → ( ¬δk → γk ))) ~δk ( δk →( ¬δk → γk )) , and the set ~∆ must also include occurrences of formulas of the form ~δk introduced in this way. Once again, observe that every δk is in For(ΣC). The 'If' part is proved analogously to item (1). (3) It is proved in a similar way. The details are left to the reader. 2 30 Remark 37 Theorem 36 above shows that CPL can be recovered inside any of the systems mbD, mbCD and mbCDE by adding an appropriate set of premises. Moreover, by adding 9α (resp. ~α) as a schema axiom in the case of mbD (resp. mbCD), the logic collapses to CPLe , the presentation of CPL over signature Σ9 (resp. Σ~) obtained by adding 9α (resp. ~α) as a schema axiom. In the case of mbCDE, there are three possibilities: by adding 9α as a schema axiom mbC e is obtained, a presentation of mbC over Σ◦9; by adding ◦α as a schema axiom mbDe is obtained, a presentation of mbD over Σ◦9; and finally, by adding both ◦α and 9α as schema axioms CPL◦9e is obtained, a presentation of CPL over signature Σ◦9 in which both ◦α and 9α are top particles. Compare these features of mbCDE with the ones enjoyed by da Costa's paraconsistent and paracomplete logic N1 described briefly in Remark 19. 4.4 The inconsistency and the undeterminedness operators As remarked in Section 3, the inconsistency operator • and the undeterminedness operator 8 may be defined from ◦ and 9 when a classical negation is available. So, • and 8 can be defined in mbC, mbD and mbCDE, since a classical negation is definable in these systems (see Proposition 34): •α def= ∼◦α, 8α def = ∼9α. Proposition 38 The rules below hold in mbC, mbD and mbCDE: Γ, ◦α⇒ ∆ Γ⇒ •α,∆ Γ⇒ •α,∆ Γ, ◦α⇒ ∆ Γ, 9α⇒ ∆ Γ⇒ 8α,∆ Γ⇒ 8α,∆ Γ, 9α⇒ ∆ Proof. Directly from the definitions of 8, •, and the rules L∼ and R∼. 2 Now, rules for • and 8 can be obtained from L¬◦ and R¬9: Γ⇒ ∆, α, •α ¬α,Γ⇒ •α,∆ L¬ •, Γ, α⇒ 8α,∆ Γ⇒ ¬α, 8α,∆ R¬ 8, 31 and semantic clauses for • and 8 are as follows: (vInc) ( v(α) = 1 and v(¬α) = 1 ) =⇒ v(•α) = 1, (vUnd) ( v(α) = 0 and v(¬α) = 0 ) =⇒ v(8α) = 1. The clause (vInc) says that v(•α) = 1 is only a necessary condition for v(α) = v(¬α) = 1: if the latter holds, the former has to hold. On the other hand, it may be that α is not contradictory (i.e. it is not the case that v(α) = v(¬α) = 1) but •α holds. Thus, w.r.t. α, we may say that •α means that a contradiction is permitted, while ◦α means that a contradiction is prohibited (i.e. not permited). This reading is in accordance with the fact that •α is the classical negation of ◦α, and the clause (vInc) is the contrapositive of (vCon). Analogously, the clause (vUnd) says that v(8α) = 1 is only a necessary condition for v(α) = v(¬α) = 0: it cannot be that the latter holds but v(8α) = 0. On the other hand, it may be that v(α) = 1 or v(¬α) = 1 (i.e. α ∨ ¬α holds) but v(8α) = 1 (i.e 8α still holds). Thus, w.r.t. α, we may understand 8α as meaning that undeterminedness is permitted, while 9α means that undeterminedness is prohibited (i.e. not permitted). This reading, in its turn, is in accordance with the fact that 8α is the classical negation of 9α, and the clause (vUnd) is the contrapositive of (vConD). 4.5 Back to duality The basic idea of duality for classical propositional connectives, expressed by Definition 4, is that the connectives are functions from {0, 1} to {0, 1} such that, when the inputs are inverted, the outputs are also inverted. Thus classical ∧ and ∨ are dual, because they correspond, respectively, to the following functions: ∧ = {〈1, 1, 1〉, 〈1, 0, 0〉, 〈0, 1, 0〉, 〈0, 0, 0〉} ∨ = {〈0, 0, 0〉, 〈0, 1, 1〉, 〈1, 0, 1〉, 〈1, 1, 1〉}. This idea can be extended to the non-truth-functional connectives of mbC and mbD. Let us use the symbol ¬c to refer to the negation of mbC. The paraconsistent negation ¬c is not functional, in the sense that the semantic 32 value of ¬cα is not functionally determined by the semantic value of α: when v(α) = 1, v(¬cα) may be 0 or 1. So, ¬c is represented by the relation below: ¬c = {〈0, 1〉, 〈1, 0〉, 〈1, 1〉}. The paracomplete negation ofmbD, referred to by ¬d, in turn, is represented by the relation ¬d = {〈1, 0〉, 〈0, 1〉, 〈0, 0〉}. The idea that inverted inputs yield inverted outputs is maintained, we just do not have 'truth-functionality' any more, but the connectives are represented by non-functional relations. The idea of considering truth-relations instead of truth-functions for dealing with non-truth-functional connectives can be traced back to Fidel. Indeed, Fidel, in 1977, introduced an algebraicrelational kind of structure for da Costa's systems Cn in [22] in which the paraconsistent negation is interpreted by means of relations. As far as we know, for the first time Fidel proved the decidability of the logics of Cn hierarchy. Such structures are now called Fidel structures or F-structures, after Odintsov (see [32]). As proven in [7, Chapter 6], there is a close relationship between F-structures and a semantics of multialgebras called swap structures, which will be analyzed in Section 5. The next definition formalizes these intuitions: Definition 39 Let κ1 and κ2 be n-ary connectives semantically characterized by valuation semantics over {0, 1} expressed by the (non-necessarily functional) relations R1 and R2, respectively. Let Inv be the operation over {0, 1} such that Inv(1) = 0 and Inv(0) = 1. We say that κ1 and κ2 are dual just in case: 〈x1, x2, ..., xn, y〉 ∈ R1 iff 〈Inv(x1), Inv(x2), ..., Inv(xn), Inv(y)〉 ∈ R2. Given convenient valuation semantics, the definition above allows the comparison of connectives from different logics.9 Let us take a look at the connectives ◦, 9, •, 8, in mbC and mbD. Although from the syntactic viewpoint 9As far as we know, the notion of dual connectives defined here by means of nonfunctional relations on {0, 1} has not yet been regarded in the literature. Note that the operation Inv is not applied to the relations, but rather to the elements of the n-tuples. We could define a notion of dual relation giving birth to different notions of duality between connectives. Of course, general cases of triality, quaternality or in general k-ality, can be also defined, even for n-valued logics, by using cyclic groups as in [5]. This is being investigated elsewhere. 33 these connectives are unary, they have to be represented by ternary relations, since the value of ∗α, ∗ ∈ {◦, 9, •, 8}, depends on the values of α and ¬α. So, for instance, in mbC, ◦ = {〈1, 1, 0〉, 〈1, 0, 0〉, 〈1, 0, 1〉, 〈0, 1, 0〉, 〈0, 1, 1〉}, and in mbD, 8 = {〈0, 0, 1〉, 〈0, 1, 1〉, 〈0, 1, 0〉, 〈1, 0, 1〉, 〈1, 0, 0〉}. The idea of considering triples (called snapshots) (z1, z2, z3) in which z1, z2 and z3 represent the truth-value of α, ¬α and ◦α, respectively, is the starting point of the swap-structures semantics for LFIs, to be analyzed in Section 5. Proposition 40 The following connectives are dual to each other: ◦ ofmbC and 8 of mbD; • of mbC and 9 of mbD; ¬ of mbC and ¬ of mbD. Proof. Straightforward, from Definition 39. 2 Remark 41 I. An important feature of the notion of duality as defined by Definition 39, and differently from Definition 4, is that given a connective ∗ and its dual ∗d, being ∼ classical negation, it may be that ∗α and ∼∗d∼α are not materially equivalent. Indeed, neither ◦α and ∼8∼α, nor 9α and ∼•∼α, are equivalent in mbCDE – in order to see this, consider the mbCDE-valuation v(α) = 1, v(¬α) = 0, v(∼α) = 0, v(¬∼α) = 1. In this valuation, it may be that v(◦α) = 1 and v(8∼α) = 1. In this case v(∼8∼α) = 0, and the equivalence between ◦α and ∼8∼α does not hold (mutatis mutandis for 9α and ∼•∼α). This happens because, as we have just seen above, these connectives are not functions but rather relations. So, the connectives ◦, •, 9 and 8 are not interdefinable in the sense that, for example, 9α cannot be defined as ◦∼α (the pairs ◦ and •, as well as 9 and 8 are, of course, interdefinable). II. The Square of Oppositions proposed by Marcos in [31] for the connectives ◦, •, 9 and 8 defined in modal terms (pp. 291-292) does not hold for these connectives in any of the logics studied here (note that in [31, p. 291], if 8 means undeterminedness, 9p and 8p should have their positions exchanged). In mbCDE, for example, the pairs 8α and •α 34 are not contraries, nor subcontraries, since they may simultaneously receive value 1 (or true), as well as value 0 (or false), for example, when v(α) = 1 and v(¬α) = 0 (ditto for 9α and ◦α). This is in accordance with the intuitive reading of the connectives proposed in page 32 above: ◦α, •α, 9α and 8α mean, respectively, that, w.r.t. to α, a contradiction is prohibited, a contradiction is permitted, undeterminedness is prohibited and undeterminedness is permitted. 4.5.1 Duality in mbCD and mbCDE In the logic mbCDE that contains the four connectives, all the dualities mentioned above hold, and the negation ¬ is dual to itself. The logic mbCD collapses the connectives ◦ and 9 into ~ in order to recover excluded middle and explosion at once. The classical negation of ~ in mbCD produces a connective :α def= ∼~α governed by the rules Γ⇒ ∆, :α, α ¬α,Γ⇒ :α,∆ L¬ :, Γ, α⇒ :α,∆ Γ⇒ :α,¬α,∆ R¬ :, and the associated semantic clause (vNcla) ( v(α) = 1 and v(¬α) = 1 ) or ( v(α) = 0 and v(¬α) = 0 ) =⇒ v(:α) = 1. As mentioned after Definition 17, in mbCD the connective ~ may be understood as a classicality operator. So, in mbCD, : may be interpreted as a non-classicality operator in the sense that :α is a consequence of α being either contradictory or undetermined: according to the clause vNcla, :α is a necessary condition for either v(α) = v(¬α) = 1 or v(α) = v(¬α) = 0. The connectives ~, : and the negation ¬ are represented in mbCD by the relations below: ~ = {〈1, 1, 0〉, 〈0, 0, 0〉, 〈1, 0, 0〉, 〈1, 0, 1〉, 〈0, 1, 0〉, 〈0, 1, 1〉}, : = {〈0, 0, 1〉, 〈1, 1, 1〉, 〈0, 1, 1〉, 〈0, 1, 0〉, 〈1, 0, 1〉, 〈1, 0, 0〉}, ¬ = {〈0, 1〉, 〈0, 0〉, 〈1, 0〉, 〈1, 1〉}. So, in mbCD the negation ¬ is the dual of itself, and ~ and : are dual of each other. 35 The examples presented in this section about dual connectives, represented as relations, suggest an interesting topic for future research. Moreover, the framework of Fidel structures seems to be suitable for dealing with such notions. 5 Swap structures As it is well-known, most of the LFIs studied in the literature are not algebraizable by means of the usual techniques such as the general framework of Blok and Pigozzi (see [3]). Moreover, most LFIs are not even characterizable by a single logical matrix. This justifies the search of alternative semantics for these logics, such as possible-translation semantics, Fidel structures and Nmatrices. The notion of swap structures formbC, as well as for some LFIs axiomatically extending mbC, was introduced in [7, Chapter 6]. Swap structures for LFIs are multialgebras B formed by triples (called snapshots) over a given Boolean algebra A, where each triple (z1, z2, z3) corresponds to a (complex) truth-value in which z1 represents the truth-value of a formula α, while z2 and z3 represent a possible truth-value for ¬α and ◦α, respectively. The possibilities of swap structures semantics lie beyond the scope of LFIs. For instance, in [14] and [24, Chapter 3] swap structures were defined as a semantical counterpart for some non-normal modal logics, where the snapshots are triples (z1, z2, z3) in which z1, z2 and z3 represent the truth-value of formulas α, α and ∼α, respectively. Given a swap structure B for a given logic L, it originates a non-deterministic matrix (in the sense of Avron and Lev, see for instance [1]) such that the class of such Nmatrices semantically characterizes L. In this section, this technique (which was additionally developed from the algebraic point of view in [13]) will be used in order to semantically characterize the logics mbD, mbCD and mbCDE (in the latter, snapshots will be quadruples instead of triples). Moreover, a decision procedure will be obtained for such logics from this semantics. Recall the following: Definition 42 An implicative lattice is an algebra A = 〈A,∧,∨,→〉 for Σ+ where 〈A,∧,∨〉 is a lattice such that ∨ {c ∈ A : a ∧ c ≤ b} exists for every a, b ∈ A, and → is an implication defined as follows: a→ b def= ∨ {c ∈ A : a∧ c ≤ b} for every a, b ∈ A (observe that 1 def= a→ a is the top element of 36 A, for any a ∈ A). If, additionally, a ∨ (a→ b) = 1 for every a, b then A is said to be a classical implicative lattice.10 It is well-known that, if A is a classical implicative lattice and it has a bottom element 0, then it is a Boolean algebra. An algebraic semantics for CPL+ is given by classical implicative lattices. That is, Γ `CPL+ α iff, for every classical implicative lattice A and for every homomorphism v from For(Σ+) to A, if v(γ) = 1 for every γ ∈ Γ then v(α) = 1. Let A = 〈A,∧,∨,→, 0, 1〉 be a Boolean algebra. Let πj : A3 → A be the canonical projections, for 1 ≤ j ≤ 3. Hence, if z ∈ A3 and zj = πj(z) for 1 ≤ j ≤ 3 then z = (z1, z2, z3). Analogously, if z ∈ A4 then we write z = (z1, z2, z3, z4), where zj denotes the jth projection of z. Definition 43 Let A be a Boolean algebra with domain A. (1) The universe of the swap structures for mbD over A is the set BmbDA = {z ∈ A3 : z1 ∧ z2 = 0 and z3 → ( z1 ∨ z2) = 1}. (2) The universe of the swap structures for mbCD over A is the set11 BmbCDA = {z ∈ A3 : z3 ∧ ( z1 ∧ z2) = 0 and z3 → ( z1 ∨ z2) = 1} = {z ∈ A3 : z3 ≤ ( z1 ∨ z2) ∧ ∼( z1 ∧ z2)}. (3) The universe of the swap structures for mbCDE over A is the set BmbCDEA = {z ∈ A4 : z3 ∧ ( z1 ∧ z2) = 0 and z4 → ( z1 ∨ z2) = 1}. Definition 44 Let A = 〈A,∧,∨,→, 0, 1〉 be a Boolean algebra. (1) A multialgebra B = 〈B,∧B,∨B,→B,¬B, 9B〉 over Σ9 is a swap structure for mbD over A if B ⊆ BmbDA and the following holds, for every z and w in B: (i) ∅ 6= z#Bw ⊆ {u ∈ B : u1 = z1#w1}, for each # ∈ {∧,∨,→}; (ii) ∅ 6= ¬B(z) ⊆ {u ∈ B : u1 = z2}; (iii) ∅ 6= 9B(z) ⊆ {u ∈ B : u1 = z3}. 10The name was taken from H. Curry, see [16]. 11Here, ∼ denotes the Boolean complement in A. 37 (2) A multialgebra B = 〈B,∧B,∨B,→B,¬B,~B〉 over Σ~ is a swap structure for mbCD over A if B ⊆ BmbCDA , the multioperations #B, are defined as in item (1) (for # ∈ {∧,∨,→,¬}) and, for every z in B: (iii) ∅ 6= ~B(z) ⊆ {u ∈ B : u1 = z3}. (3) A multialgebra B = 〈B,∧B,∨B,→B,¬B, ◦B, 9B〉 over Σ◦9 is a swap structure formbCDE overA if B ⊆ BmbCDEA , the multioperations #B, are defined as in item (1) (for # ∈ {∧,∨,→,¬, ◦}) and, for every z in B: (iv) ∅ 6= 9B(z) ⊆ {u ∈ B : u1 = z4}. As mentioned at the beginning of this section, each snapshot (z1, z2, z3) in a swap structure for mbD can be seen as a kind of complex truth-value such that z1 encodes the truth-value of a formula α, while z2 and z3 encode a possible truth-value for ¬α and 9α, respectively. The snapshots of swap structures for mbCD have a similar interpretation, but now z3 represents a possible truth-value for ~α. In the case ofmbCDE, a snapshot (z1, z2, z3, z4) is such that z1 represents the truth-value of a formula α, while z2, z3 and z4 encode a truth-value for ¬α, ◦α and 9α, respectively. From now on, the subscript 'B' will be omitted when referring to the multioperations of B. Definition 45 Let A be a Boolean algebra and L ∈ { mbD,mbCD,mbCDE } . There is a unique swap structure BLA for L with domain BLA such that '⊆' is replaced by '=' in Definition 44. As a consequence of Definition 45, the multioperations in each swap structure BLA are defined as follows: (i) z#w = {u ∈ BLA : u1 = z1#w1}, for each # ∈ {∧,∨,→} and each L; (ii) ¬(z) = {u ∈ BLA : u1 = z2}, for each L. On the other hand: (i) 9(z) = {u ∈ BmbDA : u1 = z3}, for mbD; (ii) ~(z) = {u ∈ BmbCDA : u1 = z3}, for mbCD; (iii) ◦(z) = {u ∈ BmbCDEA : u1 = z3}, for mbCDE; (iii) 9(z) = {u ∈ BmbCDEA : u1 = z4}, for mbCDE. 38 6 From swap structures to Nmatrix semantics In this section L will denote any logic in { mbD,mbCD,mbCDE } . Recall the semantics associated to Nmatrices introduced by Avron and Lev [2]. For each L as above, let KL be the class of swap structures for L. By adapting what was done in [7, Chapter 6] for several LFIs, as well as the techiques introduced in [13], it will be shown that each B ∈ KL induces a non-deterministic matrix such that the class of such Nmatrices semantically characterizes L. Definition 46 For each B ∈ KL let DB = {z ∈ |B| : z1 = 1}. The Nmatrix associated to B isM(B) = (B, DB). Let Mat ( KL ) = { M(B) : B ∈ KL } . Using the definition of valuation semantics over Nmatrices introduced in [2], the following valuation semantics can be associated to each class of Nmatrices considered above: Definition 47 Let B ∈ KL andM(B) as above. A valuation overM(B) is a function v from the set of formulas of L to |B| such that, for every formula α and β: (i) v(α#β) ∈ v(α)#v(β), for every # ∈ {∧,∨,→}; (ii) v(¬α) ∈ ¬v(α); (iii) v(9α) ∈ 9v(α), if L ∈ { mbD,mbCDE } ; (iii) v(◦α) ∈ ◦v(α), if L = mbCDE; (iv) v(~α) ∈ ~v(α), if L = mbCD. Definition 48 Let Γ ∪ {α} be a set of formulas of L. (1) We say that α is a consequence of Γ in M(B) ∈ Mat ( KL ) , denoted by Γ |=M(B) α, if v(α) ∈ DB for every valuation v over M(B) such that v(γ) ∈ DB for every γ ∈ Γ. (2) We say that α is a consequence of Γ in the class Mat ( KL ) of Nmatrices, denoted by Γ |=Mat(KL) α, if Γ |=M(B) α for everyM(B) ∈Mat ( KL ) . 39 Theorem 49 (Soundness of L w.r.t. swap structures) Let Γ ∪ {α} be a set of formulas of L. Then: Γ `L α implies Γ |=Mat(KL) α. Proof. It is an easy consequence of the definitions and of the fact that CPL+ is sound w.r.t. classical implicative lattices (and so w.r.t. Boolean algebras). Details are left to the reader (for swap structures for LFIs see [7, Chapter 6] and [13]). 2 In order to prove completeness, the technique introduced in [14] (see also [24, 13]) for constructing a Lindenbaum-Tarski multialgebra together with a canonical valuation will be adapted here. Let Γ be a non-trivial theory in L. An equivalence relation ≡LΓ in the set ForL of formulas of L is defined as follows: α ≡LΓ β iff Γ `L α → β and Γ `L β → α. Clearly, ≡LΓ is a congruence w.r.t. the connectives of CPL+ and so the quotient set ForL/≡LΓ is a classical implicative lattice with top element 1LΓ def = [p1 → p1]LΓ (here, [α]LΓ denotes the equivalence class of α w.r.t. ≡LΓ). Moreover, 0LΓ def = [p1 ∧ ¬p1]LΓ (for L = mbD); 0LΓ def = [◦p1 ∧ (p1 ∧ ¬p1)]LΓ (for L = mbCDE); and 0LΓ def = [~p1 ∧ (p1 ∧ ¬p1)]LΓ (for L = mbCD) is the bottom element of ForL/≡LΓ . Thus, A L Γ def = 〈 ForL/≡LΓ ,∧,∨,→, 0 L Γ , 1 L Γ 〉 is a Boolean algebra (details are left to the reader). Definition 50 Let Γ be a non-trivial theory in L. The Lindenbaum-Tarski swap structure for L (over Γ) is the swap structure BLALΓ defined over the Boolean algebra ALΓ (see Definition 45). The associated Nmatrix is denoted byMLΓ. Definition 51 The canonical valuation vLΓ overMLΓ is defined as follows: (i) vLΓ (α) def = ( [α]LΓ , [¬α]LΓ , [9α]LΓ ) , for L = mbD; (ii) vLΓ (α) def = ( [α]LΓ , [¬α]LΓ , [~α]LΓ ) , for L = mbCD; (ii) vLΓ (α) def = ( [α]LΓ , [¬α]LΓ , [◦α]LΓ , [9α]LΓ ) for L = mbCDE. It can be proved that vLΓ is indeed a valuation overMLΓ such that, by the very definitions, vLΓ (α) is designated iff Γ `L α. The Lindenbaum-Tarski swap structure together with the canonical valuation allows us to prove the completeness of L w.r.t. swap structures in a straightforward way: 40 Theorem 52 (Completeness of L w.r.t. swap structures) Let Γ∪{α} be a set of formulas of L. Then: Γ |=Mat(KL) α implies Γ `L α. Proof. Suppose that Γ 0L α. Then,MLΓ (see Definition 50) is an Nmatrix for L, and the canonical valuation vLΓ (see Definition 51) is a valuation overMLΓ such that vLΓ (γ) is designated, for every γ ∈ Γ, but vLΓ (α) is not designated. From this, Γ 6|=Mat(KL) α. 2 7 Decidability by finite Nmatrices As it happens with several LFIs and other logics characterized by swap structures defined over Boolean algebras (see [7, 13, 14, 24]), the swap structure BLA2 with domain B L A2 over the 2-element Boolean algebra A2 (with domain{ 0, 1 } ) is enough to characterize the logics L ∈ { mbD,mbCD,mbCDE } . This produces a decision procedure for each L by means of a finite Nmatrix, thanks to the semantical characterization of these logics through valuations (recall Section 4.1). From definitions 43 and 44, the special case for A2 produces, for mbD, a universe BmbDA2 = { T, t0, F, f0, f } such that T = (1, 0, 1), t0 = (1, 0, 0), F = (0, 1, 1), f0 = (0, 1, 0), and f = (0, 0, 0). The set of designated elements of the NmatrixMmbDA2 =M ( BmbDA2 ) is D = { T, t0 } , while ND = { F, f0, f } is the set of non-designated truth-values. The multioperations are defined as follows: ∧ T t0 F f0 f T D D ND ND ND t0 D D ND ND ND F ND ND ND ND ND f0 ND ND ND ND ND f ND ND ND ND ND ∨ T t0 F f0 f T D D D D D t0 D D D D D F D D ND ND ND f0 D D ND ND ND f D D ND ND ND 41 → T t0 F f0 f T D D ND ND ND t0 D D ND ND ND F D D D D D f0 D D D D D f D D D D D ¬ T ND t0 ND F D f0 D f ND 9 T D t0 ND F D f0 ND f ND Theorem 53 (Characterization of mbD by a finite Nmatrix) For every set of formulas Γ ∪ {α} ⊆ For(Σ9): Γ `mbD α iff Γ |=MmbDA2 α. Proof. The 'only if' part (soundness) is an immediate consequence of Theorem 49. The 'if' part (completeness) follows by the following: Fact: For every valuation v for mbD (see Definition 26) the mapping vmbD : For(Σ9) → BmbDA2 given by vmbD(α) = (v(α), v(¬α), v(9α)) is a valuation over the Nmatrix MmbDA2 such that: vmbD(α) ∈ D iff v(α) = 1, for every formula α. The proof of the Fact is analogous to the proof of Theorem 6.4.9 in [7], and is left to the reader. From this the result follows in a straightforward way. 2 Clearly, the 5-valued Nmatrix MmbDA2 provides a decision procedure for mbD. Note that the negation of mbD is explosive and paracomplete, in the sense that excluded middle is not valid (because of the behavior of f in the table of ¬.). Concerning the logic mbCD, the algebra A2 gives origin to a universe BmbCDA2 = { T, t0, t, F, f0, f } such that T, t0, F, f0 and f are as above, and t = (1, 1, 0). The set of designated elements of the Nmatrix MmbCDA2 = M ( BmbCDA2 ) is D' = { T, t0, t } , while ND = { F, f0, f } is the set of nondesignated truth-values. The multioperations are defined as follows: ∧ T t0 t F f0 f T D' D' D' ND ND ND t0 D' D' D' ND ND ND t D' D' D' ND ND ND F ND ND ND ND ND ND f0 ND ND ND ND ND ND f ND ND ND ND ND ND ∨ T t0 t F f0 f T D' D' D' D' D' D' t0 D' D' D' D' D' D' F D' D' D' ND ND ND f0 D' D' D' ND ND ND f D' D' D' ND ND ND 42 → T t0 t F f0 f T D' D' D' ND ND ND t0 D' D' D' ND ND ND t D' D' D' ND ND ND F D' D' D' D' D' D' f0 D' D' D' D' D' D' f D' D' D' D' D' D' ¬ T ND t0 ND t D' F D' f0 D' f ND ~ T D' t0 ND t ND F D' f0 ND f ND The following result can be proved in a similar way to the proof of Theorem 53: Theorem 54 (Characterization of mbCD by a finite Nmatrix) For every set of formulas Γ∪{α} ⊆ For(Σ~): Γ `mbCD α iff Γ |=MmbCDA2 α. The 6-valued NmatrixMmbCDA2 provides a decision procedure formbCD. Note that the negation of mbCD is both paraconsistent and paracomplete, respectively because of the behavior of t and the behavior of f in the table of ¬. Finally the logic mbCDE will be analyzed. The algebra A2 produces a universe BmbCDEA2 = { T 1, T 0, t10, t 0 0, t 1, t0, F 1, F 0, f 10 , f 0 0 , f 01, f 0 } such that T 1 = (1, 0, 1, 1), T 0 = (1, 0, 1, 0), t10 = (1, 0, 0, 1), t00 = (1, 0, 0, 0), t1 = (1, 1, 0, 1), t0 = (1, 1, 0, 0), F 1 = (0, 1, 1, 1), F 0 = (0, 1, 1, 0), f 10 = (0, 1, 0, 1), f 00 = (0, 1, 0, 0), f 01 = (0, 0, 1, 0), f 0 = (0, 0, 0, 0). The set of designated truth-values of the Nmatrix MmbCDEA2 = M ( BmbCDEA2 ) is D" ={ T 1, T 0, t10, t 0 0, t 1, t0 } , and ND' = { F 1, F 0, f 10 , f 0 0 , f 01, f 0 } is the set of non-designated truth-values. The multioperations are defined as follows: ∧ T 1 T 0 t10 t00 t1 t0 F 1 F 0 f10 f00 f01 f0 T 1 D" D" D" D" D" D" ND' ND' ND' ND' ND' ND' T 0 D" D" D" D" D" D" ND' ND' ND' ND' ND' ND' t10 D" D" D" D" D" D" ND' ND' ND' ND' ND' ND' t00 D" D" D" D" D" D" ND' ND' ND' ND' ND' ND' t1 D" D" D" D" D" D" ND' ND' ND' ND' ND' ND' t0 D" D" D" D" D" D" ND' ND' ND' ND' ND' ND' F 1 ND' ND' ND' ND' ND' ND' ND' ND' ND' ND' ND' ND' F 0 ND' ND' ND' ND' ND' ND' ND' ND' ND' ND' ND' ND' f10 ND' ND' ND' ND' ND' ND' ND' ND' ND' ND' ND' ND' f00 ND' ND' ND' ND' ND' ND' ND' ND' ND' ND' ND' ND' f01 ND' ND' ND' ND' ND' ND' ND' ND' ND' ND' ND' ND' f0 ND' ND' ND' ND' ND' ND' ND' ND' ND' ND' ND' ND' 43 ∨ T 1 T 0 t10 t00 t1 t0 F 1 F 0 f10 f00 f01 f0 T 1 D" D" D" D" D" D" D" D" D" D" D" D" T 0 D" D" D" D" D" D" D" D" D" D" D" D" t10 D" D" D" D" D" D" D" D" D" D" D" D" t00 D" D" D" D" D" D" D" D" D" D" D" D" t1 D" D" D" D" D" D" D" D" D" D" D" D" t0 D" D" D" D" D" D" D" D" D" D" D" D" F 1 D" D" D" D" D" D" ND' ND' ND' ND' ND' ND' F 0 D" D" D" D" D" D" ND' ND' ND' ND' ND' ND' f10 D" D" D" D" D" D" ND' ND' ND' ND' ND' ND' f00 D" D" D" D" D" D" ND' ND' ND' ND' ND' ND' f01 D" D" D" D" D" D" ND' ND' ND' ND' ND' ND' f0 D" D" D" D" D" D" ND' ND' ND' ND' ND' ND' → T 1 T 0 t10 t00 t1 t0 F 1 F 0 f10 f00 f01 f0 T 1 D" D" D" D" D" D" ND' ND' ND' ND' ND' ND' T 0 D" D" D" D" D" D" ND' ND' ND' ND' ND' ND' t10 D" D" D" D" D" D" ND' ND' ND' ND' ND' ND' t00 D" D" D" D" D" D" ND' ND' ND' ND' ND' ND' t1 D" D" D" D" D" D" ND' ND' ND' ND' ND' ND' t0 D" D" D" D" D" D" ND' ND' ND' ND' ND' ND' F 1 D" D" D" D" D" D" D" D" D" D" D" D" F 0 D" D" D" D" D" D" D" D" D" D" D" D" f10 D" D" D" D" D" D" D" D" D" D" D" D" f00 D" D" D" D" D" D" D" D" D" D" D" D" f01 D" D" D" D" D" D" D" D" D" D" D" D" f0 D" D" D" D" D" D" D" D" D" D" D" D" ¬ T 1 ND' T 0 ND' t10 ND' t00 ND' t1 D" t0 D" F 1 D" F 0 D" f10 D" f00 D" f01 ND' f0 ND' ◦ T 1 D" T 0 D" t10 ND' t00 ND' t1 ND' t0 ND' F 1 D" F 0 D" f10 ND' f00 ND' f01 D" f0 ND' 9 T 1 D" T 0 ND' t10 D" t00 ND' t1 D" t0 ND' F 1 D" F 0 ND' f10 D" f00 ND' f01 ND' f0 ND' 44 As in the previous cases, the following result can be easily proved: Theorem 55 (Characterization of mbCDE by a finite Nmatrix) For every set of formulas Γ ∪ {α} ⊆ For(Σ◦9): Γ `mbCDE α iff Γ |=MmbCDEA2 α. Proof. The proof is analogous to that for Theorem 53, with the following change: given a valuation v for mbCDE (see Definition 26), it induces a valuation vmbCDE over the Nmatrix MmbCDEA2 as follows: vmbCDE(α) = (v(α), v(¬α), v(◦α), v(9α)). 2 The 12-valued Nmatrix MmbCDEA2 constitutes a decision procedure for mbCDE. As in the case of mbCD, the negation of mbCDE is both paraconsistent (because of t1 and t0) and paracomplete (because of f 01 and f 0). 8 Final remarks We have seen here how two foundational ideas of paraconsistency may be developed further: the duality between paraconsistency and paracompleteness, and the introduction of logical operators that express meta-logical notions in the object language. The idea of da Costa's well-behavedness operator has been further developed by the consistency operator of LFIs. The later, in its turn, has given rise to the more general concept of recovery operators, represented here by the unary operators ◦, 9, and ~. Not only explosion but also excluded middle may be recovered inside systems in which they are not, in general, valid. The connectives ◦ and 9 may be combined in order to recover classical logic at once, and so the combined operator ~ may be called a classicality operator. Actually, it is fair to say that a whole path has been opened by the concept of 'logics of formal N', where the wildcard symbol N marks a space to be fulfilled by some logical property that we want to restrict and control inside a formal system. Additionally, we have already seen how a hierarchy of logics may be constructed in order to represent the degrees whereby the logical properties represented in object language are controlled. We may, for instance, represent levels of consistency, and establish the point in which the consistency of a proposition α is enough to recover explosion. The same idea may be 45 extended to determinedness, classicality, and in principle to any other logical property restricted/controlled by means of a recovery operator in an LFN. As mentioned at the beginning of Section 5, most of the LFIs introduced in the literature are not algebraizable by the usual tecnhiques, and so several alternatives were proposed in the literature, as for instance possible translations semantics (see [7, Secs. 4.3 and 6.8]). Swap structures semantics constitutes a simple and fruitful approach to algebraizability in a broader sense, by considering non-deterministic algebras instead of ordinary algebras (see [6], and [13] for recent algebraic developments on swap structures). The question of algebraizability of the LFUs and LFIUs introduced here has not been studied yet. References [1] A. Avron. Non-deterministic matrices and modular semantics of rules. In Jean-Y. Béziau, editor, Logica Universalis, pages 149–167, 2005. Birkhäuser Verlag. [2] A. Avron and I. Lev. Non-Deterministic Multiple-valued Structures. Journal of Logic and Computation, 15, 241-261, 2005. [3] W. J. Blok and D. Pigozzi. Algebraizable Logics, volume 77(396) of Memoirs of the American Mathematical Society. American Mathematical Society, Providence, RI, USA, 1989. [4] W. A. Carnielli. Possible-translations semantics for paraconsistent logics. Frontiers Of Paraconsistent Logic. (Eds. D. Batens et al). Baldock: Research Studies Press, pp. 159-172, 2000. [5] W. A. Carnielli. Groups, Not Squares: Exorcizing a Fetish. In: Béziau J.Y., Basti G. (eds) The Square of Opposition: A Cornerstone of Thought. Studies in Universal Logic. Birkhäuser, 2017. [6] W. A. Carnielli and M. E. Coniglio. Swap structures for LFIs. CLE e-Prints, vol. 14, n. 1, 2014. [7] W. A. Carnielli and M. E. Coniglio. Paraconsistent Logic: Consistency, Contradiction and Negation. Volume 40 of Logic, Epistemology, and the Unity of Science series. Springer, 2016. 46 [8] W. A. Carnielli, M. E. Coniglio, and J. Marcos. Logics of Formal Inconsistency. In: D. M. Gabbay and F. Guenthner, editors, Handbook of Philosophical Logic (2nd. edition), volume 14, pages 1–93. Springer, 2007. [9] W. A. Carnielli and J. Marcos. 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. Marcel Dekker, 2002. [10] W. A. Carnielli, J. Marcos and S. de Amo. Formal Inconsistency and evolutionary databases. Logic and Logical Philosophy, 8:115–152, 2000. [11] W. A. Carnielli and A. Rodrigues. Towards a philosophical understanding of the Logics of Formal Inconsistency. Manuscrito 38(2):155–184, 2015. [12] W. A. Carnielli and A. Rodrigues. Paraconsistency and duality: between ontological and epistemological views. In The Logica Yearbook 2015. College Publications, 2016. [13] M. E. Coniglio, A. Figallo-Orellano and A. C. Golzio. Non-deterministic algebraization of logics by swap structures. Logic Journal of the IGPL, to appear. Preprint available at arXiv:1708.08499 [math.LO], 2017. [14] M. E. Coniglio and A. C. Golzio. Swap structures for some non-normal modal logics. Submitted, 2017. [15] J. Ciuciura. Paraconsistent heap: a. hiearchy of mbCn-systems. Bulletin of the Section of Logic 43(3/4):173-182, 2014. [16] H.B. Curry. Foundations of Mathematical Logic. Dover Publications Inc., New York, 1977. [17] N. C. A. da Costa. Sistemas formais inconsistentes (Inconsistent formal systems, in Portuguese). Habilitation thesis, Universidade Federal do Paraná, Curitiba, Brazil, 1963. Republished by Editora UFPR, Curitiba, Brazil,1993. [18] N. C. A. da Costa. On the theory of inconsistent formal systems. Notre Dame Journal of Formal Logic, 4, XV, pp. 497-510, 1974. 47 [19] N. C. A. da Costa. Logics that are both paraconsistent and paracomplete. Atti Acc. Lincei Rend. fis., s. 8, v. 83, n. 1, p. 29–32, 1989. [20] N. C. A. da Costa and E. Alves. A semantical analysis of the calculi Cn. NotreDame Journal of Formal Logic, 18(4):621-630, 1977. [21] N. C. A. da Costa and Diego Marconi. A note on paracomplete logic. Atti Acc. Lincei Rend. fis., s. 8, v. 80, n. 7-12, p. 504–509, 1986. [22] M. M. Fidel. The decidability of the calculi Cn. Reports on Mathematical Logic, 8:31–40, 1977. [23] G. Gentzen. Investigations into Logical Deduction. The Collected Papers of Gerhard Gentzen (ed. M.E. Szabo), North-Holland Publishing Company (1969), 1935. [24] A. C. Golzio. Non-deterministic matrices: Theory and applications to algebraic semantics. PhD thesis, IFCH, University of Campinas, 2017. [25] A. C. Golzio and M. E. Coniglio. Non-deterministic algebras and algebraization of logics. In: M. Carvalho, C. Braida, J.C. Salles and M.E. Coniglio, editors, Filosofia da Linguagem e da Lógica, Coleção XVI Encontro ANPOF Series, pages 327–346. ANPOF, 2015. [26] E. Gomes. Sobre a história da paraconsistência e a obra de da Costa: a instauração da lógica paraconsistente (On the History of Paraconsistency and da Costa's work: the instauration of paraconsistent logic, in Portuguese). PhD thesis, IFCH, University of Campinas, 2013. [27] D. Hilbert and W. Ackermann. Principles of Mathematical Logic (Grundzüge der theoretischen Logik (1938), transl. by Lewis Hammond et al.). American Mathematical Society, 2000. [28] Jáskowski, S. Propositional calculus for contradictory deductive systems. Studia Logica (1969), 1948, vol. 24, pages 143–157 [29] S. C. Kleene. Introduction to Meta-mathematics, 1950. Republished by Ishi Press International, New York, 2009. [30] A. Loparic and E. Alves. The semantics of the systems Cn of da Costa. In A. I. Arruda, N. C. A. da Costa, and A. M. Sette, editors, Proceedings of 48 the III Brazilian Conference on Mathematical Logic, Recife, 1979, pages 161-172. Brazilian Logic Society, SÃčo Paulo, 1979. [31] J. Marcos. Nearly every normal modal logic is paranormal. Logique et Analyse, 48(189-192):279-300, 2005. [32] S. P. Odintsov. Algebraic semantics for paraconsistent Nelson's logic. Journal of Logic and Computation, 13(4):453-468, 2003. [33] G. Priest. The Logic of Paradox. Journal of Philosophical Logic. 8(1): 219-241, 1979. [34] T. G. Rodrigues. Sobre os Fundamentos da Programação Lógica Paraconsistente (On the Foundations of Paraconsistent Logic Programming, in Portuguese). MSc dissertation, IFCH, University of Campinas, 2010. [35] R. Wójcicki. Lectures on propositional calculi. Ossolineum, Wroclaw, Poland, 1984.