Paracomplete logics which are dual to the paraconsistent logics L3A and L3B Alejandro Hernández-Tello1 , Verónica Borja Macı́as1 and Marcelo E. Coniglio2 1 Instituto de Fı́sica y Matemáticas (IFM), Universidad Tecnológica de la Mixteca (UTM), Oaxaca, México. 2 Institute of Philosophy and the Humanities (IFCH) and Centre for Logic, Epistemology and The History of Science (CLE), University of Campinas (UNICAMP), Campinas, SP, Brazil {alheran,vero0304}@gmail.com, coniglio@unicamp.br Abstract. In 2016 Beziau, introduce a more restricted concept of para- consistency, namely the genuine paraconsistency. He calls genuine para- consistent logic those logic rejecting ϕ, ¬ϕ ` ψ and ` ¬(ϕ ∧ ¬ϕ). In that paper the author analyzes, among the three-valued logics, which of these logics satisfy this property. If we consider multiple-conclusion consequence relations, the dual properties of those above mentioned are ` ϕ, ¬ϕ and ¬(ψ ∨ ¬ψ) `. We call genuine paracomplete logics those rejecting the mentioned properties. We present here an analysis of the three-valued genuine paracomplete logics. Keywords: Many-valued logics · Paracomplete logics · dual logic. 1 Introduction Classically, a negation ¬ for a given logic L is semantically characterized by two properties: (1) for no sentence ϕ it is the case that ϕ and ¬ϕ are simultaneously true; and (2) for no sentence ϕ it is the case that ϕ and ¬ϕ are simultaneously false. Principle (1) is known as the law of non-contradiction (NC) (also known as the law of explosion), while (2) is usually called the law of excluded middle (EM). In terms of multiple-conclusion consequence relations1 , both laws can be represented as follows: (NC) ϕ, ¬ϕ ` and (EM) ` ϕ, ¬ϕ. This is why both laws are usually considered as being dual one from the other2 . If L has a conjunction ∧ (which corresponds to commas on the left-hand 1 We can consider a multiple-conclusion consequence relation ` as a binary relation between sets of formulas Γ and ∆, such that Γ ` ∆ means that any model of every γ ∈ Γ is also a model for some δ ∈ ∆ [7]. 2 The reader must be careful with the notation used in this document because in [3] the authors use NC for representing T ` ¬(ϕ ∧ ¬ϕ), where T is any set of formulas. Copyright © 2019 for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0) 37 side of `) and a disjunction ∨ (which corresponds to commas on the right-hand side of `), then both laws can be written as (NC) ϕ ∧ ¬ϕ ` and (EM) ` ϕ ∨ ¬ϕ. Let L be a logic with a negation ¬. If it satisfies (NC), then the negation ¬ is said to be explosive, and L is explosive (w.r.t. ¬). On the other hand, L is said to be paraconsistent (w.r.t. ¬) if (NC) does not hold in general, that is: ϕ, ¬ϕ 0 in general. This means that there are formulas ϕ and ψ such that ϕ, ¬ϕ 0 ψ (or ϕ ∧ ¬ϕ 0 ψ, if L has a conjunction). Dually, a logic L is paracomplete (w.r.t. ¬) if (EM) does not hold in general, that is: 0 ϕ, ¬ϕ in general. That is, there are formulas ϕ and ψ such that ψ 0 ϕ, ¬ϕ (or ψ 0 ϕ ∨ ¬ϕ, if L has a disjunction). As observed in [3], (NC) is sometimes expressed as follows: (NC0 ) ` ¬(ϕ ∧ ¬ϕ). However, as the authors have shown in [3], both principles are independent. Moreover, they show that several paraconsistent logics validate (NC0 ), which is arguably counterintuitive or undesirable. This motivates the definition of a strong paraconsistent logic as being a logic in which both principles, (NC) and (NC0 ), are not valid in general. In subsequent papers (see, for instance, [2]) strong paraconsistent logic was rebaptized as genuine paraconsistent logic. Thus, a logic L with negation and conjunction is genuine paraconsistent if, for some formulas ϕ and ψ, (GP1) ϕ ∧ ¬ϕ 0 and (GP2) 0 ¬(ψ ∧ ¬ψ). Given the duality between (NC) and (EM), it makes sense to consider (in a logic with disjunction) the dual property of (NC0 ), namely (EM0 ) ¬(ϕ ∨ ¬ϕ) ` . This motivates the following definition: Definition 1. A logic L with negation and disjunction is said to be a gen- uine paracomplete logic (or a strong paracomplete logic) if neither (EM) nor (EM0 ) is valid, that is: for some formulas ϕ and ψ, (GP1D ) 0 ϕ ∨ ¬ϕ and (GP2D ) ¬(ψ ∨ ¬ψ) 0 . Observe that, in terms of a tarskian (single-conclusion) consequence relation (see Definition 2), (GP2D ) is equivalent to the following: (GP2D ) ¬(ψ ∨ ¬ψ) 0 ϕ for some formulas ϕ, ψ. In semantical terms, if (GP2D ) holds for ψ then ψ is satisfiable, that is: it has some model. 38 Remark 1. If L is a logic with negation ¬ and conjunction ∧ such that ¬ satisfies the right-introduction rule: Γ, ϕ ` ∆ implies that Γ ` ¬ϕ, ∆ (which implies that (EM) is valid in L, that is, L is not paracomplete) then (NC) implies (NC0 ). In this case, L is genuine paraconsistent if it satisfies (GP2) for some formula. Indeed, if (GP2) holds for some formula ϕ then (GP1) also holds for ϕ. Dually, if L is a logic with negation ¬ and disjunction ∨ such that ¬ satisfies the left-introduction rule: Γ ` ϕ, ∆ implies that Γ, ¬ϕ ` ∆ (which implies that (NC) is valid in L, that is, L is not paraconsistent), then (EM) implies (EM’). In this case, L is genuine paracomplete, if it satisfies (GP2D ) for some formula. Indeed, if (GP2D ) holds for some ϕ, then (GP1D ) also holds for ϕ. Examples: 1. Propositional Intuitionistic logic IPL is paracomplete, but it is not genuine paracomplete: the formula ¬(ϕ ∨ ¬ϕ) is unsatisfiable. 2. The Belnap-Dunn logic F OU R (with the truth ordering) is both genuine paraconsistent and genuine paracomplete. 3. Nelson logic N4 is both genuine paraconsistent and genuine paracomplete. 4. The 3-valued logic MH, introduced in [4], is genuine paracomplete and ex- plosive. As we shall see, it is a 3-valued genuine paracomplete logics which conservatively extend the 2-valued truth tables of classical logic CPL. 2 Basic concepts We consider a formal language L = hatom(L), C, Ai, where atom(L) is an enu- merable set, whose elements are called atoms and are denoted by lowercase letters; C is a set of connectives and A is a set of auxiliary symbols. Formulas are constructed as usual and will be denoted by lowercase Greek letters. The set of all formulas of L is denoted as F orm(L). Theories are sets of formulas and will be denoted by uppercase Greek letters. Definition 2. A (tarskian) consequence relation ` between theories and formulas is a relation satisfying the following properties, for every theory Γ ∪ ∆ ∪ {ϕ}: (Reflexivity) if ϕ ∈ Γ , then Γ ` ϕ; (Monotonicity) if Γ ` ϕ and Γ ⊆ ∆, then ∆ ` ϕ; 39 (Transitivity) if ∆ ` ϕ and Γ ` ψ for every ψ ∈ ∆, then Γ ` ϕ. in addition if for every L-substitution θ, holds that Γ ` ϕ implies θ(Γ ) ` θ(ϕ), ` is called structural. If there exist some non-empty theory Γ and some ϕ such that Γ 6` ϕ, ` is called non-trivial. Sometimes to define a logic is required that ` be finitary3 . However, here we consider a logic as it is established in Definition 3. Definition 3. A logic is a pair L = hL, `L i, where `L is a structural and non-trivial consequence relation, satisfying be closed under Modus Ponens (MP), which means that for any formulas ϕ and ψ holds that ϕ → ψ, ϕ `L ψ. The notation Γ `L ϕ could be read as ϕ can be inferred from Γ in L. Whenever the logic is clear the subscript will be dropped. The usefulness of a logic depends on the available connectives in its language, as we have pointed out in the introduction, for talking about paracompleteness we need a negation and a disjunction satisfying particular conditions. However, we are going to complete the language with an appropriate conjunction and an appropriate implication. In Definition 4 we establish some conditions on connec- tives so they can be considered as conjunction, disjunction, implication. Definition 4. [1] Let L be a logic in the language L with binary connectives ∧, ∨ and →, then: 1. ∧ is a conjunction for L, when: Γ ` ϕ ∧ ψ iff Γ ` ϕ and Γ ` ψ. 2. ∨ is a disjunction for L, when: Γ, ϕ ∨ ψ ` σ iff Γ, ϕ ` σ and Γ, ψ ` σ. 3. → is an implication for L, when: Γ, ϕ ` ψ iff Γ ` ϕ → ψ. In [5] in order to find a suitable implication for the logics L3A and L3B the authors define the concept of classical implication as follows. Definition 5. [5] Let L be a logic in the language L with a binary connective →, it is a classical implication if: i) Γ ` ϕ and Γ ` ϕ → ψ imply that Γ ` ψ; ii) Γ `  ϕ → (ψ → ϕ);    iii) Γ ` ϕ → (ψ → σ) → (ϕ → ψ) → (ϕ → σ) . It is not difficult to prove in the context of tarskian consequence relations that the notions of implication in Definition 4 and Definition 5 agree. The usual manner to define many-valued logics is by means of a matrix. Definition 6. A matrix for a language L, is a structure M = hV, D, F i, where: V is a non-empty set of truth values (domain); 3 Informally speaking, it means that every deduction can be obtained by a finite num- ber of hypothesis. 40 D is a subset of V (set of designated values); F := {fc |c ∈ C} is a set of truth functions, with a function for each logical connective in L. Definition 7. Given a language L, a function v : atom(L) −→ V that maps atoms into elements of the domain is a valuation. It can be extended to all formulas v : F orm(L) −→ V as usual, i.e. applying recursively the truth functions of logical connectives in F . Now we can define the notion of model, see Definition 8. Definition 8. Given a matrix M , we say that v is a model of the formula ϕ, if v(ϕ) ∈ D and we denote it by t |=M ϕ. A formula ϕ is a tautology in M if every valuation is a model of ϕ, it is denoted by |=M ϕ. Whenever the matrix is clear the subscript will be dropped. It is also possible to define a consequence relation by means of a matrix. Definition 9. [1] Given a matrix M , its induced consequence relation, de- noted by `M , is defined by: Γ `M ϕ if every model of Γ is a model of ϕ. We denote by LM = hL, `M i the logic obtained with this consequence relation. Now we define neoclassical connectives, its name can be easily understood if we identify the True value with designated and False with not designated. These conditions are generalizations of those that satisfy and in some way define the nature of the connectives in Classical Logic. Definition 10. [5] Let M = hV, D, F i be a matrix, D the set of non-designated values, and v any valuation, then: 1. ∧ is a Neoclassical conjunction, if it holds that: v(ϕ ∧ ψ) ∈ D iff v(ϕ) ∈ D and v(ϕ) ∈ D. 2. ∨ is a Neoclassical disjunction, if it holds that: v(ϕ ∨ ψ) ∈ D iff v(ϕ) ∈ D and v(ϕ) ∈ D. 3. → is a Neoclassical implication, if it holds that: v(ϕ → ψ) ∈ D iff v(ϕ) ∈ D or v(ψ) ∈ D. Definition 11. A three-valued operator ~ : V 2 −→ V is a: Conservative extension, of a bi-valued operator if the restriction of ~ to the values of the bi-valued operator coincide[3]. Molecular operator, if the range of it is a proper subset of V . Observe that conditions of neoclassicality of Definition 10 are more restrictive than those on Definition 4. Specifically, we have that items 2 and 3 on Definition 10 imply items 2 and 3 on Definition 4. Moreover, item 1 on Definition 10 is equivalent to item 1 on Definition 4. 41 3 Three-valued genuine paracomplete logics In this section we study logics LM = hL, `M i, where M = h{0, 1, 2}, D, F i and 0, 2 are identified with False and True respectively. This implies 2 ∈ D, 0 6∈ D. We search three-valued genuine paracomplete logics extending conservatively classical logic, apart from some extra conditions such as neoclassicality, non- molecularity, etc. 3.1 Independence of EM and EM0 In Definition 1, we ask two conditions for a logic be called genuine paracomplete, let us see that these conditions are independent. If we define negation as v(¬ϕ) = 2 − v(ϕ) and disjunction as the maximum among the disjuncts, then depending on the choice of the set of designated values we have one and just one principle satisfied. On one hand, if the set of designated values are {1, 2}, in Table 1, we can see that the third column from left to right is composed only by designated values therefore EM is satisfied, meanwhile EM0 is not, since in the fourth column there is a row which has one designated value. On the other hand, if we take the set of designated values as {2}, then the fourth column has not designated values and so EM0 is satisfied, but since the third column has a not designated row EM does not hold. This shows that in order to get a three-valued genuine paracomplete logic it is necessary to use a different combination of truth tables for the connectives of negation and disjunction. ϕ ¬ϕ ϕ ∨ ¬ϕ ¬(ϕ ∨ ¬ϕ) 0 2 2 0 1 1 1 1 2 0 2 0 Table 1. Independency of principles EM and EM0 3.2 Genuine Paracomplete Negation Let us start by analyzing the negation. Since we are considering connectives that are conservative extensions of the 2-valued truth tables of classical logic, we have already fixed some of the values of the truth table for negation, namely those that are boxed in Table 2. As a result of this, only the second row in the table should be analyzed in order to fix the value of the variable n, that denotes the unknown value for negation. Note that we can not assign 2 to n. Otherwise, in Table 2, we have in every row either ϕ or ¬ϕ are designated validating EM in terms of multiple-conclusion 42 consequence relations. Therefore, n must be in {0, 1}. Up to this point, we know that 2 ∈ D and 0 6∈ D, but if we set 1 as designated once more in every row either ϕ or ¬ϕ is designated validating EM. Hence, in a three-valued genuine paracomplete logic D = {2}. ϕ ¬ϕ 0 2 1 n 2 0 Table 2. Possible negations 3.3 Genuine Paracomplete Disjunction As in the case of negation, due to the condition of being conservative extensions, there are some fixed values in the truth table for the disjunction, they will be boxed in Table 3 in order to be identified. We want to obtain a neoclassical disjunction in order to keep the semantical behavior of the classical disjunction, this condition fixes two more values which are circled in Table 3 and restricts the value of the three remaining ones as not designated. The condition of symmetry reduces the number of variables to d1 , d2 ∈ D, since 0 ∨ 1 = 1 ∨ 0 = d1 . Finally, the values for d1 and d2 depend on the choice of n in the truth table for negation, either n = 0 or n = 1. Let us analyze by cases. ∨ 0 1 2 0 0 d1 2 1 d1 d2 2 2 2 2 2 Table 3. Possible disjunction Case n = 0 Considering the negation whose table takes the value of 0 for n, we have the following sub-cases: 1. If d1 = 0, DP1D and DP2D hold and Definition 1 is satisfied, regardless of the value of d2 , as Table 4 shows. DP1D holds since in the third column, ϕ ∨ ¬ϕ is not a tautology due to the 0 in the second row. On the other hand, DP2D holds since in the fourth column ¬(ϕ ∨ ¬ϕ) has a model due to the 2 in the second row. 43 ϕ ¬ϕ ϕ ∨ ¬ϕ ¬(ϕ ∨ ¬ϕ) 0 2 2 0 1 0 0 2 2 0 2 0 Table 4. Truth tables for DP1D and DP2D when n = 0 and d1 = 0 2. If d1 = 1, then for any valuation v(¬(ϕ ∨ ¬ϕ)) = 0 and DP2D does not hold. Therefore, the only acceptable value for d1 is 0. Thus we have the combinations d1 = 0, d2 = 0 and d1 = 0, d2 = 1. However, if d1 = d2 = 0, the connective ∨ becomes molecular, which is not desirable. So, if n = 0 we have only one choice to get a genuine paracomplete disjunction, d1 = 0 and d2 = 1. See Table 7 left. Case n = 1 When n = 1, we have the following sub-cases: 1. If d2 = 0, then DP1D as well as DP2D hold as desired, without considering d2 , as we can see in Table 5 analogously to Table 4. ϕ ¬ϕ ϕ ∨ ¬ϕ ¬(ϕ ∨ ¬ϕ) 0 2 2 0 1 1 0 2 2 0 2 0 Table 5. Truth tables for DP1D and DP2D when n = 1 and d2 = 0 2. If d2 = 1, then v(¬(ϕ ∨ ¬ϕ)) ∈ D and DP2D does not hold. Analogously to the case n = 0 we have only one choice to get a genuine para- complete disjunction, d2 = 0 and d1 = 1. See Table 7 right. The previous analysis leads us to two different three-valued genuine paracom- plete logics in the language that include ¬ and ∨ as their unique connectives. An interesting fact is that we can get the same truth tables for negation and disjunction, up to reordering, just considering the negation and conjunction of the genuine paraconsistent logics L3A and L3B, and dualizing them. We mean by dualizing switching the truth values 2 for 0, 1 by 1 and 0 for 2. In Table 6 we show this process, where we obtain dualized connectives of negation and disjunction from L3A and L3B. Definition 12. The three-valued logic LM = hL, `M i, where M is the matrix with a set of values {0, 1, 2}, 2 as the only designated value, and connectives taken from left side of Table 7 is called L3AD . Otherwise, if we take the connectives on the right side, we obtain the L3BD logic. 44 ϕ ¬L3A ϕ ϕ (¬L3A )D ϕ ∧L3A 0 1 2 (∧L3A )D 2 1 0 0 2 dualizing 0 000 dualizing 2 0 2 222 −−−−−→ −−−−−→ 1 2 1 0 1 012 1 210 2 0 0 2 2 022 0 200 ϕ ¬L3B ϕ ϕ (¬L3B )D ϕ ∧L3B 0 1 2 (∧L3B )D 2 1 0 0 2 dualizing 0 000 dualizing 2 0 2 222 −−−−−→ −−−−−→ 1 1 1 1 1 021 1 201 2 0 0 2 2 012 0 210 Table 6. Dual connectives of ¬ and ∧ in genuine paraconsistent logics L3A and L3B ϕ ¬ϕ ∨012 ϕ ¬ϕ ∨012 0 2 0002 0 2 0012 1 0 1012 1 1 1102 2 0 2222 2 0 2222 L3AD L3BD Table 7. Truth tables for ¬ and ∨ in L3AD and L3BD 3.4 Genuine Paracomplete Conjunction Since the definition of genuine paracompleteness does not impose conditions over the conjunction connective we can choose any of the definable conjunctions in a three-valued logic. Considering again, conservative extensions, neoclassicality symmetry and not molecularity we have a partial table for the conjunction as the one on the left side of Table 8 where c1 , c2 and c3 ∈ D and it is not the case that c1 = c2 = c3 = 0. Then there are 7 different conjunctions satisfying all these restrictions. However, if we want to extend L3AD and L3BD with a conjunction keeping its duality with the paraconsistent logics L3A and L3B, we must dualize their disjunction i.e. the maximum function. The resulting conjunction for the genuine paracomplete logics is the minimum function, see the right side of Table 8. ∧ 0 1 2 ∧012 0 0 c1 0 0000 1 c1 c2 c3 1011 2 0 c3 2 2012 Table 8. Possible conjunction and ∧ in L3AD and L3BD 45 3.5 Genuine Paracomplete Implication In [5] a search for implications, satisfying specific properties, in L3A and L3B is done. Analogously, here we search for implications for L3AD and L3BD . The condition of being a conservative extension fix four values, see boxes in Table 9a. By the nature of the logics in this section and the fact D = {2}, see Section 3.2, the conditions in Definition 5 can be re-written as follows: For any valuation v: If v(ϕ) = 2 and v(ϕ → ψ) = 2, then v(ψ) = 2; MP v(ϕ → (ψ → ϕ)) = 2; A1 v( (ϕ → (ψ → σ)) → ((ϕ → ψ) → (ϕ → σ))) = 2. A2 Assume that → is a connective satisfying MP, A1, and A2. Then i5 6= 2 as a consequence of MP. Suppose that v(ϕ) = 2, as A1 is satisfied, then by MP we must have v(ψ → ϕ) = 2, therefore i4 = 2. If i3 = 1, then 1 → (1 → 1) = 1, a contradiction with A1, hence i3 6= 1. This gives Table 9b. Up to now we have two chances with respect to i5 , its value is 0 or 1. In the former case, if i5 = 0 in Table 9b, then: • i2 = 2, otherwise A1 would not hold when v(ϕ) = 1 and v(ψ) = 2; • If i1 = 0, then A2 does not hold, for v(ϕ) = 0, v(ψ) = 0 and v(σ) = 1; • If i1 = 1, i3 = 0, then A1 does not hold for v(ϕ) = 1 and v(ψ) = 0; • If i1 = 1, i3 = 2, then A2 does not hold for v(ϕ) = 0, v(ψ) = 2 and v(σ) = 1; • If i1 = 2, i3 = 0, then A2 does not hold for v(ϕ) = 1, v(ψ) = 0 and v(σ) = 1. this analysis for i5 = 0 only leave us one option, namely →0 in Table 10. In the second case, when i5 = 1 we have: • i3 = 2, otherwise A1 would not hold when v(ϕ) = 1 and v(ψ) = 2; • If i1 = 0, then A2 does not hold, for v(ϕ) = 0, v(ψ) = 0 and v(σ) = 1; • If i1 = 1, i2 = 1, then A1 does not hold for v(ϕ) = 0 and v(ψ) = 0; • If i1 = 2, i2 = 1, then A2 does not hold for v(ϕ) = 1, v(ψ) = 1 and v(σ) = 0. this analysis for i5 = 1 leave us with 4 options, namely →1 , →2 , →3 and →4 in Table 10. The five connectives in Table 10 are conservative extensions of the classical implication and are implications according to 4. Now if we ask for neoclassicality to be satisfy, see Definition 10, we only have →0 and →1 . One nice additional feature of connectives →0 and →1 is that any of the logics obtained extending L3AD or L3BD with any of the connectives →0 or →1 , satisfy the positive fragment of classical logic. The logic obtained extending L3BD with →0 , namely L3BD →0 is MH from [4], where a Hilbert system for it is presented. But, if we look for a non-molecular implication, just one option is left →1 . It is worth to mention that this implication corresponds to the implication of the three-valued logic of Kleene [1]. 46 → 0 1 2 → 0 1 2 0 0 i1 2 0 0 i1 2 1 i2 i3 i4 1 i2 0/2 2 2 2 i5 2 2 2 0/1 2 a b Table 9. Possible implications →0 0 1 2 →1 0 1 2 →2 0 1 2 →3 0 1 2 →4 0 1 2 0 222 0 222 0 212 0 222 0 212 1 222 1 222 1 022 1 022 1 222 2 002 2 012 2 012 2 012 2 012 Table 10. Possible implications for L3AD and L3BD 4 Conclusions In this paper we introduce the notion of genuine paracomplete logic, these logics are presented as logics rejecting the dual principles that define genuine para- consistent logic. On one hand, in a similar way to the analysis done in [3], we develop a study among three-valued logics in order to find all connectives defin- ing genuine paracomplete logics. We found two unary connectives that can serve as negation and fixing one of these negations, we discover in each case just one disjunction that works accordingly to our requests established for this particular kind of paracompleteness. On the other hand, if we take the connectives defining genuine three-valued paraconsistent logics, L3A and L3B, later perform a pro- cess of dualizing them, we obtain the same connectives as before. This process conducted to L3AD and L3BD logics, see Definition 12. In a further step, trying to extend the language with a conjunction, we found seven different suitable connectives for conjunction, among these, we select the minimum function in order to get L3A and L3B completely dualized. Finally, proceeding analogously to [6], we found implications for L3AD and L3BD , satisfying being neoclassical implications, namely →0 and →1 , these implications give place to the logics L3AD D D D →0 , L3A→1 , L3B→0 and L3B→1 . This completes our analysis leaving four genuine paracomplete three-valued logics that dualize L3A and L3B. In [4] a Hilbert system for one of these logics is presented, as a future work we consider to find axiomatizations for the remaining ones in order to have a better understanding of the nature of these logics. For instance, the relations among the connectives is not evident from the truth tables, since they are defined individually. However, axioms facilite to observe the way in which the connectives are related. 47 References [1] Ofer Arieli and Arnon Avron. Three-valued paraconsistent propositional log- ics. In Jean-Yves Beziau, Mihir Chakraborty, and Soma Dutta, editors, New Directions in Paraconsistent Logic, pages 91–129, New Delhi, 2015. Springer India. [2] Jean-Yves Beziau. Two genuine 3-valued paraconsistent logics. In Towards Paraconsistent Engineering, pages 35–47. Springer, 2016. [3] Jean-Yves Beziau and Anna Franceschetto. Strong three-valued paraconsis- tent logics. In New directions in paraconsistent logic, pages 131–145. Springer, 2015. [4] Colin Caret. Hybridized paracomplete and paraconsistent logics. The Aus- tralasian Journal of Logic, 14(1), 2017. [5] Alejandro Hernández-Tello, José Arrazola Ramı́rez, and Mauricio Oso- rio Galindo. The pursuit of an implication for the logics L3A and L3B. Logica Universalis, 11(4):507–524, 2017. [6] Alejandro Hernández-Tello, José Arrazola Ramı́rez, and Mauricio Osorio Galindo. The pursuit of an implication for the logics l3a and l3b. Logica Universalis, 11(4):507–524, 2017. [7] David J Shoesmith and Timothy John Smiley. Multiple-conclusion logic. CUP Archive, 1978. 48