=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==
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