{'fraction_non_alphanumeric': 0.053135593220338985, 'fraction_numerical': 0.01944915254237288, 'mean_word_length': 3.8883595691797845, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 6, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Belnap-Dunn Semantics for the Variants of BN4 and E4 which Contain Routley and Meyer’s Logic B

The logics BN4 and E4 can be considered as the 4-valued logics of the relevant conditional and (relevant) entailment, respectively. The logic BN4 was developed by Brady in 1982 and the logic E4 by Robles and Méndez in 2016. The aim of this paper is to investigate the implicative variants (of both systems) which contain Routley and Meyer’s logic B and endow them with a Belnap-Dunn type bivalent semantics.


Introduction
Belnap-Dunn semantics (BD-semantics) was originally introduced by means of the well-known logic B4 developed by Belnap and Dunn to treat inconsistent and incomplete information [cf. 5,6,9,10]. According to this semantics, there is the possibility of assigning T , F , both T and F or neither T nor F to a formula (T represents truth and F represents falsity). The logic B4 is equivalent to Anderson  Brady defined in 1982 the system BN4 [cf. 7], a logic built upon the matrix MBN4 which is also a modification of the matrix MSm4 referred to above. This system is closely related to both Belnap and Dunn's logic B4 and Routley and Meyer's logic B. On the one hand, BN4 can be considered a strengthening of B4 obtained by implicatively expanding the latter. On the other hand, the logic BN4 was first developed by taking as the starting point the axiomatization of B, as Brady himself stated. Therefore, BN4 can also be seen as a 4-valued extension of Routley and Meyer's logic B. As a matter of fact, even though it is tempting to read BN4 as B(oth) and N(either) 4-valued logic, the label was chosen by Brady because "the system contains the basic system B of Routley et al. 1982, Chapter 4, and has a characteristic 4-valued matrix set, one of the values being 'n', representing neither truth nor falsity" [cf. 7, p. 32, note 1]. BN4 may be seen as an interesting 4-valued extension of B since Meyer et al. maintain that "BN4 is the correct logic for the 4-valued situation where the extra values are to be interpreted in the both and neither senses" [14, p. 25] and according to Slaney, BN4 has the truth-functional implication most naturally associated with the logic FDE referred to above (and equivalent to B4; cf. [22, p. 289]). Moreover, the system BN4 is a central non-classical logic not only due to its relation with the family of relevant logics but also because of its position among other important many-valued logics. In particular, the "strong implication" of the bilattice logic GLB ⊃ [cf. 2,3] of considerable importance in artificial intelligence is actually the conditional of BN4 [cf. 13,Appendix].
The logic E4 is built upon a modification of Brady's matrix MBN4 and was developed by Robles and Méndez as a companion to the system BN4 worthy of consideration [cf. 18]. They believe that E4 is related to BN4 in a similar way to which Anderson and Belnap's logic of entailment E is related to the system R [cf. 1 about the logics E and R]. In this sense, the system E4 could be understood as the 4-valued entailment counterpart to the 4-valued relevant conditional presented in BN4.
In the conclusions of [18], Robles and Méndez suggest that E4 might not be the only alternative to BN4 and set out six different tables for f → which could be of interest. I will investigate the logics built upon these tables and prove that these matrices are the only implicative variants of MBN4 and ME4 that verify Routley and Meyer's logic B (cf. §3; they also verify FDE since B is a proper extension of FDE). In that sense, we will talk about the class of all implicative expansions of B4 verifying B while maintaining the conditional structure of MBN4 or ME4. The aim of this paper is to display the systems built upon these six alternative tables for f → and endow them with a Belnap-Dunn semantics in order to investigate whether any of these tables can advantageously substitute those of MBN4 and ME4. The results also contribute to pursue further investigation on implicative expansions of FDE 1 , which is well-known to be a core non-classical system among many-valued and relevant logics [cf. 15 and references therein].
The structure of the paper is now explained. In Section 2, Belnap and Dunn's matrix MB4 is defined while in Section 3, the six implicative variants of MBN4 and ME4 are displayed and the fact that they are the only ones of their kind verifying Routley and Meyer's logic B is proved. In Section 4, a basic sublogic (labeled "b4") contained in all the systems developed upon the previous matrices (including BN4 and E4) is presented and some of its properties are proved. In Section 5, all the logics characterized by those matrices (let them be called Ltilogics) are axiomatized in a Hilbert-style way as extensions of b4. In Section 6, each Lti-logic is endowed with a Belnap-Dunn semantics and the soundness theorems are proved. In Section 7, I display the extension and primeness lemmas which will be useful in the completeness theorem proved later, in Section 8. Finally, in Section 9, some properties of Lti-logics are explained: Lti-logics have the quasi-relevance property [1, p. 417, Proposition 9.4 of this paper] and their characteristic matrices are natural implicative expansions 2 of MB4 (i.e., FDE; cf. Corollary 9.12) among other related properties.

The matrix MB4
In this section, the matrix characteristic of Belnap and Dunn's logic B4, MB4 3 , will be presented. First of all, some basic notions will be defined.
Definition 2.1 (Languages). The propositional language consists of a denumerable set of propositional variables (P) p 0 , p 1 , . . . , p n , . . . and some or all of the following connectives → (conditional), ∧ (conjunction), ∨ (disjunction), ¬ (negation). The biconditional (↔) and the set of wffs (F ) are defined in the customary way. A, B (possibly with subscripts 0, 1, . . . , n), etc. are metalinguistic variables. 1 In [15], some of the most well-studied implicative expansions of the logic FDE are briefly explained, including BN4. In the conclusion of the paper, Omori and Wansing mention some interesting topics for further research, including new expansions of FDE and axiomatizations of relevant logics à la American plan.
2 I follow Tomova's notion of natural implication as it has been redefined by Robles and Méndez (cf. [23,p. 175] and [19, p. 2, note 2]). 3 By this label, I will refer to the matrix presented in [5,6,10], which is characteristic of the logic FDE. Definition 2.2 (Logics). A logic L is a structure L, ⊢ L where L is a propositional language and ⊢ L is a (proof-theoretical) consequence relation defined on L by a set of axioms and a set of rules of derivation. The notions of proof and theorem are understood as it is customary in Hilbert-style axiomatic systems (Γ ⊢ L A means that A is derivable from the set of wffs Γ in L; and ⊢ L A means that A is a theorem of L). Definition 2.3 (Extensions and expansions of a propositional logic L). On the one hand, let L and L ′ be two propositional languages. L ′ is a strengthening of L if the set of wffs of L is a proper subset of the set of wffs of L ′ . On the other hand, let L and L ′ be two logics built upon the propositional languages L and L ′ , respectively. Furthermore, suppose that every axiom of L is a theorem of L ′ and all primitive rules of inference of L are provable in L ′ . Then, L ′ is an extension of L if L and L ′ are the same propositional language; and L ′ is an expansion of L if L ′ is an strengthening of L. An extension L ′ of L is a proper extension if L is not an extension of L ′ . Definition 2.4 (Logical matrix). A (logical) matrix is a structure V, D, ̥ , where (1) V is a (ordered) set of (truth) values; (2) D is a non-empty proper subset of V (the set of designated values); (3) ̥ is the set of n-ary functions on V such that for each n-ary connective c (of the propositional language in question), there is a function f c ∈ ̥ such that f c : V n → V.

Implicative variants of MBN4 and ME4 which verify Routley and Meyer's logic B
On the one hand, Brady developed the system BN4 as a 4-valued extension of B [cf. 21,Chapter 4]. On the other, the system E4 was presented by Robles and Méndez [18] as a companion of BN4 worthy of consideration. As stated by them, E4 is the 4-valued entailment counterpart to the 4-valued relevant conditional represented in BN4. However, they also pointed out that E4 may not be the only interesting alternative to BN4. As a matter of fact, they suggested that there would be at least six other interesting alternatives to it. The aim of this section is to present these matrices and prove that they are the only ones (of their kind) verifying Routley and Meyer's basic logic B.
I start by displaying the matrices upon which logics BN4 and E4 are built. On the other hand, the notions of interpretation, consequence and validity in MBN4 and ME4 are understood according to Definition 2.5.
As it has been mentioned above, Robles and Méndez asserted that E4 may not be the only interesting alternative to BN4. In this sense, they suggested that the matrices built upon the following six implicational tables are the only implicative variants of MBN4 and ME4 that verify Routley and Meyer's basic logic B: The label Mti (1 i 8) will be used to refer to the matrix characterized by the implicative table ti. 4 It is worth underlining that the matrices characterized by the expansions of MB4 with those tables, together with MBN4 and ME4, are the only ones which satisfy B while preserving one of the following general structures (i.e., either BN4 or E4 implicative matrix structure): Now, suppose that the entries recorded in the tables above are fixed and the blank spaces can be filled with any truth-value from V (cf. Definition 2.6). Next, we will prove that MBN4, ME4 and the matrices characterized by the rest of the implicative tables shown above (i.e., t2-t4 and t6-t8) are the only ones verifying B. Proof. The fact that the rules and axioms of B are valid in Mti (1 i 8) can be easily proved with the help of a tester [cf. 12]. However, we also want to specify the reasons why those matrices are the only possible ones (having one of those implicative structures) that verify B. The method will consist in constraining the possibilities for blank spaces in such a way that the validity of (firstly) the rules and (then) the axioms of B is preserved. (1) In order to make the rule MP valid, the following possibilities have to be non-designated: . Once we have limited the possibilities of blank spaces according to (1), we take these results into account and keep limiting possibilities until the validity of the rules and axioms of B is preserved. (2) To validate the rule contraposition, the succeeding possibilities need to take a non-designated value: Likewise, the restriction of the values resulting from the following possibilities to 0 is needed to preserve prefixing or suffixing rules: . According to the points made so far, our implicative structures will be restricted as shown below: 5 The previous restrictions are still not sufficient for our matrices to validate the prefixing and suffixing rules, let alone every theorem of B. Thus, the restrictions just remarked will be separately analyzed from now on. Let us start with BN4-type implicational  It would be easy to verify that if any of the restrictions remarked above is not followed, the resulting implicational tables will fail to verify some rules (or theorems) of B. For instance, let us skip restriction (2). Then, let f → (3, 2) ∈ D be the case. For any distinct propositional variables p and q, there is an interpretation I such that I(p) = 3 and I(q) = 2. Therefore, the rule of contraposition will fail since we have

The basic logic b4 and its properties
Before defining the eight logics determined by each Mti (1 i 8), it will be useful to define the logic b4. b4 is a new system contained in all the logics we are going to define in this paper and serves a mere instrumental purpose. 6 The label b4 is intended to abbreviate "basic logic included in every variant of BN4 or E4 which contain Routley and Meyer's logic B". In what follows, the basic logic b4 is defined and some of its properties are proved.
Definition 4.1 (b4). The logic b4 is axiomatized with the following axioms and rules of inference.
Axioms: Proposition 4.3. The following theorems are derivable in b4:
In the following lines, I will introduce the notion of a Eb4-theory and the types of Eb4-theories of interest in this paper in order to prove some predicable properties of both b4-theories and Eb4-theories. By the label EL, I will refer to an extension (or an expansion, as the case may be) of the logic L (cf. Definition 2.3).
Definition 4.4 (Eb4-theories). Let L be an Eb4-logic. An L-theory T is a set of wffs closed under adjunction (Adj) and provable L-entailment (L-ent). That is to say, a set of wffs is closed under Adj iff, whenever A, Definition 4.5 (Types of Eb4-theories). Let L be an Eb4-logic and T be an L-theory. We set (1) T is prime iff, for wffs A and B, whenever A ∨ B ∈ T , then either A ∈ T or B ∈ T ; (2) T is regular iff T contains all theorems in L; (3) T is trivial iff it contains every wff; (4) T is aconsistent (consistent in an absolute sense) iff T is not trivial; (5) T is empty iff it contains no wff.
Immediate by A7 and A8 and the fact that L-theories for Eb4-logics are closed by L-entailment we obtain: Lemma 4.7. Let L be an Eb4-logic and T be a prime L-theory. Then,     A ∨ A)) and the fact that T is fully regular (i.e., closed under dCON, dPREF, dSUF and dCTE, respectively for each case). Cases (5)-(6): by hypothesis, T is fully regular (therefore closed under MP) and by the fact that T is closed under CON and SUF (given what has already been proved in cases (1) and (3)), respectively for each case.
Lemma 4.11. Let L be an Eb4-logic and T be a prime full regular Ltheory. 8 Then, A → B ∈ T iff either A / ∈ T or B ∈ T and either ¬A ∈ T or ¬B / ∈ T .
Proof. (a) (⇒): Suppose (1) A → B ∈ T and, by reductio, (2i) (A ∈ T and B / ∈ T ) or (2ii) (¬A / ∈ T and ¬B ∈ T ). If we suppose (2i), given that T is closed under MP, we get B ∈ T , which is impossible. Let us suppose then (2ii). We will get ¬A ∈ T since T is closed under MT (cf. Proposition 4.10). But this is also impossible. 9 (b) (⇐): Suppose 8 We do not actually need our theories to be fully regular in order to prove this lemma, but we do need them to be regular and closed under MP and MT at least. However, being closed under MP and MT also requires being closed under dMP and dCON for some of the logics considered in this paper.
9 Subcases (2i) and (2ii) could be also proved by means of the corresponding axioms instead of MP and MT rules. However, since only some of the logics we are considering in this paper validate those axioms (cf. Definition 5.1), I will use the rules to generalize the proof as much as possible.
(1) (A / ∈ T or B ∈ T ) and (¬A ∈ T or ¬B / ∈ T ). Four options should be considered: In cases (1i) and (1ii), we obtain A → B ∈ T by axioms A9 and A10, respectively, and the fact that T is prime. Similarly, case (1iii) is solved by A11 and the fact that T is a prime regular L-theory. Suppose now case (1iv) B ∈ T and ¬A ∈ T . Moreover, let us suppose (2) A → B / ∈ T by reductio. Then, given that T is regular, we get (3)

