We introduce three 5-valued paraconsistent logics that we name FiveASP1, FiveASP2 and FiveASP3. Each of these logics is genuine and paracomplete. FiveASP3 was constructed with the help of Answer Sets Programming. The new value is called e attempting to model the notion of ineffability. If one drops e from any of these logics one obtains a well known 4-valued logic introduced by Avron. If, on the other hand one drops the \implication" connective from any of these logics, one obtains Priest logic FDEe. We present some properties of these logics.
Belnap [
On the other hand, Priest argues in [
Some authors claim that many arguments formulated in Buddhist texts
correspond to such well recognized rules of inference as Modus Ponens, constructive
dilemma and categorical syllogism (also known as hypothetical syllogism) among
other rules of inference, see [
However Priest makes a remarkable work by studying in great detail the
work of the buddhist texts from the Pali Canon to the MMK by Nagarjuna and
beeing able to model their way of reasoning in terms of modern noCn-ocplyarsisgihcta©l 2019 for this paper by its authors.
logics [
A main issue is to represent the notion of ineffability. The fth value, e, then, is the value of ineffable.
There is a complex but well known phenomenon that often arises when a
philosophy argues that there are limits to thought/language, and tries to justify
this view by giving reasons as to why there are things about which one cannot
think/talk|in the process appearing to give the lie to the claim. In poetry we
also nd a similar situation: the need to talk about extreme situations, which
somehow we can not talk [
According to him, Buddhist philosophy has resources to address this kind of issue much less present in Western traditions. Buddhist logicians consider that there are four possibilities: only true, only false, both true and false, and nally neither true or false. Later developments add a fth possibility: ineffability3. Of course, one might be skeptical that such ideas can be made logically respectable.
Priest shows how to accomplish this task with some tools from contemporary non-classical logic. His work is impeccable, but as stated earlier, we consider prudent to extend FDEe logic with an "implication" connective that at least satis es Modus Ponens.
For the nature of this work is desirable to consider the use of
paraconsistent logics [
Paraconsistent logics accept inconsistencies without presenting the problem that once a contradiction has been derived, then any proposition follows as a consequence, as is the case of classical logic.
We introduce three paraconsistent (genuine and paracomplete) logics that
are constructed based on the combination of two logics: BDEe (by Priest) and
a version of Four due to Avron that we call it BL . The main point is to add
an implication to FDEe that satis es (at least) Modus Ponens. Furthermore,
as a second contribution (a minor one) we brie y explain how to use Answer
Set Programming (ASP) [
According to our experience, we know that always it is very useful to have
software tools that help us to analyze logics. One of these tools is the ASP
tool called clasp4, which computes the answer sets of logic programs. ASP is
a declarative knowledge representation and logic programming language, it has
been used to develop different approaches in the areas of planning, logical agents
and arti cial intelligence [
In this section, we present two of the more common ways of de ning a logic, and
provide examples. In Section 2.1 we de ne a logic from the semantical point of
view, particularly via muti-valued systems. On the other hand, in Section 2.2,
we present one axiomatic formal system for logic BL , provided by Avron in
[
A way to de ne a logic is by means of truth values and interpretations. Multivalued systems generalize the idea of using the truth tables that are used to determine the validity of formulas in classical logic. It has been suggested that multi-valued systems should not count as logics; on the other hand pioneers such as Lukasiewicz considered such multi-valued systems as alternatives to the classical framework. Like other authors do, we prefer to give to multi-valued systems the bene t of the doubt about their status as logics.
The core of a multi-valued system is its domain of values D, where some of such values are special and identi ed as designated. Connectives (e.g. ^, _, !, :) are then introduced as operators over D according to the particular de nition of the logic. An interpretation is a function I : L ! D that maps atoms to elements in the domain. The application of I is then extended to arbitrary formulas by mapping rst 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 multi-valued logic is classical logic where: D = f0; 1g, 1 is the unique designated value, and connectives are de ned through the usual basic truth tables.
Not all multi-valued logics must have the four connectives mentioned before, in fact classical logic can be de ned in terms of two of those connectives :; ^ (primitive connectives), and the other two (non-primitive) can be de ned in terms of :; ^. In case of a logic having the implication connective, it is desirable that it preserves 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 subindices 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. Objects 0, 1, 2 and 3 are part of the semantics of logics studied in this paper and were chosen only for convenience, it does not correspond to natural numbers.
A logic satis es the principle of explosion (EFQ)) if x; :x j= y. A logic is
paraconsistent if it rejects the principle of explosion. A logic satis es the principle
of non-contradiction (PNC) if j= :(x ^ :x). A logic is genuine if it rejects the
principle of non-contradiction. A logic satis es the law of excluded middle if
j= x _ :x. A logic is paracomplete if it rejects the law of excluded middle.
Kleene's 3-valued logic. The Kleene's 3-valued logic, denote here by K, is
de ned in [
The basic 3-valued paraconsistent logic PAC. We consider the domain of
the logic P AC as D = f0; 2; 3g, this logic is a 3-valued paraconsistent logic with
2 and 3 as designated values (We take this domain with the purpose of P AC
becomes a fragment of BL logic). The connectives :, ^ and _ have exactly
the same properties as those of the logic K. Table 2 shows the truth tables of
connectives :PAC and !PAC [
Logic BL . This logic is a 4-valued logic with truth values in the domain D = f0; 1; 2; 3g 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 de ned according to the truth tables given in Table 3. 5 The reason for considering this domain is that these values and the behavior of its connectives coincide with part of the logic BL .
The logic BL is represented in Fig. 1. Note that if we consider only the values 0, 1 and 3 (right part of the Fig. 1) we obtain the Kleene's logic while if we take the values 0, 2 and 3 (left part of the Fig. 1) we have the P AC logic.
As A. Avron mentions in [
:= ( ! ) ^ ( ! ) the well-formed formulas are constructed as usual, the axiom schemas are: I1 I2 I3 C1
! ( ! )
( ! ( ! )) ! (( ! ) ! ( ! ))
(( ! ) ! ) !
( ^ ) !
6 This means that each one of ^, and _ is monotonic with respect to both t and
[
Logic BL is sound and complete with respect to this axiomatization.
⊢BL if and only if j=BL : 2.3
This subsection is a summary of some material from [
First Degree Entailment (FDE) is a system of logic de ned by Priest that can be set up in many ways, but one of these is as a 4-valued logic whose values are t (true only), f (false only), b (both), and n (neither). Negation maps t to f , vice versa, n to itself, and b to itself. Conjunction is greatest lower bound, and disjunction is least upper bound. The set of designated values, D, is fb; tg The four corners of truth and the FDE logic seem like a correct match.
FDE can be characterised by the following sound and complete rule system, where a double line indicates a two-way rule, and overlining indicates discharging an assumption7:
A;B A^B A^B A(B)
A(B) A_B A:::C B:::C :(AA_^BB) :(AC_B) ::A :A_:B :A^:B A
Now we move to FDEe, a 5-valued logic that incorporates the notion of ineffability. According to Priest, technically, the obvious thought is to add a new value, e, to our existing four ft; f; b; ng), expressing this new status.
Since e is the status of claims such that neither they nor their negations should be accepted, it should obviously not be designated. Thus, we still have that same designated values. Priest addresses the following major question: How are the connectives to behave with respect to e?
Both e and n are the values of things that are, in some sense, neither true nor false, but they need to behave differently if the two are to represent distinct alternatives. The simplest suggestion is to take e to be such that whenever any input has the value e, so does the output: e-in=e-out.
The logic that results by modifying FDE in this way is obviously a sub-logic of it. It is a proper sub-logic. It is not difficult to check that all the rules of FDE are designation-preserving except the rule for disjunction-introduction, which is not, as an obvious counter-model shows. However, replace this with the rules: φ(A) C φ(A) C φ(A) (B) C
A_C :A_C (A^B)_C where φ(A) and (B) are any sentences containing A and B. Call these the φ Rules, and call this system F DEφ. F DEφ is sound and complete with respect to the semantics. 3
We present three logics that are constructed based on the combination of two logics: BDEe (by Priest) and BL .
The core of the three logics is based on the following assumptions.
We have 5 values: f0; 1; 2; 3; eg. FDEe uses ff; n; b; t; eg instead. The designated values are f2; 3g as FDEe. f0; 1; 2; g de nes a lattice where 0 < 1, 0 < 2, 1 < 3, 2 < 3. The connective _ is the lub, while ^ is the glb.
Since e is interpreted as ineffable then X op e = e op X = e, where X 2 f0; 1; 2; 3; eg. With respect to negation ( ), we have 0 = 3, 3 = 0, 1 = 1, 2 = 2, e = e.
Implication is as de ned by Avron for the subdomain f0; 1; 2; 3g, namely: X ! Y = 3 when X is not designated, X ̸= e, Y ̸= e. While X ! Y = Y when X is designated, Y ̸= e.
The next two expressions are yet unde ned e ! X and e ! X for X in f0; 1; 2; 3; eg.
Notice that the sublogic de ned in the subdomain f0; 1; 2; 3g corresponds exactly to BL logic. Also the sublogic in the domain f0; 1; 2; 3; eg but eliminating the implication connective correspond exactly to FDEe. 3.1
This logic tries to stay very close to FDEe. We de ne e ! X = X ! e = e for X 2 f0; 1; 2; 3; eg, and we name this logic as FiveASP1.
Proof (sketch). Directly using truth tables. For example, to prove that it is paracomplete, it is enough to evaluate the formulas with val(X) = 1, for every atom X.
FDEe admits no tautologies. FiveASP1 is faithful in this aspect to FDEe and hence we have the following result.
Proof (sketch). Evaluating each atom in any formula with e, then the nal evaluation is e which is not designated.
Proof (sketch). (case 1) They are proven by contradiction using truth tables. (case 2) They are proven by construction, since the three logics behave as logic FDEe regarding the connectives ^, _ and negation, and that logic satis es such inference rules. 3.2
This logic is somehow the \middle way" between logics FiveASP1 and FiveASP3 (to be introduced soon). It only changes \e ! e = e" (in FiveASP1) to \e ! e = 3" (in FiveASP2), in order to allow some basic tautologies. Recall that the notion of ineffable is to some extend paradoxical, we can not talk about something ineffable but actually we do it in order to convey a given major message (at least partially). Here, we have that: if X is ineffable and is true and only true that X ! Y , then (our logic claims that) Y is ineffable.
We de ne e ! X = X ! e = e for X 2 f0; 1; 2; 3g and e ! e = 3 and we name this logic as FiveASP2.
Proof (sketch). Directly using truth tables.
We can observe that FiveASP2 satis es some well known tautologies, as X ! X and De Morgan laws, among some of them. Hence, we have the following theorem.
Proof (sketch). FiveASP2 accept the mentioned tautologies in the phrase previous to this theorem and they are proven directly.
Proof (sketch). (case 1) They are proven by contradiction using truth tables.
(case 2) They are proven by construction, since the three logics behave as logic
FDEe regarding the connectives ^, _ and negation, and that logic satis es such
inference rules.
This logic is kind of pragmatic and the connective \Implication" is a kind of
metalinguistic connective [
Proof (sketch). Directly using truth tables.
We can observe that FiveASP3 satis es many well known tautologies, as X ! X and De Morgan laws, the standard two implication rules for positive logic among some of them. Hence, we have the following theorem.
Proof (sketch). FiveASP3 accepts the mentioned tautologies in the phrase previous to this theorem and they are proven directly.
Proof (sketch). (case 1) They are proven by contradiction using truth tables. (case 2) They are proven by construction, since the three logics behave as logic FDEe regarding the connectives ^, _ and negation, and that logic satis es such inference rules.
Recall that ASP is logic programming that allows to write the speci cation of a problem (de ning only the \what" with no concern to the \how"). On this regard, it follows a generate and test strategy. In this case our concern is to de ne an implication operator that satis es certain given constraints. To de ne such implication operator we write:
Meaning that given the domain for X; Y (in this case v(X), v(Y )) we de ne a function "impl" with co-domain Z (de ned by v(Z)).
The rest of the code provides basic de nitions such as the domain, the designated values, etc. and also some constraints (test part) such as for example: :
not impl(Y; X; 3); v1(Y ); v1(X); notdes(Y ):
This constraint says that our implication operator should behaved as BL , namely that if the rst argument of the implication operator is not designated (and belongs to the subdomian of this 4-valued logic) then our operator should evaluate to 3. In the appendix A, the complete program code with some further comments is presented. 4
We introduce three 5-valued logics by combining FDEe and BL . The three of them satisfy the following properties: they are paraconsistent, genuine and paracomplete logics. They satisfy Modus Ponens and Hypothetical Syllogism as well as all inference rules of FDEe. More research needs to be done to understand these logics and to nd further mathematical properties of each of them. We also believe that our logics or some extensions of them could be used to represent/understand complex poems where inconsistent, uncertain and/or ineffable beliefs are considered.
It is also interesting to consider extending these logics by de ning a
possibilistic version of each of our three logics, see [
FiveASP3.clasp is a program that builds a logic of ve values from two logic, one from Priest and another from Avron. The logic of Priest has ve values but does not include implication connective. Avron's logic has only four values but includes all the connectives. We verify known tautologies, among these: (x^y) ! x, (x^y) ! y, x ! (y ! (x^y)), (x_y) ! ((x ! z) ! ((y ! z)) ! z), y $ ::y, Pierce formula ((x ! y) ! x) ! x. #show impl/3. v1(0..3). v(e). v(X):- v1(X).
des(2..3). %% Definition AND (Priest) and(X,X,X) :- v1(X). and(0,X,0) :- v1(X). and(X,3,X) :- v1(X). and(3,X,X) :- v1(X). and(2,1,0). and(e,X,e) :- v(X). %% Definition OR (Priest) or(X,X,X):- v1(X). or(0,X,X):- v1(X). or(X,3,3):- v1(X). or(3,X,3):- v1(X). or(2,1,3). or(e,X,e) :- v(X). and(X,0,0):- v1(X). and(1,2,0).
and(X,e,e) :- v(X). or(X,0,X):- v1(X). or(1,2,3). % impl (Any function of 2 arguments) 1 { impl(X,Y,Z) : v(Z) } 1 :- v(X), v(Y). % Restrictions for the implication of Avron (4-valued logic) :- not impl(Y,X,3), v1(Y), v1(X), not des(Y). :- not impl(Y,X,X), v1(Y), v1(X), des(Y). % Traditional definition of equivalence equ(X,Y,Z) :- impl(X,Y,L), impl(Y,X,R), and(L,R,Z). % Definition of negation according to Priest neg(0,3). neg(3,0). neg(1,1). neg(2,2). neg(e,e). %% inference rules MP :- impl(X,Y,Z), des(X), des(Z), v(Y), not des(Y). %% axioms 1,2 impl, %X -> ( Y -> X) :- impl(Y,X,Z), impl(X,Z,R), v(R), not des(R). % (X -> (Y -> Z)) -> ( ( X -> Y) -> (X -> Z) %% -(A ->B) <-> (A & -B) :- impl(A,B,L), neg(L,L1), neg(B,B1), and(A,B1,R), equ(L1,R,Q), not des(Q), v(Q). %%% FINISHES Basic construction. %There are exactly 4 logics that meet the above. %% We eliminate the one that evaluate e for values at {0,1,2,3} x {e} % to contrast with logic fiveASP1. The result is a single logic. :- impl(X,e,e), v1(X).