Methodology to represent functions in logic BL⊃ Mauricio Osorio1 , Daniela Hernández-Grijalva2 and Alejandro Hernández-Tello2 1 Departamento de Actuarı́a Fı́sica y Matemáticas, Universidad de las Américas Puebla(UDLAP), Puebla, México, E-mail: osoriomauri@gmail.com 2 Instituto de Fı́sica y Matemáticas(IFM), Universidad Tecnológica de la Mixteca (UTM), Oaxaca, México, E-mail: hg.danii@gmail.com E-mail: alheran@gmail.com Abstract. In 1996 Avron and Arieli present a four-valued logic with its axiomatization, this logic is called BL⊃ , and is defined in terms of four connectives ¬, ∧, ∨, →. In this paper, we look over BL⊃ and show that it is a genuine paraconsistent logic, besides being paracomplete. Furthermore, we show a methodology for representing functions through a many-valued logic. In particular for expressing the Klein group, through the logic BL⊃ . Keywords: many-valued logics · genuine paraconsistent logic · Klein group. Introduction Several authors ([4, 7, 8, 11] and [12]) agree in the definition of paraconsistency, which accepts that a single contradiction should not imply every formula. For- mally, this may be represented by p, ¬p 0 q (where p and q are propositional variables) [4]. In [6] the concept of genuine logic is presented as a logic that does not obey either p, ¬p 0 q or 0 ¬(p ∧ ¬p). Motivation – In [10], da Costa and Krause point out some applications of paraconsistency logic into physics, particularly they talk about quantum theory: The possibility of using non-standard systems does not necessarily entail that classical logic is wrong, or that (in particular) quantum theory needs at the moment another logic. Physicists probably will continue to use classical (informal) logic in the near future. But we should realize that other forms of logic may help us in the better understanding of certain features of the quantum world as well, not easily treated by classical devices, as the concepts of complementarity and of non-individuality show [...] [10, p.17]. Copyright © 2019 for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0) 49 – Graham Priest in a recent paper claims that using paraconsistent logic can be useful for treating the Gödel’s First Incompleteness Theorem. Much has been written about Gödel’s First Incompleteness The- orem. Nearly always, this is on the assumption that the logic of the theory of arithmetic in question is classical –or at least intuitionistic– logic. Yet the use of a paraconsistent logic puts a distinctively new spin on matters [14]. – In 2015 Graham Priest shows a very interesting use of a 4-valued logic in Indian logic. • The catus.kot.i (Greek: tetralemma; English: four corners) is a venerable prin- ciple of Indian logic, which has been central to important aspects of reasoning in the Buddhist tradition [...] [13, p.1]. • [...] The four kot.is (corners) of the catus.kot.i are four options that one might take on a question. Given any question, there are four possibilities, yes, no, both, and neither [...] [13, p.2]. – Arieli and Avron in [3] make some remarks in the advantage of using tetra- valued logics for artificial intelligence, for instance, they mention that: • In his well-known paper “How computer should think” Belnap (1977) argues that four-valued semantics is very suitable setting for computarized reasoning [...] [3, p.97]. • The main advantage of using F OU R rather than three-valued systems is, of course, that it allows us to deal with both types of abnormal propositions in one system [...] [3, p.125]. • [...] This freedom to use more truth values does not add much; each one of the multi-valued logics considered here can actually be characterized by one of our four-valued logics. [3, p.128]. – In modern algebra Klein group is studied, it is a group of cardinality 4, such that any element is its inverse. It is worth mentioning that there is not a group of three elements with such property (see section 1.3). It has applications in biology, specifically in molecular systems [1]. In this work, we deal with BL⊃ , one paraconsistent logic defined in [2]; it has four primitive connectives ¬, ∧, ∨, →. Our contributions are the following: 1. We provide a weak form of the substitution property for BL⊃ , we show that the regular substitution property does not hold in BL⊃ . See section 2, Theorem 2. 2. At the end of Section 2.1, we give a list of steps that allows us to express the operation of a group in terms of connectives of a logic, particularly in that section we show how to construct the operation of Klein group in terms of connectives of BL⊃ . 3. In Theorem 5, we show that every function f : Dn −→ D, where D is the set of values of BL⊃ can be expressed in terms of a special set of functions. 50 1 Background In this section, we present two of the more common ways of defining a logic and provide examples. In Section 1.1, we define a logic from the semantical point of view, particularly via many-valued systems. On the other hand, in Section 1.2, we give one axiomatic formal system for logic BL⊃ , [5, Section 4.2], which corresponds to the syntactical approach. 1.1 Many-valued logics A way to define a logic is by truth values and interpretations. Many-valued systems generalize the idea of using the truth tables that are used to determine the validity of formulas in classical logic. Pioneers such as Lukasiewicz considered such many-valued systems as alternatives to the classical framework. As other authors do, we prefer to give to many-valued systems the benefit of the doubt about their status as logics. The core of a many-valued system is its domain of values D, specifically D is a nonempty set of truth-values, where some of such values are special and identified as designated. Connectives (e.g. ∧, ∨, →, ¬) are then introduced as operators over D according to the particular definition of the logic. An interpretation is a function I : L → D that maps atoms to elements in the domain, where L is the set formed by the atoms of language. The application of I is then extended to arbitrary formulas by mapping first the atoms to values in D, and then evaluating the resulting expression in terms of the connectives of the logic. A formula is said to be a tautology if, for every possible interpretation, the formula evaluates to a designated value. The most simple example of a many-valued logic is classical propositional logic where: D = {0, 1}, 1 is the unique designated value, and connectives are defined through the usual basic truth tables. Not all many-valued logics must have the four connectives mentioned before, in fact, classical logic can be defined in terms of two of those connectives ¬, ∧ (primitive connectives), and the other two (non-primitive) can be defined in terms of ¬, ∧. In case of a logic having the implication connective, it should preserve tautologies, in the sense that if x, x → y are tautologies, then y is also a tautology. This restriction enforces the validity of Modus Ponens in the logic. Since we will be working with several logics, we will use subindexes next to the connectives to specify to which logic they correspond, for example, ¬K corresponds to the connective ¬ of Kleene’s logic. In those cases where the given logic is understood from the context, we drop such subindexes. Numbers 0, 1, 2 and 3 are part of the semantics of logic studied in this paper and were chosen only for convenience. 51 Kleene’s 3-valued logic. The Kleene’s 3-valued logic, denote here by K, is defined in [5]. Kleene’s logic is a 3-valued logic with truth values in the domain D = {0, 1, 3}, where 3 is the only designated value1 . Conjunction and disjunction are defined as the min and max functions respectively, namely α∧β = min(α, β), and α ∨ β = max(α, β). The connectives →K and ¬K are defined according to the tables given in Table 1. It is important to mention that in this paper we use the implication of Kleene as defined by Avron in [5, p.11]. →K 0 1 3 x ¬K x 0 333 0 3 1 333 1 1 3 013 3 0 Table 1. Truth tables of connectives → and ¬ in Kleene’s logic. The basic 3-valued paraconsistent logic P AC. We consider the domain of the logic P AC as D = {0, 2, 3}, this logic is a 3-valued paraconsistent logic with 2 and 3 as designated values2 . The connectives ¬, ∧ and ∨ have the same properties as those of the logic K. Table 2 shows the truth tables of connectives ¬PAC and →PAC [5]. →PAC 0 2 3 x ¬PAC x 0 333 0 3 2 023 2 2 3 023 3 0 Table 2. Truth tables of connectives →, ¬ in P AC. Logic BL⊃ . This logic is a four-valued logic with truth values in the domain D = {0, 1, 2, 3} where 2 and 3 are the designated values. The connectives ∧ and ∨, as usually, correspond to the greatest lower bound (Glb) and the least upper bound (Lub), respectively. The connectives ¬ and → are defined according to the truth tables given in Table 3. →BL⊃ 0 1 2 3 x ¬BL⊃ x 0 3333 0 3 1 3333 1 1 2 0123 2 2 3 0123 3 0 Table 3. Truth tables of connectives → and ¬ in logic BL⊃ . 1 The reason for considering this domain is that these values and the behavior of its connectives coincide with part of the logic BL⊃ . 2 We take this domain with the purpose of P AC be a fragment of BL⊃ logic. 52 The logic BL⊃ is represented in Fig. 1, note that if we consider only the values 0, 1 and 3 (right part of figure 1) we obtain the Kleene’s logic while if we take the values 0, 2 and 3 (left part of figure 1) we have the P AC logic. Knowledge 3 2 1 0 True Fig. 1. Lattice logic BL⊃ . As A. Avron mentions in [2], BL⊃ is interlaced 3 and hence satisfies that 1 ∧ 2 = 0 and 1 ∨ 2 = 3. As a consequence of this result, we can take D = {1, 2}. However, for simplicity we use D = {0, 1, 2, 3} and from now on whenever we put D we will be referring to this set. For Theorem 2 in Section 2 we need the following recursive substitution property definition (on α). Definition 1. [15] Let α, β be formulas we define the proposition obtained by replacing all occurrences of an atom p in α by β as follows: ( α if α atomic and α 6= p α[β/p] = β if α = p (α1 α2 )[β/p] = α1 [β/p]α2 [β/p], where  is any of the binary connectives and α1 , α2 any formulas. (¬α)[β/p] = ¬α[β/p]. 1.2 The system HBL Let us consider HBL, a formal axiomatic theory for BL⊃ [2] formed by the primitive logical connectives: ¬, →, ∧ and ∨, and the logical constants 0, 1, 2 and 3. We also consider one logical connective defined in terms of the primitive ones: α ↔ β := (α → β) ∧ (β → α) the well-formed formulas are constructed, as usual, the axiom schemas are: 3 This means that each one of ∧, ∨, ⊗ and ⊕ is monotonic with respect to both ≤t and ≤k [2, Definition 2.2, p.3] 53 I1 α → (β → α) I2 (α → (β → γ)) → ((α → β) → (α → γ)) I3 ((α → β) → α) → α C1 (α ∧ β) → α C2 (α ∧ β) → β C3 α → (β → (α ∧ β)) D1 α → (α ∨ β) D2 β → (α ∨ β) D3 (α → γ) → ((β → γ) → (α ∨ β → γ)) N1 ¬(α ∨ β) ↔ ¬α ∧ ¬β N2 ¬(α ∧ β) ↔ ¬α ∨ ¬β N3 ¬¬α ↔ α N4 ¬(α → β) ↔ α ∧ ¬β and as the only inference rule: Modus Ponens α α→β β Logic BL⊃ is soundness and completeness with respect to this axiomatiza- tion. Theorem 1. [2, Section 3][Sound and Complete] Γ `BL⊃ α if and only if Γ |=BL⊃ α. 1.3 Klein group In group theory, the Klein group hG, ·i has several representations (in [9] we can see some of its representations), this group is formed by four elements G = {0, 1, 2, 3}, where each element is its own inverse and 0 is the neutral element. Table 4 shows the product of the elements of G. · 0123 00123 11032 22301 33210 Table 4. Product of G. One more motivation for studying BL⊃ logic is that it is very close to Klein group since as we can see in Theorem 4, the operation given in Table 4 can be expressed in terms of functions in logic BL⊃ . On the other hand, the applications of G are varied, as we mention in the Introduction, due to their characteristic property that each element is its own inverse. It is worth mentioning that it is not possible to build a group of three elements with such property, to see this fact, suppose that there is a group of 3 elements where each element is its own inverse; under this assumption it is possible to prove that the group has only two elements, this put in evidence the importance of extending the 3-valued logics to the 4-valued logics. 54 2 Some results about the representation of functions in BL⊃ logic In this section, we present some results on BL⊃ logic. But, above all, we focus our study on the presentation of a methodology for representing functions, from Dn to D. Remark 1. a) Logic BL⊃ satisfies Modus Ponens. Indeed, if I(α) ∈ {2, 3} and |= α → β, then I(β) ∈ {2, 3} . b) Any logic that has axioms I1, I2 and Modus Ponens as the only inference rule satisfies the hypothetical syllogism, i.e. α → β, β → θ ` α → θ. Particularly in BL⊃ , the hypothetical syllogism is satisfied. c) The deduction theorem is satisfied in BL⊃ , this means that if Γ, α |=BL⊃ β, then Γ |=BL⊃ α → β. d) The connective ↔BL⊃ introduced at the beginning of Section 1.2 defines an equivalence relation among formulas. It is reflexive, symmetric and transitive. e) BL⊃ is a genuine paraconsistent logic, namely, there are formulas α, β ∈ BL⊃ such that α, ¬α 6|=BL⊃ β and 6|=BL⊃ ¬(α ∧ ¬α). For verifying the first one α, ¬α 6|=BL⊃ β, it is enough to consider the value of 2 for α and 1 for β. For 6|=BL⊃ ¬(α ∧ ¬α) consider the value 1. f) BL⊃ is a paracomplete logic, this means that there exist some formula α in BL⊃ such that 6|=BL⊃ α ∨ ¬α, just consider the value 1. Definition 2. We say that the binary connective OP has the substitution prop- erty if by substituting equivalent parts we obtain equivalent propositions, this is if |= α1 OP α2 , then |= β[α1 /p] OP β[α2 /p], where p is an atom. The connective ↔ of logic BL⊃ does not satisfy the substitution property. Consider for instance α1 = γ → γ and α2 = θ → θ. Note that in this case |= α1 ↔ α2 (|= (γ → γ) ↔ (θ → θ)). To verify this, let I be any interpretation, then we have two cases: 1. I(θ) 6= 2 y I(γ) 6= 2, in this situation, I(α1 ↔ α2 ) = 3. 2. I(θ) = 2, o I(γ) = 2 then I(α1 ↔ α2 ) = 2. In both cases α1 ↔ α2 evaluates designated, therefore |= α1 ↔ α2 . On the other hand 2 β[α1 /p] ↔ β[α2 /p]. To see this, consider β = ¬p, I(γ) = 2 and I(θ) = 3, we have that I (¬(γ → γ) ↔ ¬(θ → θ)) = 0. Therefore, 2 ¬(γ → γ) ↔ ¬(θ → θ). Definition 3. Let α, β be formulas of BL⊃ , we define the connective ⇔ as follows: α ⇔ β := (α ↔ β) ∧ (¬α ↔ ¬β) Remark 2. It is not difficult to see that α ⇔ β is a tautology if and only if α and β have the same truth value. 55 Theorem 2 (Substitution). If |= α1 ⇔ α2 , then |= θ[α1 /p] ⇔ θ[α2 /p], where p is an atom. Sketch of proof. The proof is done by induction on the length of θ. 1. The atomic case is identical to the version in classical logic. 2. θ = ¬θ1 immediately by the definition of ↔ . 3. θ = θ1 ∧ θ2 it is derived from positive logic and De Morgan’s laws. 4. θ = θ1 → θ2 is obtained thanks to the axiom ¬(α → β) ↔ α ∧ ¬β. 5. θ = θ1 ∨ θ2 it is derived from case 2, 3 and De Morgan’s laws. The following result shows that if α is a semantical consequence of Γ in BL⊃ , then it is also a semantical consequence in Kleene and P AC. Theorem 3. [15] If Γ |=BL⊃ α, then Γ |=K α and Γ |=PAC α. Proof. We proceed by contrapositive. Assume that Γ 2K α, then exist a model M of Γ such that M (α) = 0 or M (α) = 1. Since 0 and 1 are not designated in BL⊃ we have to Γ 2BL⊃ α. Similarly, if we assume that Γ 2PAC α, then exist a model M of Γ such that M (α) = 0 which is not designated in BL⊃ . Therefore Γ 2BL⊃ α. The reciprocal of the previous theorem is not fulfilled. Consider the following counter-example. Let Γ = {p, ¬p} and α = q ∨ ¬q. Note that there is no truth value assignment in Kleene that makes Γ true. Then Γ |=K α by vacuity. On the other hand, the only truth value that models Γ in P AC is 2 and since q ∨ ¬q is a tautology in P AC we have to Γ |=PAC α. Finally, in BL⊃ 2 is the only values that models Γ but α is not a tautology, just consider the truth value 1 for q, so also α worth 1 that is not a designated value. Therefore, Γ 2BL⊃ α. 2.1 Expressing the operation of Klein group by means of function in logic BL⊃ To express the operation of Klein group in BL⊃ , we introduce some special functions as follows. Definition 4. For all x ∈ {0, 1, 2, 3} we define the connectives: t(x) := x ∧ (¬x → 0) f (x) := ¬x ∧ (x → 0) ⊥(x) := (¬x → 0) ∧ (x → 0) The reader can easily verify the behavior of these connectives, we use them to define functions that identify precisely each one of the values of BL⊃ , it means that, with the help of the connectives t, f and ⊥ of Definition 4, we define four functions that give 3 for a specific value of x and 0 in another case. Definition 5. Let gi : D −→ D, i ∈ {0, 1, 2, 3} given by: – g0 (x) = ¬⊥(x) ∧ f (x) 56 – g1 (x) = ⊥(x) – g2 (x) = ¬f (x) ∧ ¬(¬x → 0) – g3 (x) = t(x) ∧ ¬(x → 0) The truth table of each one of the functions gi , i ∈ {0, 1, 2, 3} is presented in Table 2.1. Note that for each i ∈ {0, 1, 2, 3} and x ∈ D : ( 3 x=i gi (x) = 0 x 6= i x g0 (x) x g1 (x) x g2 (x) x g3 (x) 0 3 0 0 0 0 0 0 1 0 1 3 1 0 1 0 2 0 2 0 2 3 2 0 3 0 3 0 3 0 3 3 Table 5. Functions g0 , g1 , g2 and g3 . Definition 6. Let fij : D × D −→ D, i, j ∈ {0, 1, 2, 3} be the function given by: ( 3 x = i, y = j fij (x, y) = gi (x) ∧ gj (y) = 0 in other case The functions fij allow us to place 3 in any position in Table 4. If we want to have any other value 0, 1 or 2, it is enough to take the conjunction of this function fij with a function that evaluates the desired value. The final representation of G The main objective is to build a two-variable function that models the pro- duct of G. Note that as we have mentioned, the functions fij of Definition 6 can be redefined to obtain any entry from Table 4 as shown below. Definition 7. Let fij : D × D −→ D, i, j, k ∈ {0, 1, 2, 3} be function given by: ( k k x = i, y = j fij (x, y) = gi (x) ∧ gj (y) ∧ k = 0 in other case To have better control, we introduce functions that allow us to represent each one of the lines of the product of G. Definition 8. Let hi : D × D −→ D, i ∈ {1, 2, 3, 4} be function given by: 57 0 1 2 3 h1 (x, y) = f00 (x, y) ∨ f01 (x, y) ∨ f02 (x, y) ∨ f03 (x, y) 1 0 3 2 h2 (x, y) = f10 (x, y) ∨ f11 (x, y) ∨ f12 (x, y) ∨ f13 (x, y) 2 3 0 1 h3 (x, y) = f20 (x, y) ∨ f21 (x, y) ∨ f22 (x, y) ∨ f23 (x, y) 3 2 1 0 h4 (x, y) = f30 (x, y) ∨ f31 (x, y) ∨ f32 (x, y) ∨ f33 (x, y) Each hi , i ∈ {1, 2, 3, 4} provides the i-th row of Table 4 and in the rest of entries gives 0 as shown in Table 6. h1 (x, y) 0 1 2 3 h2 (x, y) 0 1 2 3 0 0123 0 0000 1 0000 1 1032 2 0000 2 0000 3 0000 3 0000 h3 (x, y) 0 1 2 3 h4 (x, y) 0 1 2 3 0 0000 0 0000 1 0000 1 0000 2 2301 2 0000 3 0000 3 3210 Table 6. Functions h1 , h2 , h3 , h4 . Finally, for all x, y ∈ D the product of group is expressed by the function φ(x, y) = h1 (x, y) ∨ h2 (x, y) ∨ h3 (x, y) ∨ h4 (x, y). (1) As a summary, we describe in a general way the process of representing the operation of the Klein group. 1. Construction of unary functions gi ’s which provide 3 for a specific value and 0 otherwise. 2. With the help of the functions gi ’s, we build the functions of two variables fij to place 3 in a specific position of Table 4, and to place 0 in another case. Furthermore, we generalize these functions to obtain the exact value in each k product entry of G, this with the functions fij . k 3. Using the appropriate functions fij we express the operation of G. Theorem 4. There is a function of two variables given in the expression (1) such that it represents the Klein group. Proof. It follows immediately by the previous construction. k Remark 3. Functions fij can be generalized to functions of n-variables. This is: ( k k x1 = i1 , x2 = i2 ,..., xn = in fi1 ,...,in (x1 , ..., xn ) = 0 in other case. 58 Theorem 4 can be generalized and its proof is a generalization of the previ- ous construction. But, before to do it, consider the next example. Let B = {(0, 0, 0), (1, 1, 1), (0, 2, 0), (0, 3, 1)} ⊂ D3 , f : B −→ D be the function: ( 0 if x1 = x2 = x3 f (x1 , x2 , x3 ) = 2 if x1 = 0 y x2 6= 0 k Now let’s express f in terms of fij . We need to calculate f (0, 0, 0), f (1, 1, 1), f (0, 2, 0) and f (0, 3, 1), due to space limitations, here we just calculate f (1, 1, 1) and f (0, 2, 0), the two remaining terms can be calculated analogously. 0 f (1, 1, 1) = 0 = f1,1,1 (1, 1, 1) = fik22,i2 ,i2 (1, 1, 1), where i21 = i22 = i23 = 1 and k2 = 0. 1 2 3 2 f (0, 2, 0) = 2 = f0,2,0 (0, 2, 0) = fik33,i3 ,i3 (0, 2, 0), where i31 = i33 = 0, i32 = 2 and k3 = 2. 1 2 3 Therefore, f (x1 , x2 , x3 ) = fik11,i1 ,i1 (x1 , x2 , x3 ) ∨ fik22,i2 ,i2 (x1 , x2 , x3 ) ∨ fik33,i3 ,i3 (x1 , x2 , x3 ) 1 2 3 1 2 3 1 2 3 ∨fik44,i4 ,i4 (x1 , x2 , x3 ) 1 2 3 4 _ k = fill,il ,il (x1 , x2 , x3 ) 1 2 3 Theorem 5. Everyl=1function f : Dn −→ D, can be expressed in terms of the functions fik1 ,...,in . Furthermore, m _ f (x1 , ..., xn ) = fikll,...,il (x1 , ..., xn ); 1 n l=1 for some m ∈ N. 3 Conclusions and future work We have provided a methodology to represent functions from Dn to D using the connectives of BL⊃ . In particular, we express the binary operation that defines the Klein group. As future work, we could consider at least to lines of research. First, explore the possibility to express answer set programming (without strong negation) by using four valued logic instead of the actual three-valued Gödel logic. That goal seems to be direct. Then, by taking advantage of the four values, one should be able to express new useful operators. Second, consider extending the logic Four to fifth-valued logic, in a way that the new valued could represent the notion of ineffability with potential applica- tions in semi-automatic constructions of complex literature. 4 Acknowledgment We thank Arnon Avron and Graham Priest for answering our questions about their respective logics. 59 References [1] Edward A. Rietman, Robert L. Karp, and Jack A. Tuszynski. Re- view and application of group theory to molecular systems biology. urlhttp://tbiomedcentral.com/articles/10.1186/1742-4682-8-21, 2011. [2] Ofer Arieli and Arnon Avron. Reasoning with logical bilattices. Journal of Logic, Language and Information, 5(1):25–63, 1996. [3] Ofer Arieli and Arnon Avron. The value of the four values. Artif. Intell., 102(1), 1998. [4] Ofer Arieli, Arnon Avron, and Anna Zamansky. Ideal paraconsistent logics. Studia Logica, 99(1-3):31–60, 2011. [5] Arnon Avron. Natural 3-valued logics–characterization and proof theory. Journal of Symbolic Logic, 56(1):3–4, 03 1991. [6] Jean-Yves Beziau. Two genuine 3-valued paraconsistent logics. In Towards Paraconsistent Engineering, pages 35–47. Springer, 2016. [7] Jean-Yves Béziau, Walter Alexandre Carnielli, and Dov M Gabbay. Hand- book of paraconsistency. College publications, 2007. [8] Walter Alexandre Carnielli, Marcelo Coniglio, and Itala Maria Lof D’ottaviano. Paraconsistency: The logical way to the inconsistent. CRC Press, 2002. [9] Sunil K Chebolu and Ján Minác. Representations of the miraculous klein group. arXiv preprint arXiv:1209.4074, 2012. [10] Newton C. A. da Costa and Décio Krause. Remarks on the applications of paraconsistent logic to physics, December 2003. [11] Joke Meheus. An extremely rich paraconsistent logic and the adaptive logic based on it. In Diderik Batens, Chris Mortensen, Graham Priest, and Jean Paul Van Bendegem, editors, Frontiers of Paraconsistent Logic, page 98. Research Studies Press, Baldock, UK, 2000. [12] Hitoshi Omori and Toshiharu Waragai. Negative modalities in the light of paraconsistency. In The Road to Universal Logic, page 1. Springer, 2015. [13] Graham Priest. None of the above: The catuskoti in indian buddhist logic. In New Directions in Paraconsistent Logic, pages 517–527. Springer, 2015. [14] Graham Priest. Gödel’s theorem and paraconsistency, volume 1 of n. 2019. [15] Dirk van Dalen. Logic and structure (2. ed.). Universitext. Springer, 1989. 60