Lemma 5.2 (Negated conditionals in Lti-logics). Let L be an ELti-logic,
where Lti refers to one of the extensions of b4 displayed in Definition 5.1 and let T be a prime and fully regular L-theory. We have: Proof. This proof is similar to that of Lemma 4.11. 10 Therefore, it suffices to prove one case as example and provide a brief outline for the others. Let us prove the case of ELt6-logics. 10 A couple of axioms from the list above are not used in this proof: A16 and A17 (i.e., modus ponens and modus tollens axioms). However, those axioms could have been used in the proof of Lemma 4.11 (instead of their corresponding rules) for those Lti-logics which validate them, as it was already mentioned in that Lemma.

Belnap-Dunn semantics for the Lti-logics
In this section, a Belnap-Dunn semantics for the Lti-logics is developed. I start by defining the notions of Lti-models, Lti-consequence and Ltivalidity.  F ∈ I(B)). F ∈ I(B)). The following proposition proves that consequence relations Mti (cf. Definition 2.5 and Proposition 3.2) and Lti (cf. Definition 6.2) are coextensive. Then, the soundness theorem will follow immediately. On the other hand, given a Lti-interpretation I ′ , the Mti-interpretation I corresponding to I ′ can be defined in a similar way with analogous results.

Lt8-models: (5b) F ∈ I(A → B) iff (F / ∈ I(A) & T / ∈ I(B)) or (T ∈ I(A) &
Being the latter stated, the proof follows easily by Proposition 3.2 and Definitions 2.5, 2.6 and 6.2. Now, soundness is proved. Proof. (1) Given one of the considered Lti-logics, it is easy to check that the rules preserve Mti-validity, whereas the axioms of Lti are assigned either 3 or 2 by any Mti-interpretation I. Therefore, if Γ ⊢ Lti A, then Γ Mti A. As for (2), it is immediate given (1) and Proposition 6.3. Finally, if Γ is the empty set, the proof is similar. 11

Extension and primeness lemmas
In the present section,we shall introduce the extension lemmas. Throughout this section, we display a couple of definitions and some lemmas which will be crucial points in the completeness theorem proved in the next section. We follow the method developed in "Relevant logics and their rivals I" [cf. 21, Chapter 4] and followed by Brady [cf. 7, pp. 24-25]. We shall omit some of those proofs since they are similar to Brady's. 12 Definitions and Lemmas throughout this section are developed in general for extensions of the basic logic b4 (Eb4-logics). However, we note that the class of Eb4-logics in Lemmas 7.2, 7.4 and 7.5 has to be restricted to those logics closed under the rules that determine the full regularity of Eb4-theories (cf. Definition 4.9). Otherwise it is possible that the Extension Lemma is not provable for some Eb4-logic.
Firstly, we set a preliminary definition.
Definition 7.1 (Disjunctive Eb4-derivability). Let L be an Eb4-logic, Γ and Θ be non-empty sets of wffs, then Θ is disjunctively derivable The following lemma is essential in order to prove the Extension to maximal sets lemma (see Lemma 7.4). We get it by induction on the length of formulas (cf. p. 27 in [7] and Lemma 6.2 in [18]).
Lemma 7.2 (Preliminary lemma to the extension lemma). Let L be an Eb4-logic closed under no other rules than those specified in Definition 4.9 . For any wffs A, B 1 , . . . , B n , if {B 1 , . . . , B n } ⊢ L A, then, for any wff C, C ∨ (B 1 ∧ · · · ∧ B n ) ⊢ L C ∨ A. Now, the process of extending sets of wffs to maximal sets is required.
Just like Lemma 9 in [7] and Lemma 6.4 in [18], we get: Lemma 7.4 (Extension to maximal sets). Let L be an Eb4-logic closed under no other rules than those specified in Definition 4.9, Γ and Θ sets of wffs such that Γ d L Θ. Then, there are sets of wffs Γ ′ and Θ ′ such Finally, the Primeness Lemma can now be proved.
Lemma 7.5 (Primeness). Let L be an Eb4-logic closed under no other rules than those specified in Definition 4.9. If Γ is a L-maximal set, then it is a fully regular prime L-theory.
Proof. The fact that Γ is a L-theory (i.e., a set of wffs closed under adjunction and L-entailment) can be proved as Brady did for the logic BN4 (cf. Lemma 8 in [7]). Now, let us prove that Γ is prime and fully regular. (1) Γ is regular (i.e., Γ contains any theorem of L). It is clear that, if Γ is a L-maximal set (Γ d L Γ ), Γ must contain every theorem of L. Otherwise, there would be some wff A such that ⊢ L A and A / ∈ Γ . Therefore, we would have A ∈ Γ and consequently, Γ ⊢ d L Γ , contradicting the maximality of Γ . (2) Γ is fully regular (cf. Definition 4.9). We have to prove that Γ is closed under the rules of L. For instance, let us prove that Γ is closed under dPREF. By reductio, suppose there are wffs A, B, C, D such that contradicting the maximality of Γ . (3) Γ is prime. If there were some wffs A, B such that A ∨ B ∈ Γ but A / ∈ Γ and B / ∈ Γ , then Γ would not be L-maximal given A1 ((A ∨ B) → (A ∨ B)).

Completeness of the Lti-logics
We shall prove the completeness of the Lti-logics (1 i 8) (cf. Definition 5.1) w.r.t. both Mti and Lti . Completeness w.r.t. Lti is proved by means of a canonical model construction. Then, completeness w.r.t.
Mti follows immediately by Proposition 6.3.
We begin by the definition of canonical Lti-models. It will be proved that if A is not derivable from Γ in a Lti-logic, then A does not follow from Γ in some canonical Lti-model. The concept of a canonical Ltimodel is based upon the notion of a T -interpretation.   Next, we prove completeness. In order to do so, the notion of "set of consequences in Lti of a given set of wffs Γ " is recalled.

Some facts about Lti-logics
I will investigate if some properties characteristic of relevant logics are predicable of the Lti-logics. In particular, I will prove that no Lti-logic (1 i 8) is a relevant logic since they lack the "variable-sharing property" (vsp). However, they are strongly related to the family of relevant logics since they have another related property called "quasi relevant property" (qrp).  Proof. Let M be the matrix determining the logic L. The proof is immediate since, for any distinct propositional variables p and q, the wff ¬(p → p) → (q → q) is M-valid, this is, the wff is valid in any Lti-logic [cf. 12]. Next, I will prove that Lti-logics are paraconsistent and paracomplete in the sense of the following definitions. In other words, a logic is paraconsistent if theories built upon L are not necessarily trivial when a contradiction arises. Proof. Let M be the matrix determining the logic L and let p and q be distinct propositional variables. There is an M-interpretation I such that I(p) = 2 and I(q) = 0. Therefore, {p, ¬p} M q, this is, Ecq does not hold in any Lti-logic. In other words, a logic is paracomplete if there are prime, fully regular L-theories that are not complete in the sense that they lack at least both a formula and its negation. Proof. Let M be the matrix determining the logic L, then for any propositional variable p there is an M-interpretation I such that I(p) = 1. Therefore, I(p ∨ ¬p) = 1 given Definition 2.6, i.e., PEM does not hold in any Lti-logic.
Next, I define the natural implicative expansions of Belnap and Dunn's logic B4 and prove that Lti-logics (1 i 8) are indeed natural implicative expansions of it. First, following Robles and Méndez [19] (who likewise follow Tomova [23]), I introduce the notion of "natural conditionals" and then I will examine the case of 4-valued matrices.    Proof. It is obvious given that each Mti (1 i 8; cf. Section 3) is one of the 32.768 f → -functions defined in Proposition 9.10 and therefore all of them fulfill the requirements mentioned in Definition 9.9.

Conclusion
By way of conclusion, I shall make five remarks.
1. In the present paper, the class of all implicative expansions of MB4 verifying B while maintaining the conditional structure of MBN4 or ME4 was presented. This class is formed by all the Lti-logics displayed in §5, most of which (with the obvious exception of BN4 and E4) had not been deeply studied before 13 (to the best of my knowledge) and could be seen 5. There are, of course, other conditional structures different from those investigated in this paper that could also be a source of similar interest and another line for further research. 15