=Paper= {{Paper |id=Vol-2585/paper5 |storemode=property |title=Methodology to represent functions in logic BL⊃ |pdfUrl=https://ceur-ws.org/Vol-2585/paper5.pdf |volume=Vol-2585 |authors=Mauricio Osorio,Daniela Hernández-Grijalva,Alejandro Hernández-Tello |dblpUrl=https://dblp.org/rec/conf/lanmr/0001HH19 }} ==Methodology to represent functions in logic BL⊃== https://ceur-ws.org/Vol-2585/paper5.pdf
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