=Paper= {{Paper |id=None |storemode=property |title=Implication and biconditional in some three-valued logics |pdfUrl=https://ceur-ws.org/Vol-2264/paper10.pdf |volume=Vol-2264 |authors=Verónica Borja Macías,Alejandro Hernández-Tello |dblpUrl=https://dblp.org/rec/conf/lanmr/MaciasH18 }} ==Implication and biconditional in some three-valued logics== https://ceur-ws.org/Vol-2264/paper10.pdf
         Implication and Biconditional in some
                  Three-valued Logics

             Verónica Borja Macı́as and Alejandro Hernández-Tello

                      Universidad Tecnológica de la Mixteca,
                     Huajuapan de León, Oaxaca 69000, México
                         {vero0304,alheran}@gmail.com



       Abstract. The interpretation for ¬, ∨ and ∧ is quite standard in most
       of the best known three-valued logics. However, this is not the case for
       the connectives → and ↔, which are the relevant ones in order to study
       the notions of consequence and equivalence as well as translatability and
       synonymity. The purpose of this paper is to focus on the behavior of these
       last connectives in some Three-valued Logics, namely K3, LP, L3, G03 ,
       CG03 , L3Ag and L3Bg . Particularly we find equivalence connectives in
       logics L3, G03 , CG03 , L3Ag and L3Bg .

       Keywords: Implication · equivalence · many-valued logic.


1    Introduction

Aristotle restricted logic to statements, i.e. sentences that can be true or false,
as a result, Classical Logic is bivalent and it assumes that all statements are
actually true or false. Many logicians think that there are good reasons to avoid
such assumption and there is where Many-valued logics allowing for additional
truth values or truth value gaps appear. Many-valued logic has become a vast
field in logic and it continues growing as an independent discipline. One can find
excellent introductions to the topic as those in [11] or [6].
    Many-valued logics are a big family of non-classical logics. Though they reject
the bivalent principle, they accept the principle of truth-functionality, namely,
that the truth of a compound sentence is determined by the truth values of
its component sentences. Once one there are extra truth values for sentences
or they have run away of them, one must rethink the meaning of the logical
connectives as well as the definition of notions such as validity or consequence.
In both scenarios a huge amount of options arises; e.g. in case of a third option
apart from true and false is included, we have 33 = 27 different unary connectives
and 39 = 19683 binary connectives to select a new interpretation for the usual
connectives namely ¬, ∨ ∧ → and ↔.
    One can feel overwhelmed by such a bunch of different options. At the same
time, one can wonder if it is possible to select different connectives and that they
lead us to similar logics. In fact, even if two logics are defined using different lan-
guages or approaches they can have the same expressive power, (translatability




                                        114
2       V. Borja and A. Hernández-Tello.

equivalent logics) or even more, they can be the same logic (synonymous log-
ics).This problem is not an easy one, as it is revealed by Pelletier and Urquhart
in [9].
    The interpretation for ¬, ∨ and ∧ is quite standard, but it is not unique as
we will see in Section 4. However, this is not the case for the connectives →
and ↔, which are the relevant ones in order to study the notions of consequence
and equivalence as well as translatability and synonymity. The purpose of this
paper is to focus on the behavior of these last connectives in some of the most
important Three-valued Logics.


2   Basic Concepts

Let us start by introducing the syntax of the language considered in this article
as well as some definitions. We suppose that the reader has some familiarity
with basic concepts related to mathematical logic such as those given in the first
chapter of [7].
    We consider a formal language L built from: an enumerable set of atoms
(denoted as p, q, r, . . .), the set of atoms is denoted as atom(L) and the set of
connectives C = {∧, ∨, →, ¬}. Formulas are constructed as usual and will be
denoted as lowercase Greek letters. The set of all formulas of an language L
is denoted as F orm(L). Theories are sets of formulas and will be denoted as
uppercase Greek letters. There is no consensus on the definition of logic, but
two of the most accepted ones are that a logic can be considered as the set of
its theorems or defined instead by the valid inferences it accepts.

Definition 1. Given a language L, a logic L in the language L is a subset of
F orm(L).

   In this case the elements of a logic L are called theorems and the notation
`L ϕ is used to state that the formula ϕ is a theorem of L.

Definition 2. Given a language L, a logic L is a relation between sets of for-
mulas and formulas, i.e. a subset of P(F orm(L)) × F orm(L).

In this case the elements of a logic L are pairs, the valid inferences. The notation
Γ `L ϕ is used to state that the formula ϕ can be inferred from Γ in L. Whenever
it is clear by the context which logic you are referring to, the subscript will be
dropped.
    It is common to impose extra conditions to the previous definitions to define
a logic. For example in the context of Definition 1 is common to ask that the
set is closed under Modus Ponens (MP) and substitution. Meanwhile regarding
Definition 2 it is common to ask that the relation satisfies reflexivity, mono-
tonicity and transitivity. We take no position on this issue and we will consider
Definitions 1 and 2 equally valid.
    The usefulness of a logic depends on the available connectives in its language,
particularly important connectives are: implication, conjunction, disjunction and




                                      115
                Implication and Biconditional in some Three-valued Logics       3

negation. In the following definition we ask for some conditions on binary con-
nectives so they can be considered as conjunctions, disjunctions or implications
according to [1].

Definition 3. 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 Γ ` ϕ → ψ.

L is a semi-normal logic if it has at least one of this connectives, If the logic
has the three of them then it is called normal logic .

    Here some extra important notions on regard to the connectives behavior.

Definition 4. [5] Let `L be a logic whose language has some of the following
connectives ∧, ∨, → and ¬, then:

1. ¬ is a Classical Negation if Γ, ¬ϕ ` ψ and Γ, ¬ϕ ` ¬ψ imply that Γ ` ϕ.
2. ∧ is a Classical Conjunction if Γ, ϕ ∧ ψ ` ϕ, Γ, ϕ ∧ ψ ` ψ and Γ, ϕ, ψ `
   ϕ ∧ ψ.
3. ∨ is a Classical disjunction if Γ, ϕ ` ϕ ∨ ψ, Γ, ψ ` ϕ ∨ ψ and if Γ, ϕ ` σ
   and Γ, ψ ` σ then Γ, ϕ ∨ ψ ` σ.
4. → is a Classical implication  if Γ ` ϕ → (ψ
                                               → ϕ), if Γ ` ϕ and Γ ` ϕ →
    ψ imply that Γ ` ψ, and Γ ` ϕ → (ψ → σ) → (ϕ → ψ) → (ϕ → σ) .


3    Many-valued logics

The early notions of many-valued logics can be traced back to Boole, Peirce and
Vasiliev, however, first papers introducing many-valued logics formally are due
to Lukasiewicz and Post around 1920.
   The usual manner to define the many-valued logic is by means of a matrix.
Definition 5. Given a language L, a matrix is a structure M := hV, D∗ , F i:

1. V is a non-empty set of truth values (domain).
2. D is a subset of D (set of designated values).
3. F := {fc |c ∈ C} is a set of truth functions, with a function for each logical
   connective in L.

Definition 6. Given a language L, a valuation or an interpretation is a func-
tion t : atom(L) → V that maps atoms into elements of the domain.

   An interpretation t can be extended to all formulas by t̂ : F orm(L) → V as
usual, i.e. applying recursively the truth functions of logical connectives in F .
The interpretations allow us to define the notion of validity.




                                     116
4       V. Borja and A. Hernández-Tello.

Definition 7. Given a matrix M , we say that the formula ϕ is valid under the
interpretation t, if t̂(ϕ) ∈ D and we denote it by t |=M ϕ.
    In this case the validity depends on the interpretation, but if we want to find
the “logical truths” of the system then the validity should not depend on the
interpretation, in other words we have:
Definition 8. Given a matrix M , we say that a formula ϕ is a tautology in M
(or simply it is valid) if for every possible interpretation, the formula ϕ is valid
and we denote this by |=M ϕ.
    It is also possible to define a consequence relation by means of a matrix.
Definition 9. Given M , Γ and ϕ, a matrix, a theory and a formula respectively,
we say that ϕ is a consequence of γ in M if for any interpretation t, t |=M ϕ
whenever t |=M Γ .
    When one defines a logic L via a matrix M we have two cases. Using Defi-
nition 1 the set of theorems of the logic is defined as the set of tautologies that
are obtained from the matrix, i.e. `L ϕ iff |=M ϕ. On the other hand if we use
Definition 2 instead, then an inference Γ `L ϕ is valid if ϕ is a consequence of
Γ in M , i.e. Γ `L ϕ iff Γ |=M ϕ.
    Some extra important notions are those classifying the connectives behavior
as:
Definition 10. Let M = hV, D, F i be a matrix in the language L, A ⊆ V and
a1 , . . . , an ∈ V . An n-ary connective  in L is:
1. A-closed if a1 , . . . , an ∈ A implies ˜(a1 , . . . , an ) ∈ A.
                (a1 , . . . , an ) ∈ A implies a1 , . . . , an ∈ A.
2. A-limited if ˜
   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 11. [5] Let M = hV, D, F i be a matrix for the language L and D =
V \ D then:
1. ¬ ia a Neoclassical negation, when ¬p ∈ D iff p ∈ D.
2. ∧ is a Neoclassical conjunction, iff it is D-closed and D-limited.
3. ∨ is a Neoclassical disjunction, it is D-closed and D-limited.
4. → is a Neoclassical implication, when a1 → a2 ∈ D iff a1 ∈ D or a2 ∈ D.
Definition 12. [2] A multivalued operator ~ is a conservative extension of
a bi-valued operator if the restriction of ~ to the values of the bi-valued operator
coincide.
Definition 13. Given a bi-valued logic L1 and a multivalued logic L2 such that
the set of connectives of L1 is a subset of the connectives of L2 , L2 is a con-
servative extension of L1 if all the connectives in common are conservative
extensions.




                                           117
                 Implication and Biconditional in some Three-valued Logics        5

4     Three-valued logics

Many-valued logics, particularly three-valued logics have been one of the most
prolific family of non-classical logics since they formally show up around 1920.
Due to its high degree of plasticity, they have served as counterexamples, as
models to solve philosophical problems and have found many applications in
areas such as computer science. Consequently, it is valuable to continue studying
them. In this section we present some of the most important three-valued logics
by means of matrices that show the slight but important differences between
these logics. In all the cases the domain will be the set V = {0, 1, 2} where 0 is
identified with False, 2 is identified with True but the interpretation of the third
one, namely 1 will vary among systems.


4.1   Logic K3

The original three-valued logic by Kleene has an epistemological motivation. The
third logical value was designed to mark indeterminacy of some proposition at
a certain stage of scientific investigation. The matrix of K3 logic is given by:
M = hV, D, F i where: the domain is V = {0, 1, 2} and the set of designated
values is D = {2} and the set F of truth functions for connectives ∧, ∨, → and
¬ consists of the functions shown in Table 1. In this case K3 must be defined
as a logic according to Definition 2 due to the absence of tautologies since any
valuation which assigns the value 1 to each propositional variable sends any
formula into 1.


       f¬                  f∧ 0 1 2             f∨ 0 1 2             f→ 0 1 2
        0 2                 0 000                0 012                0 222
        1 1                 1 011                1 112                1 112
        2 0                 2 012                2 222                2 012

          Table 1. Truth functions of connectives ∧, ∨, → and ¬ in K3.




4.2   Logic LP

A popular paraconsistent logic is the logic LP (Logic of Paradox), introduced
by Asenjo in 1966. The idea behind LP is to take classical logics two-valued
semantics and extend it to a three-valued semantics, with truth values true,
false and paradoxical (identified here as 0, 2 and 1 respectively). We think of
the third truth value as meaning both true and false. The matrix of LP logic
is given by: M = hV, D, F i where: the domain is V = {0, 1, 2} and the set of
designated values is D = {1, 2} and the set F of truth functions for connectives
∧, ∨, → and ¬ consists of the same functions shown in Table 1. LP validates all
classical tautologies; however, it fails to validate all classical inferences.




                                      118
6      V. Borja and A. Hernández-Tello.

4.3   Logic L3

The matrix of L3 logic is given by: M = hV, D, F i where: the domain is V =
{0, 1, 2} and the set of designated values is D = {2} and the set F of truth
functions for connectives ∧, ∨, → and ¬ consists of the functions shown in Table
2. Truth tables for connectives ∧, ∨ and ¬ remain the same as for K3 and
LP. In this case the law of non-contradiction, ¬(ϕ ∧ ¬ϕ), is not valid in L3.
However, there are some classical tautologies that even can turn out false in L3:
¬(ϕ → ¬ϕ) ∨ ¬(¬ϕ → ϕ).


       f¬                 f∧ 0 1 2             f∨ 0 1 2             f→ 0 1 2
        0 2                0 000                0 012                0 222
        1 1                1 011                1 112                1 122
        2 0                2 012                2 222                2 012

          Table 2. Truth functions of connectives ∧, ∨, → and ¬ in L3.




4.4   Logic G03

In [3] Carnielli and Marcos define G03 as a paraconsistent logic and use it only
as a tool to prove that (ϕ ∨ (ϕ → ψ)) is not a theorem of Cω . In [8] Osorio
and Carballido make a detailed study of G03 . The matrix of G03 logic is given
by: M = hV, D, F i where: the domain is V = {0, 1, 2} and the set of designated
values is D = {2} and the set F of truth functions for connectives ∧, ∨, → and
¬ consists of the functions shown in Table 3.


       f¬                 f∧ 0 1 2             f∨ 0 1 2             f→ 0 1 2
        0 2                0 000                0 012                0 222
        1 2                1 011                1 112                1 022
        2 0                2 012                2 222                2 012

          Table 3. Truth functions of connectives ∧, ∨, → and ¬ in G03 .




4.5   Logic CG03

The logic CG03 is a paraconsistent logic that extends G03 . The logical matrix of
CG03 is given by V = {0, 1, 2}, D = {1, 2} and the truth functions are those of
G03 that can be found in the Table 3. In other words we obtain the matrix of
CG03 by adding 1 as designated value to the matrix of G03 .




                                     119
                Implication and Biconditional in some Three-valued Logics      7

4.6   Logic L3Ag
Genuine Paraconsistent logics L3A and L3B were defined in 2016 by Béziau
et al, including only three logical connectives, namely, negation disjunction and
conjunction. Afterwards Hernández-Tello et al, provide implications for both
logics and define the logics L3AG and L3BG in [5]. Logic L3AG and it is given
by a matrix given by V = {0, 1, 2}, D = {1, 2} and the truth functions can
be found in the Table 3. It is worth mentioning that the matrix of L3AG is
very close to the matrix of CG03 since the only differences are on the table of
disjunction, specifically ∧(1, 2) = 2 and ∧(2, 1) = 2, while in CG03 this table
correspond to the minimum as shown in Table 4.


       f¬                 f∧ 0 1 2            f∨ 0 1 2             f→ 0 1 2
        0 2                0 000               0 012                0 222
        1 2                1 012               1 112                1 022
        2 0                2 022               2 222                2 012

         Table 4. Truth functions of connectives ∧, ∨, → and ¬ in L3Ag .




4.7   Logic L3Bg
The matrix of L3BG differs from the one for L3Ag only in the connectives ¬
and ∨ as shown in Table 5.


       f¬                 f∧ 0 1 2            f∨ 0 1 2             f→ 0 1 2
        0 2                0 000               0 012                0 222
        1 1                1 021               1 112                1 022
        2 0                2 012               2 222                2 012

         Table 5. Truth functions of connectives ∧, ∨, → and ¬ in L3Ag .




4.8   Some remarks
We have presented seven different logics. Though they share some connectives,
their properties are quite different. In the following theorems we summarize
some of these properties. Proofs are straightforward from the interpretation of
the connectives.
Theorem 1. Let L ∈ {K3, LP, L3, G03 , CG03 , L3Ag , L3Bg } then L is a con-
servative extension of Classical Logic.
Proof. Given a logic L according to Definition 13 it is necessary to verify that
each of the connectives ¬, ∨, ∧ and → in the corresponding logic are conservative




                                     120
8       V. Borja and A. Hernández-Tello.

extensions of the classical ones. If we identify 0 as F (False) and 2 as T (True)
and we ignore all the entries that involve the third value leaving them as ?, for
any of the cited logics we obtain the truth tables in Table 6 which correspond
to the classical truth tables in all cases.


       f¬                 f∧ F ? T              f∨ F ? T               f→ F ? T
       F T                F F?F                 F F?T                   F T?T
        ? ?                ? ? ??                ? ? ??                 ? ? ??
       T F                T F?T                 T T?T                   T F?T

           Table 6. Truth tables of restrictions of three valued operators




Theorem 2. The logics K3, LP and G03 are semi-normal logics and L3, CG03 ,
L3Ag and L3Bg are normal logics.
Proof. In all the cases it is enough to check the truth tables for all the connec-
tives. The connective → is not an implication according to Definition 3 for those
logics that said to be semi-normal, for example for logic LP it is enough to check
the case when the antecedent is 1 and the consequent is 0.
   On the other hand if we focus on the neoclassicality of the connectives we
have the following:
Theorem 3. Most of the connectives ∧, ∨, → and ¬ are neoclassical in the
logics in B = {K3, LP, L3, G03 , CG03 , L3Ag , L3Bg } as depicted in Table 7 (a
check mark in the table establishes the respective connective is neoclassical in the
corresponding logic, meanwhile an × mark means the connective is not neoclas-
sical).
                                  L3Ag
                                  L3Bg
                                  CG03
                                  LP
                                  K3


                                  G03
                                  L3




                               ¬××× X × × ×
                               ∨XXX X X X X
                               ∧XXX X X X X
                               →×X× × X X X
              Table 7. Neoclassicality of connectives ¬, ∧, ∨ and →.




Proof. In all the cases the truth tables give the evidence or the counterexample
of the respective property. For example → is not a neoclassical implication nor
for K3, L3 neither for G03 . In all cases it is enough to check the case when the
antecedent is 1 and the consequent is 0.




                                      121
                 Implication and Biconditional in some Three-valued Logics           9

There is also a close relation between the notions of connective, neoclassicla
connective and classical connective as stated by the following propositions.

Proposition 1. [4] Neoclassical connectives define classical connectives, i. e. if
~ is a connective then if it is a neoclassical connective, it is a classical connective
as well.

Proof. Let see the case of implication, the rest of the proofs are analogous. Let
ϕ and ψ be two formulas and let rightarrow be a neoclassical implication. We
will verify that each of the conditions required to be a classical implication is
fulfiled.
 – Suppose that ϕ → (ψ → ϕ) is not designated for some valuation v. Since
   → is neoclassical, then v(ϕ) ∈ D and v(ψ → ϕ) ∈   / D. The last part implies
   that v(ϕ) ∈/ D, which leads us to a contradiction, then ϕ → (ψ → ϕ) must
   be designated.
 – Let suppose that Γ ` ϕ and Γ ` ϕ → ψ, then for any valuation that models
   Γ it also models ϕ and ϕ → ψ, since → is neoclassical then that valuation
   also models ψ as a result Γ ` ψ.
 – Suppose that (ϕ → (ψ → σ)) → ((ϕ → ψ) → (ϕ → σ)) is not designated
   for some valuation v. Since → is neoclassical then v(ϕ → (ψ → σ)) ∈ D and
   v((ϕ → ψ) → (ψ → σ)) ∈   / D and that v(ϕ), v(ψ) ∈ D and v(σ) ∈  / D, which
   leads us to a contradiction, then (ϕ → (ψ → σ)) → ((ϕ → ψ) → (ϕ → σ))
   must be designated.

Proposition 2. [4] A conjunction (disjunction or implication) defines a classi-
cal conjunction (disjunction or implication).

    The proofs of previous proposition is based on the properties of consequence
relations. This lead us to the following theorem.

Theorem 4. Most of the connectives ∧, ∨ and → are classical in the logics in
B as depicted in Table 8.
                                   L3Ag
                                   L3Bg
                                   CG03
                                   LP
                                   K3


                                   G03
                                   L3




                                ∨XXX X X X X
                                ∧XXX X X X X
                                →××X X X X X
                 Table 8. Classicality of connectives ¬, ∧, ∨ and →.




    As a final remark from Theorems 2, 3 and 4 we can see that the converse
of Proposition 1 is not valid and notions of connective, classical connective and
neoclassical connective do not agree.




                                       122
10      V. Borja and A. Hernández-Tello.

5    Implication and Validity


The existence of a third truth value also forces us to revise the relationship
between implication and validity. Some of the principles stated for granted in
classical logic are anymore acceptable in three-valued logics.
    K3 is a semi-normal logic, in this case the connective → is not a neoclassi-
cal connective nor a classical one. Apart from Modus Ponens any of the usual
properties regarding implication is satisfied.
   In particular in LP, Modus Ponens fails, it can be seen by making p = 1 and
q = 0. In that case both p and p → q have designated values (both are 1), but
the conclusion is 0. But LP is a very simple and intuitive proposal. Various ways
around the problem have been proposed, see [10] for more details.
    Logic L3 is quite similar to K3 in fact the unique difference is in its definition
of implication in that ”1 implies 1” is 2. This small change in the truth table lead
us to a completely different logic that has a lot of classical theorems, but not all
of them, e.g. law of excluded middle, ϕ ∨ ¬ϕ, and the law of non-contradiction,
¬(ϕ ∧ ¬ϕ).
   Though G03 , CG03 , L3Ag and L3Bg share the truth table for →, which agrees
with implication of the well known three-valued logic of Gödel, the behavior of
G03 differs from the others since it has only one designated value.
    Several principles, rules and theorems made the boundary between implica-
tion and validity indistinguishable. Let us focus in some of them such as:


 – Identity Principle (IP ` ϕ → ϕ),
 – Modus Ponens (MP ϕ, ϕ → ψ ` ψ )
 – Deduction Theorem (DT If Γ, ϕ ` ψ then Γ ` ϕ → ψ)
 – Thinning Principle (TP ` ϕ → (ψ → ϕ))


Most of the many-valued logics we study are paraconsistent logics, in the sense
that at least one of the following formulations of the principle of non contradic-
tion fails.


 – Non Contradiction (NC Γ ` ¬(ϕ ∧ ¬ϕ) )
 – Explosion by Contradiction (EC Γ, ϕ, ¬ϕ ` ψ)


And some of them are genuine paraconsistent logics, i. e. that both NC and EC
fail. In Table 9 it is possible to observe which of the studied properties hold in
each logic.




                                       123
                 Implication and Biconditional in some Three-valued Logics        11




                                                 L3Ag
                                                 L3Bg
                                                 CG03
                                                 LP
                                                 K3


                                                 G03
                                                 L3
                    Property
                 IP ` ϕ → ϕ                   ×XX X X X X
                MP ϕ, ϕ → ψ ` ψ               X×× X X X X
                DT If Γ, ϕ ` ψ then Γ ` ϕ → ψ × X X × X X X
                TP ` ϕ → (ψ → ϕ)              ×XX X X X X
                EC ϕ, ¬ϕ ` ψ                  X×× X × × ×
                NC ` ¬(ϕ ∧ ¬ϕ)                ×XX X X × ×
       Table 9. Properties of some three-valued logics paraconsistent logics.




6   Biconditional and Substitution

Up to now we have used matrices whose language includes ¬, ∧, ∨ and →, but
those matrices can be extended by a new connective, ↔, either as a primitive
connective or as an abbreviation in terms of the primitive ones. We are familiar
with the classical definition of ↔ using → and ∧, ϕ ↔ ψ =df (ϕ → ψ)∧(ψ → ϕ).
However, as we saw in the previous section the behavior of the implication in
our set of logics is varied and conjunction also vary at least in L3Ag and L3Ag .
   Considering the classical definition of ↔ using → and ∧, ϕ ↔ ψ =df (ϕ →
ψ) ∧ (ψ → ϕ) and the → connective of each logic we obtain that it is not an
equivalence relation:


          f↔ 0 1 2          f↔ 0 1 2           f↔ 0 1 2           f↔ 0 1 2
           0 210             0 210              0 200              0 200
           1 111             1 121              1 021              1 022
           2 012             2 012              2 012              2 022

          K3, LP               L3             G03 , CG03          L3Ag
                                                L3Bg
                     Table 10. Truth functions of connective ↔.


   We are particularly interested in logics whose biconditional connective corre-
sponds to equality. As stated in the following propositions, it is possible to define
an equivalence connective between formulas by means of the binary connective
⇔ as follows.

Proposition 3. In L3 there is an equivalence connective, namely:
                                                         
                 ϕ ⇔ ψ =df ¬ ¬¬(ϕ ↔ ψ) → ¬(ϕ ↔ ψ)

Proposition 4. In G03 and CG03 there is an equivalence connective, namely:

                              ϕ ⇔ ψ =df ¬¬(ϕ ↔ ψ)




                                       124
12      V. Borja and A. Hernández-Tello.

Proposition 5. In L3Ag there is an equivalence connective, namely:
                                                                  
      ϕ ⇔ ψ =df ¬ (ϕ → ψ) ∧ ¬(ψ → ϕ) ∧ ¬ (ψ → ϕ) ∧ ¬(ϕ → ψ)
Proposition 6. In L3Bg there is an equivalence connective, namely:
                                     ϕ ⇔ ψ =df
                                                                                    
¬ (ϕ → ψ) ∧ (ϕ → ψ) ∧ ¬(ψ → ϕ) ∧ ¬(ψ → ϕ) ∧ ¬ (ψ → ϕ) ∧ (ψ → ϕ) ∧ ¬(ϕ → ψ) ∧ ¬(ϕ → ψ)

   The propositions follows directly from the truth tables of the connectives
involved in the definition and in Table 11 one can find the truth table for ⇔
according to their definition.


                                      f↔ 0 1 2
                                       0 200
                                       1 020
                                       2 002
        Table 11. Truth functions for ⇔ in L3, G03 , cG03 L3AG and L3BG



Definition 14. [9] Let ↔ be a connective in a matrix M = hV, D, F i, we say
that M is an algebraic matrix if it satisfies the condition that for any elements
a, b ∈ V , a ↔ b ∈ D iff a = b.
Let B 0 be the set of logics containing L3, G03 , CG03 L3AG and L3BG . As a result
of the previous propositions and definition we obtain the following theorem:
Theorem 5. The matrices for L3, G03 , CG03 L3AG and L3BG are algebraic
matrices.
If M is an algebraic matrix, then we can think of the elements of the algebra
formed by hV, F i as propositions, and of the designated elements in D as the
true propositions. Then an algebraic matrix is a matrix in which equivalent
propositions are identified. Algebraic matrices are an important tool to define
and identify notions such as translatable equivalent logics or canonical models
(see [9]).
    Another benefit of the equivalence connective ⇔ is that the substitution of
logical equivalents, also known as the replacement theorem, holds.
Definition 15. Let σ1 = {p/ϕ} and σ2 = {p/ψ} be two substitutions in a logic
L, logic L satisfies substitution of logical equivalents if `L ϕ ⇔ ψ implies that
for any formula ρ it holds that `L σ1 (ρ) ⇔ σ2 (ρ).
Theorem 6. The replacement theorem holds in L3, G03 , CG03 L3AG and L3BG .
Proof. L For L ∈ {L3, G03 , CG03 L3AG , L3BG } if `L ϕ ⇔ ψ, then for any
interpretation t in L, t̂(ϕ) = t̂(ψ) and due to the recursive definition of t̂, we have
that t̂(σ1 (ρ)) = t̂(σ2 (ρ)) for any interpretation, which means that `L σ1 (ρ) ⇔
σ2 (ρ).




                                       125
                 Implication and Biconditional in some Three-valued Logics          13

The theorem states that, if any part of a formula is replaced by an equivalent
of that part, the resulting formula and the original are also equivalents in the
underlying logic. Such replacements need not be uniform.


7    Conclusions
The interpretation for connectives → and ↔ in many-valued logics is not stan-
dard and it is important to study them since they are the relevant connectives
in order to define notions of consequence and equivalence as well as many oth-
ers related to this like translatability and synonymity. We selected seven of the
most important Three-valued Logics namely, K3, LP, L3, G03 , CG03 , L3AG ,
L3BG and analyzed notions of classicality and neoclassicality of connective →
as well as its behavior with respect to some principles, rules and theorems that
involves this connective. After that we look for an equivalence connective for
each of the presented logics obtaining that in five of them this is possible, which
has interesting consequences.


References
 1. Arieli, O., Avron, A.: Three-valued paraconsistent propositional logics. In: New
    Directions in Paraconsistent Logic, pp. 91–129. Springer (2015)
 2. Beziau, J.Y., Franceschetto, A.: Strong three-valued paraconsistent logics. In: New
    directions in paraconsistent logic, pp. 131–145. Springer (2015)
 3. Carnielli, W.A., Marcos, J.: A taxonomy of C-systems. In: Paraconsistency: the
    logical way to the inconsistency, pp. 1–94. Marcel Dekker, New York (2002)
 4. Hernández-Tello, A.: Lógicas Paraconsistentes Genuinas. Ph.D. thesis, Benemérita
    Universidad Autónoma de Puebla (2018)
 5. Hernández-Tello, A., Arrazola Ramı́rez, J., Osorio Galindo, M.: The pursuit of an
    implication for the logics L3A and L3B. Logica Universalis 11(4), 507–524 (2017).
    https://doi.org/10.1007/s11787-017-0182-3
 6. Malinowski, G.: Many-valued Logics. Oxford logic guides, Clarendon Press (1993)
 7. Mendelson, E.: Introduction to mathematical logic. CRC press (2009)
 8. Osorio Galindo, M., Carballido Carranza, J.L.: Brief study of G’3 logic. Journal of
    Applied Non-Classical Logics 18(4), 475–499 (2008)
 9. Pelletier, F.J., Urquhart, A.: Synonymous logics. Journal of Philosophical Logic
    32(3), 259–285 (2003). https://doi.org/10.1023/A:1024248828122
10. Thomas, N.: LP=>: Extending LP with a strong conditional operator. arXiv
    preprint arXiv:1304.6467 (2013)
11. Urquhart, A.: Many-valued Logic, pp. 71–116. Springer Netherlands, Dordrecht
    (1986). https://doi.org/10.1007/978-94-009-5203-4 2




                                       126