An epistemic approach to paraconsistency: a logic of evidence and truth

Abstract

The purpose of this paper is to present a paraconsistent formal system and a corresponding intended interpretation according to which true contradictions are not tolerated. Contradictions are, instead, epistemically understood as conflicting evidence, where evidence for a proposition A is understood as reasons for believing that A is true. The paper defines a paraconsistent and paracomplete natural deduction system, called the Basic Logic of Evidence (BLE), and extends it to the Logic of Evidence and Truth ($\textit{LET}_{J}$). The latter is a logic of formal inconsistency and undeterminedness that is able to express not only preservation of evidence but also preservation of truth. $\textit{LET}_{J}$ is anti-dialetheist in the sense that, according to the intuitive interpretation proposed here, its consequence relation is trivial in the presence of any true contradiction. Adequate semantics and a decision method are presented for both BLE and $\textit{LET}_{J}$, as well as some technical results that fit the intended interpretation.

1 Introduction

The distinctive feature of paraconsistent logics is that the principle of explosion, according to which anything follows from a contradiction, does not hold, thus allowing the acceptance of contradictions within a theory without falling into triviality. Paraconsistency is the study of paraconsistent logics, both in its technical and philosophical aspects. Dialetheism is the view according to which there are true contradictions (see e.g. Priest and Berto 2013). The dialetheist claims that some contradictions are ontological in the sense that they are due to some ‘inner contradictory essence of reality’—or in other words, that reality, in order to be correctly described, demands pairs of contradictory propositions.¹ Of course, endorsing a paraconsistent logic and being a dialetheist are not the same thing: the latter implies the former, but not the other way round. One can be a paraconsistent logician without being a dialetheist, since paraconsistent logics may be studied and developed without the commitment to the truth of accepted contradictions. Another view in paraconsistency, that we call metaphysical neutrality, ‘suspends judgement’ with respect to the nature of contradictions. It is a somewhat pragmatic position: the fact that contradictions occur in several contexts of reasoning is enough to justify a non-explosive account of logical consequence, and there is no need to go into the metaphysical question about the nature of such contradictions. A third position in paraconsistency, antagonistic to dialetheism, claims that no contradiction is ontological but, rather, all contradictions that occur in scientific theories, belief systems, a number of situations in informal reasoning, and even in semantic and set theoretical paradoxes—that are, strictly speaking, results about languages with certain characteristics—have epistemic character in the sense that they are related to thought and language. This is the position endorsed by us.

It is likely that no paraconsistent logician would be opposed to epistemic contradictions. However, to the best of our knowledge, a paraconsistent formal system suited to an intuitive reading according to which only epistemic contradictions are allowed (and true contradictions are ‘prohibited’) is still lacking. Our aim here is to present a system of this kind. In order to work out such an account of paraconsistency we have to explain what it means to say that a pair of propositions A and $\lnot A$ simultaneously ‘hold’, or ‘may be accepted’, without being true.

According to the standard view, that can be traced back to Aristotle and is to be found in virtually every book on elementary logic, the validity of an inference is a matter of necessary preservation of truth. The essential property of propositions, from the viewpoint of classical logic, is truth. Indeed, the more effective way of prohibiting true contradictions is the principle of explosion that, together with excluded middle, composes the deductive properties of classical negation. But truth is not always the only property of propositions that matters. In intuitionistic logic, for example, the property at stake is not only truth but truth together with the availability of a constructive proof. Thus, there may be a proposition A such that both A and $\lnot A$ do not hold because there is no proof for any of them. Given the soundness of the system, a proof of A entails the truth of A, but it may be the case that A has been proved true by non-constructive means although there is no constructive proof of A. Notice that the following situation is perfectly feasible: given two propositions A and $\lnot A$, exactly one of them is true, but from a constructivist point of view neither holds because there is no proof available for A or for $\lnot A$. Such a view combines a realistic notion of truth with a notion of constructive proof that is essentially epistemic.²

In the case of a non-dialetheist paraconsistent logic the situation is dual. There may be a proposition A such that it is not the case that both A and $\lnot A$ are true, but in some sense both hold in a given context. In this case, the essential question Q is the following: Q: what property are we going to ascribe to a pair of accepted

contradictory propositions such that it would be possible

for a proposition to enjoy it without being true? Such a property has to be something weaker than truth. If we want to reject the principle of explosion together with dialetheism, without assuming a position of metaphysical neutrality, we have to give a convincing answer to Q. Our proposal is that the notion of evidence is well suited to be such an answer.

The main aim of this paper is to present a paraconsistent formal system, that we call the Logic of Evidence and Truth ($\textit{LET}_{J}$), and an anti-dialetheist explanation of it according to which contradictions are understood epistemically as conflicting evidence and true contradictions are not allowed. Section 2 briefly discusses the notion of evidence in order to show that it is an appropriate answer to question Q above. Section 3 presents a paracomplete and paraconsistent natural deduction system for a logic we call BLE, (the Basic Logic of Evidence), whose inference rules are intended to preserve evidence, not truth. Neither excluded middle nor explosion hold in BLE because evidence can be incomplete as well as contradictory.³ Section 4 is dedicated to extending BLE to a logic we call $\textit{LET}_{J}$ (Logic of Evidence and Truth based on positive intuitionistic sentential logic). $\textit{LET}_{J}$is a logic of formal inconsistency and undeterminedness that extends BLE by adding resources to express that a particular formula A behaves classically: a unary sentential connective $\circ$ is added to the language of BLE, and $\circ A$ recovers explosion and excluded middle for A. A valuation semantics, a decision method and some technical results for BLE and $\textit{LET}_{J}$ will be presented.⁴ Finally, in Sect. 5, we face some issues related to paraconsistency as preservation of evidence.

2 On the notion of evidence

There are a number of circumstances in which we have to deal with pairs of propositions A and $\lnot A$ such that there are reasons for accepting and/or believing in both. It does not mean that both are true, nor that we actually believe that both are true. However, in such circumstances, although there may be nothing conclusive with respect to the truth-value of A, we still wish to draw inferences in the presence of both A and $\lnot A$.⁵ The acceptance of A and $\lnot A$ can be understood as some kind of ‘conflicting information’ about A, in the sense of having non-conclusive reasons for accepting the truth as well as the falsity of A. This kind of ‘conflicting information’ we call here conflicting evidence. Let the falsity of A be represented by $\lnot A$. So,

• ‘evidence that A is true’ means ‘reasons for believing in/accepting A’;

• ‘evidence that A is false’ means ‘reasons for believing in/accepting $\lnot A$’.

There may be evidence that A is true even if A is false. Conflicting evidence occurs when reasons for accepting A and $\lnot A$ are simultaneous and non-conclusive. Conclusive evidence is evidence that establishes conclusively the truth (or the falsity) of A, and eliminates any opposed non-conclusive evidence. Typical cases of conflicting evidence, in the sense explained above, are the following. You may ask two different but reliable doctors about the cause of some symptoms and get two different and incompatible diagnoses. Another example: two witnesses may deliver two contradictory statements regarding some point that is crucial to the judge’s final decision. Supposing, again, that both are reliable, it may be said that there are reasons for believing both A and $\lnot A$, although only one of them is true. The idea of non-conclusive versus conclusive evidence is well illustrated in theories about empirical phenomena. A good example is the conflict between classical mechanics and the theory of electromagnetic field, that are in the origin of Einstein’s special relativity (see Carnielli and Rodrigues 2016). Actually, it is not uncommon that two different scientific theories, successful in describing and predicting a class of phenomena, may yield contradictory results in some specific situations.⁶

The use we make here of the notion of evidence is close to the way evidence in understood in epistemology. In Kelly (2014) we read that evidence “is the kind of thing which can make a difference to what one is justified in believing or ...what it is reasonable for one to believe” and later he adds that since “evidence is the sort of thing which confers justification ...it is natural to think that ‘reason to believe’ and ‘evidence’ are more or less synonymous.” The link between ‘evidence’ and ‘reasons to believe’ is also clear in the ‘principle of reasonable belief’, presented by Achinstein (2010a): if, in the light of background information $\varPhi$, $\kappa$ is evidence that A, then, given $\varPhi$, $\kappa$ is a good reason for believing A. Achinstein also distinguishes potential evidence from veridical evidence. Roughly speaking, an evidence $\kappa$ for a proposition A is veridical if A is true and there is an ‘explanatory connection’ between A and $\kappa$ (this means, as we understand it, that $\kappa$establishes conclusively the truth of A). On the other hand, $\kappa$ may be potential evidence for A, even if A is false. Achinstein’s notions of potential and veridical evidence are close to what we call here, respectively, evidence simpliciter (non-conclusive) and conclusive evidence.

It is important to call attention to the fact that evidence, in the sense used here, is always external to the formal system. We are not formalizing the notion of evidence, nor will we present a ‘semantics of evidence’.⁷ The aim of Sect. 3 is to give an account of the deductive behaviour of the sentential connectives from the point of view of preservation of evidence, instead of preservation of truth: an inference is taken to be valid just in case there cannot exist evidence for the premises without evidence for the conclusion. What constitutes evidence depends on the area of study and the subject matter, and this is not a problem of logic. Actually, it is not surprising that there is no unified account of what constitutes evidence for a given proposition A (see Achinstein 2010b). What kind of thing constitutes non-conclusive or conclusive evidence varies for the physicist, chemist, archaeologist and so on.

3 A logic of evidence

The aim of this section is to devise a paraconsistent formal system suited to the reading of contradictions as conflicting evidence. What we will do here has an analogy to the inference rules for intuitionistic logic, when the latter is understood epistemically as concerned with the availability of a constructive proof. Natural deduction rules are particularly well suited to expressing the intuitionistic way of constructing proofs. Roughly speaking, the basic idea of the Brouwer–Heyting–Kolmogorov (BHK) interpretation is that an inference rule is valid if it transforms constructive proofs for one or more premises into a constructive proof of the conclusion. Here, analogously, the guiding idea is the following: supposing the availability of evidence for the premises, we ask whether an inference rule yields a conclusion for which evidence is also available.

As we have seen, (i) the falsity of A is represented here by $\lnot A$, (ii) ‘evidence that A is true’ is understood as ‘reasons for accepting/believing in A’, and (iii) ‘evidence that A is false’ means ‘reasons for accepting/believing in $\lnot A$’. So,

• ‘A holds’ means ‘there is evidence that A is true’;

• ‘A does not hold’ means ‘there is no evidence that A is true’;

• ‘$\lnot A$ holds’ means ‘there is evidence that A is false’;

• ‘$\lnot A$ does not hold’ means ‘there is no evidence that A is false’.

Accordingly, the following scenarios may be described with respect to a proposition A:

• 1. No evidence at all: both A and $\lnot A$ do not hold.

• 2. Only evidence that A is true: A holds, $\lnot A$ does not hold.

• 3. Only evidence that A is false: $\lnot A$ holds, A does not hold.

• 4. Conflicting evidence: both A and $\lnot A$ hold.

Thus, the formal system we are looking for must be not only paraconsistent but also paracomplete: neither the principle of explosion nor excluded middle should hold. The next section examines which natural deduction rules are suitable for expressing the propagation of evidence through implication, conjunction, disjunction, and negation.

3.1 A natural deduction system for preservation of evidence

Let $L_{0}$ be a language with a denumerable set of propositional letters $\{p_{0}, p_{1},$$p_{2},\ldots \}$, parentheses, and closed under the connectives in the set $\{\lnot , \wedge ,$$\vee , \rightarrow \}$. The set $S_{0}$ of formulas of $L_{0}$ is obtained recursively in the usual way. Roman capitals stand for meta-variables for formulas of $L_{0}$. The definition of a derivation D of A from a set $\varGamma$ of premises is the usual one for natural deduction systems.

A complete natural deduction system for classical propositional logic is defined by adding to the introduction and elimination rules for $\rightarrow$, $\vee$ and $\wedge$ the rules of explosion and excluded middle below:

By dropping the rules above and keeping only the introduction and elimination rules for $\rightarrow$, $\vee$ and $\wedge$, we get positive intuitionistic propositional logic (PIL). We start with PIL, arguing that it is able to express the notion of preservation of evidence.

With respect to PIL, the availability of evidence is analogous to availability of proof. As usual in natural deduction systems, [A] means that the hypothesis A has been discharged (or canceled). An evidence-interpretation for the introduction rules for $\wedge$ and $\vee$ is straightforward. If $\kappa$ and $\kappa '$ are evidence, respectively, for A and B, $\kappa$ and $\kappa '$ together constitute evidence for $A \wedge B$.⁸ Similarly, if $\kappa$ constitutes evidence for A, then $\kappa$ is also evidence for any disjunction that has A as one disjunct. The rule $\rightarrow I$ deserves some remarks. When the supposition that there is evidence $\kappa$ for A leads to the conclusion that there is evidence $\kappa '$ for B, this is itself evidence for $A \rightarrow B$. Notice that $\rightarrow$ does not demand any relation between the contents or meanings of A and B. If there is evidence for B, we may conclude that there is also evidence for $A \rightarrow B$, for any A. The implication, therefore, works analogously to both classical and BHK interpretation: if B is true, $A \rightarrow B$ is also true; if there is a construction of B, there is a construction of $A \rightarrow B$. Up to this point, this takes care of the introduction rules.

The elimination rules may be obtained from the introduction rules. Gentzen (1935, p. 80) famously remarks that “The introductions represent, as it were, the ‘definitions’ of the symbols concerned, and the eliminations are no more, in the final analysis, than the consequences of these definitions”. Prawitz (1965, p. 33) has put this idea more precisely in the so-called inversion principle. We reformulate Prawitz’ inversion principle in terms of evidence as follows:

• Evidence inversion principle (EIP)

  Let $\alpha$ be an application of an elimination rule that has B as consequence. Then, any $\kappa$ that is evidence for the major premise of $\alpha$, when combined with evidence for the minor premises of $\alpha$ (if any), already constitutes evidence for B; the existence of evidence for B is thus obtainable directly from the existence of evidence for the premises, without the addition of $\alpha$.

We thus easily gain the respective elimination rules which do preserve availability of evidence. For the sake of an example, let us take a look at $\wedge E$. If some evidence $\kappa$ for $A \wedge B$ is available, $\kappa$ would be, or would ‘contain’ evidence for A, as well as for B. Analogous reasoning apply to the other rules.

Up to this point we have what could be called a positive logic of preservation of evidence. PIL is well suited to express both preservation of evidence and the (positive) BHK interpretation. It is worth noting that the introduction and elimination rules for conjunction, implication and disjunction, therefore, preserve a notion stronger than truth (constructive proof) as well as a notion weaker than truth (evidence).

3.2 Negation

A central issue in paraconsistency is that of specifying a negation without (some of) the properties of classical negation but that still retains enough properties to be termed a negation. As discussed in the beginning of Sect. 3, the principle of explosion and excluded middle do not hold from the viewpoint of preservation of evidence. Another property of classical negation that must be invalid is the so-called introduction of negation:

$$\begin{aligned} A \rightarrow B, A \rightarrow \lnot B \vdash \lnot A. \end{aligned}$$

(1)

The reason is that any extension of PIL in which introduction of negation holds is able to prove that for any A and B:

$$\begin{aligned} A, \lnot A \vdash \lnot B, \end{aligned}$$

(2)

that is, from a contradiction, any negated proposition follows, which is an undesirable result for a paraconsistent system.⁹ Besides, and more importantly, the introduction of negation does not fit the intuitive interpretation in terms of evidence, since there may be a circumstance such that there is evidence for B and for $\lnot B$, and so also for $A \rightarrow B$ and $A \rightarrow \lnot B$, but no evidence for $\lnot A$.

Now we turn to rules in which the conclusion is a negation of a conjunction, a disjunction or an implication. Natural deduction rules for concluding falsities may be obtained in a way similar to the rules for concluding truths. The point is that instead of asking about the conditions of assertibility, we ask about the conditions of refutability (cf. López-Escobar 1972). An example of a natural deduction rule whose conclusion is the falsity of a conjunction is the following

This rule is obtained by asking what would be sufficient conditions for refuting a conjunction. We now apply an analogous idea, asking what would be sufficient conditions for having evidence for the falsity of a conclusion. If $\kappa$ is evidence that A is false, $\kappa$ constitutes evidence that $A \wedge B$ is false—mutatis mutandis for B. Analogous reasoning for $\vee$ and $\rightarrow$ gives the following introduction rules:

Elimination rules are obtained by applying the evidence inversion principle (EIP) mentioned above.

Indeed, let us take a look at rule $\lnot \rightarrow E$. When $\kappa$ is evidence that a formula $A \rightarrow B$ is false, $\kappa$ must also be evidence for the truth of the antecedent A and for the falsity of the consequent B.¹⁰

The validity of double negation,

is perhaps not so clear as the other rules, but we claim that in both directions DN fits an intuitive notion of evidence. The rules above relate, in a perspicuous way, evidence that a proposition A is true and evidence that A is false. Suppose $\kappa$ is evidence that A is true. It is reasonable to see $\kappa$ as evidence that it is false that A is false. Now suppose, conversely, that $\kappa$ is evidence that it is false that A is false. Again, it is reasonable that $\kappa$ also constitutes evidence that A is true.

Let us call the logic defined by the rules DN, introduction and elimination for $\rightarrow$, $\vee$ and $\wedge$, plus introduction and elimination for negated $\rightarrow$, $\vee$ and $\wedge$, the Basic Logic of Evidence (BLE). BLE faithfully represents preservation of evidence when the latter is understood as reasons for believing the truth/falsity of propositions, as explained in Sect. 2 above.¹¹

Lemma 1

The following properties hold for BLE:

• P1. Reflexivity: if $A\in \varGamma$, then $\varGamma \vdash A$;

• P2. Monotonicity: if $\varGamma \vdash B$, then $\varGamma , A \vdash B$, for any A;

• P3. Transitivity (cut): if $\varDelta \vdash A$ and $\varGamma , A \vdash B$, then $\varDelta ,\varGamma \vdash B$;

• P4. Deduction theorem: if $\varGamma , A \vdash B$, then $\varGamma \vdash A\rightarrow B$;

• P5. Compactness: if $\varGamma \vdash A$, then there is $\varDelta \subseteq \varGamma$, $\varDelta$ finite such that $\varDelta \vdash A$.

Proof

The properties P1, P2, P3 and P5 are direct consequences of the definition of a deduction of A from premises in $\varGamma$. The deduction theorem (P4) amounts to the rule $\rightarrow$-introduction. $\square$

Since its consequence relation is reflexive, monotonic and transitive (properties P1, P2 and P3), BLE is thus a Tarskian or standard logic.

3.3 A semantics for BLE

Some logics allow for a semantics with an intuitive appeal independent of the corresponding deductive system. This is the case, for example, of the truth-tables for classical logic and the possible-worlds semantics for alethic modal logic. Indeed, these semantics do provide an insight into these logics because it really seems that the semantic clauses ‘make sense’ independently of the inference rules and/or axioms. And it is of course a relevant matter to show that the semantics and the deductive system are two different ways of determining the same set of valid inferences. On the other hand, the semantics to be presented here for BLEis not intended to have any intuitive appeal independent of the deductive system. Rather, such semantics should be seen as a mathematical tool capable of representing the inference rules in such a way that some technical results may be proved, not only for BLE but also for $\textit{LET}_{J}$, an extension of BLE that will be seen in Sect. 4. The ‘meaning’ of the logic BLE is given by the fact that its rules preserve evidence.¹² In what follows, the values 0 and 1 are better seen as labels that intend to be faithful to the inference rules. Ascribed to a formula A, they mean, respectively, that A does not hold and that A holds. So, according to the explanation in terms of evidence given in Sect. 3,

• $v(A)=1$ means ‘there is evidence that A is true’;

• $v(A)=0$ means ‘there is no evidence that A is true’;

• $v(\lnot A)=1$ means ‘there is evidence that A is false’;

• $v(\lnot A)=0$ means ‘there is no evidence that A is false’.

The valuation semantics presented below is sound, complete, and yields a decision procedure for BLE.

Definition 2

A semivaluations for BLE is a function from the set S of formulas to $\lbrace 0, 1 \rbrace$ such that:

• 1. if $s(A)=1$ and $s(B)=0$, then $s(A \rightarrow B)=0$;

• 2. if $s(B)=1$, then $s(A \rightarrow B)=1$;

• 3. $s(A \wedge B)=1$ iff $s(A)=1$ and $s(B)=1$;

• 4. $s(A \vee B)=1$ iff $s(A)=1$ or $s(B)=1$;

• 5. $s(A) = 1$ iff $s(\lnot \lnot A) = 1$;

• 6. $s(\lnot (A \wedge B)) = 1$ iff $s(\lnot A) = 1$ or $s(\lnot B) = 1$;

• 7. $s(\lnot (A \vee B)) = 1$ iff $s(\lnot A) = 1$ and $s(\lnot B) = 1$;

• 8. $s(\lnot (A \rightarrow B)) = 1$ iff $s(A) = 1$ and $s(\lnot B) = 1$;

Definition 3

A valuation for BLE is a semivaluation for which the condition below holds:

• (Val) For all formulas of the form $A_{1} \rightarrow (A_{2} \rightarrow \cdots \rightarrow (A_{n} \rightarrow B)\ldots )$ with B not of the form $C \rightarrow D$:

  if $s(A_{1} \rightarrow (A_{2} \rightarrow \cdots \rightarrow (A_{n} \rightarrow B)\ldots )) = 0$, then there is a semivaluation $s'$ such that for every i, $1 \le i \le n$, $s(A_{i})=1$ and $s(B)=0$.

We say that a valuation v is a model of $\varGamma$ ($v \vDash \varGamma$) if for all $B \in \varGamma$, $v(B)=1$; $v \vDash A$ means that $v(A)=1$. Logical consequence in BLE is defined as follows: $\varGamma \vDash A$ if and only if for every valuation v, if v is a model of $\varGamma$, then $v(A) = 1$. It is also worth noting that this semantics shows that BLE is not compositional, in the sense that the semantic value of a complex formula is not functionally determined by the semantic values of its component parts. Indeed, this semantics may be represented by the so-called quasi-matrices.¹³ Let us see an example below.

Example 4

$A \vee (A \rightarrow B)$ is invalid in BLE.

The subformula $A \rightarrow B$ receives 0 in the semivaluation $s_{1}$. The latter is not excluded by condition Val (that is, it is a legitimate valuation) because there is a semivaluation s such that $s(A)=1$ and $s(B)=0$, namely, $s_{4}$. Notice that the formula $A \vee (A \rightarrow B)$, added to PIL, yields positive classical propositional logic.

The semantic clauses are intended to represent the deductive properties of the formal system in terms of the semantic values 0 and 1. It is not difficult to see a correspondence between the inference rules and the clauses 3–8 of Definition 2, for disjunction, conjunction and negation. The clauses for implication deserve some remarks. Implication is defined by clauses 1 and 2 of Definition 2 plus condition Val of Definition 3. Clause 1 expresses the fact that if $v(A)=1$ and $v(B)=0$, it cannot be that $v(A \rightarrow B)=1$, since it would contradict modus ponens. Clause 2 expresses the fact that $v(B)=1$ implies that $v(A \rightarrow B)=1$. Clause Val establishes the equivalence between $\varGamma , A \vDash B$ and $\varGamma \vDash A \rightarrow B$. In order to see how this works, notice that without the clause Val we cannot guarantee the validity of $\vDash A \rightarrow (B \rightarrow A)$.¹⁴

Example 5

$A\rightarrow (B\rightarrow A)$ is valid in BLE.

Some semivaluations at line 4 need to be excluded: $s_{1}$ and $s_{4}$ do not satisfy condition Val and therefore are not valuations. So, the formula receives 1 under every valuation (namely $s_{2}$, $s_{3}$, $s_{5}$, $s_{6}$ and $s_{7}$) and is thus valid.

3.3.1 Soundness

Theorem 6

If $\varGamma \vdash A$, then $\varGamma \vDash A$.

Proof

We show by induction on the length of a derivation D with premises in $\varGamma$ and conclusion A, that $\varGamma \vDash A$ holds.

Base if D has one element A, it means $\lbrace A \rbrace \vdash A$. So, $A \in \varGamma$, and $\varGamma \vDash A$.

Inductive step For each rule, the inductive hypothesis says that there are sound derivations for the premise(s). The rest of the proof consists in showing that the derivation obtained by the application of the rule is sound. Details of this routine proof are left to the reader. $\square$

3.3.2 Completeness

Theorem 7

If $\varGamma \vDash A$, then $\varGamma \vdash A$.

Proof

Completeness is achieved by means of a Henkin-style proof. Suppose $\varGamma \nvdash A$. An A-saturated set $\varDelta$ is obtained from $\varGamma$ by means of a Lindenbaum construction in the usual way. The following propositions, corresponding to clauses 1 to 8 of Definition 2 plus condition (Val) of Definition 3, can be proved:

$(1')$ :

if $A \in \varDelta$ and $B \notin \varDelta$, then $A \rightarrow B \notin \varDelta$;

$(2')$ :

if $B \in \varDelta$, then $A \rightarrow B \in \varDelta$;

$(3')$ :

$A \wedge B \in \varDelta$ iff $A \in \varDelta$ and $B \in \varDelta$;

$(4')$ :

$A \vee B \in \varDelta$ iff $A \in \varDelta$ or $B \in \varDelta$;

$(5')$ :

$A \in \varDelta$ iff $\lnot \lnot A \in \varDelta$;

$(6')$ :

$\lnot (A \wedge B) \in \varDelta$ iff $\lnot A \in \varDelta$ or $\lnot B \in \varDelta$;

$(7')$ :

$\lnot (A \vee B) \in \varDelta$ iff $\lnot A \in \varDelta$ and $\lnot B \in \varDelta$;

$(8')$ :

$\lnot (A \rightarrow B) \in \varDelta$ iff $A \in \varDelta$ and $\lnot B \in \varDelta$;

$(Val')$ :

If $\varDelta$ is A-saturated and $A_{1} \rightarrow (A_{2} \rightarrow \cdots \rightarrow (A_{n} \rightarrow B)\ldots ) \notin \varDelta$, then there is a B-saturated set $\varDelta '$ such that $\varDelta \cup \lbrace A_{1}, A_{2}, \ldots A_{n} \rbrace \subseteq \varDelta '$.

The proofs of $(1')$ to $(8')$ are straightforward. In order to prove $(Val')$, suppose $A_{1} \rightarrow (A_{2} \rightarrow \cdots \rightarrow (A_{n} \rightarrow B)\ldots ) \notin \varDelta$ and $\varDelta$ is A-saturated. So, $\varDelta \nvdash A_{1} \rightarrow (A_{2} \rightarrow \cdots \rightarrow (A_{n} \rightarrow B)\ldots )$, and consequently $\varDelta \cup \lbrace A_{1}, A_{2}, \ldots A_{n} \rbrace \nvdash B$. A B-saturated set $\varDelta '$ may be obtained from $\varDelta \cup \lbrace A_{1}, A_{2}, \ldots A_{n} \rbrace$ by means of a Lindenbaum construction.

Consider now the characteristic function v of the set $\varDelta$: in view of clauses $1'$ to $8'$ and $Val'$, v is a valuation for BLE and v is a model for $\varDelta$¹⁵. Since $\varGamma \subseteq \varDelta$, v is also a model for $\varGamma$. But $v(A)=0$, so $\varGamma \nvDash A$. By contraposition, completeness is thus obtained. $\square$

3.3.3 A decision procedure for BLE

In Examples 4 and 5 above we have seen how all possible valuations involved could be checked effectively by means of quasi-matrices. This depends essentially on the fact that in order to determine whether A follows from (finite) $\varGamma$, it is enough to check a finite number of valuations involving only subformulas and negated subformulas of $\varGamma \cup \{A\}$.

Theorem 8

Derivability in BLE is decidable.

Proof

From Lemma 1 item 5, derivability in BLE is compact. Given a derivation D of A from a (possibly infinite) set $\varGamma$, there will always be a finite set $\varGamma ^{0}$ such that $\varGamma ^{0}$ contains precisely the hypotheses of D. Let $Sub^{*}$ be the set of subformulas and negated subformulas of the formulas in $\varGamma ^{0} \cup \{A\}$. The set $Sub^{*}$ is finite, and a valuation depends on no more than the formulas in $Sub^{*}$. Consequently, the corresponding quasi-matrix is finite. So, checking clauses 1–8 of Definition 2 and the clause Val of Definition 3 is clearly computable. Hence, in view of completeness and soundness, derivability in BLE is decidable. $\square$

There is also an interesting result about BLE that we call ‘grounding of contradictoriness’. Roughly, it says that there can be no contradiction at all, unless there is some contradiction in the atomic level.

Fact 9

A compound formula A is contradictory in a valuation v (i.e. $v(A) = 1$ and $v(\lnot A)=1$) only if at least one atom p that occurs in A is contradictory in v.

Proof

Suppose there is a valuation v such that $v(A) = v(\lnot A) = 1$. By induction on the complexity of A, we prove that there is at least one atom p that occurs in A such that $v(p) = v(\lnot p) = 1$.

Base case$A = p$. Clearly, $v(A) = v(\lnot A) = v(p) = v(\lnot p) = 1$.

Inductive step We prove the case in which $A = B \rightarrow C$.

Inductive hypothesis if $v(B) = v(\lnot B) = 1$, then there is a p in B such that $v(p) = v(\lnot p) = 1$; mutatis mutandis for C. Suppose $v(B \rightarrow C) = v(\lnot (B \rightarrow C)) = 1$. So, by clauses 1 and 8 of Definition 2, $v(B) = v(C) = v(\lnot C) = 1$. Now, apply the inductive hypothesis. We leave the remaining cases to the reader. $\square$

Notice, however, that the converse does not hold: there may be a contradictory atom p in a formula A without A being contradictory. Let A be the formula $p \vee q$ and consider the valuation v such that $v(p) = v(\lnot p) = 1$, $v(q) = 1$ and $v(\lnot q) = 0$. In this case, $v(p \vee q) = 1$ but $v(\lnot (p \vee q)) = 0$.

It is also worth noting that the dual of Fact 9 with respect to undetermined formulas does not hold: there may be compound formulas A and valuations v such that $v(A) = 0$ and $v(\lnot A)=0$, although there is no atom p in A such that $v(p) = 0$ and $v(\lnot p)=0$. For example, it may be that $v(p \rightarrow q)=v(\lnot (p \rightarrow q)) = 0$ for $v(p) = 0$, $v(\lnot p)=1$, $v(q) = 0$ and $v(\lnot q)=1$ according to clauses 1 and 8 of Definition 2. In this aspect, BLE differs from intuitionistic logic.

Although it is almost obvious that BLE is equivalent of N4, for the sake of clarity we prove the fact below.

Fact 10

BLE is equivalent to Nelson’s logic N4.

Proof

The equivalence between N4 and BLE is straightforward from the natural deduction system for N4 presented by Wansing and Kamide (2015, Sect. 2.4). The latter slightly differs from the system we adopted in the negation rules (Sect. 3.2). Clearly, the rules $\lnot \wedge I$, $\lnot \vee I$, $\lnot \rightarrow I$, $\lnot \vee E$, $\lnot \rightarrow E$ are respectively equivalent in each system. The only case deserving attention is the equivalence between Wansing and Kamide’s rule $\lnot \wedge E$ (call it R1)

and ours (call it R2)

(i) In order to get R1 from R2, make $C = \lnot A \vee \lnot B$. The latter is obtained from $\lnot A$ (resp. $\lnot B$) by $\vee I$:

(ii) On the other hand, we get R2 from R1 by means of obtaining C from $\lnot A \vee \lnot B$ through $\vee E$:

$\square$

4 A logic of evidence and truth

Although the logic BLE is able to express preservation of evidence, it is not able to express preservation of truth. However, in some contexts of reasoning we deal simultaneously with truth and evidence, that is, with propositions that we take as conclusively established as true or false, as well as others for which only non-conclusive evidence is available. On the other hand, classical logic gives a very good, maybe the best possible, account of truth preservation. Thus, we get a tool for dealing with such contexts of reasoning if we are able to restore classical logic for propositions for which there is conclusive evidence, that is, those we want to declare either true or false. If classical logic holds with respect to such propositions, we may express (with respect to them) the relation of truth-preservation. What we need is to add to BLE the means of recovering the properties of classical negation—or, more precisely, we need to restore the validity of explosion and excluded middle with respect to those formulas for which we want to recover classical logic. This will be made clear in what follows.

4.1 Logics of formal inconsistency and undeterminedness

The Logics of Formal Inconsistency (from now on, LFIs), are a family of paraconsistent logics able to express, inside the object language, the notions of ‘non-explosiveness’, ‘consistency’, or even ‘inconsistency’, as applied to formulas. This is done by means of adding a unary propositional connective $\circ$ to the language, where $\circ A$ means that A is consistent.¹⁶

Explosion holds only with respect to propositions marked with $\circ$, i.e. consistent (in some sense) propositions. Although explosion is not valid simpliciter in the sense that

• for some $\varGamma$, A and B: $\varGamma , A, \lnot A \nvdash B$,

the following always holds:

• for every $\varGamma$, A and B: $\varGamma , \circ A, A, \lnot A \vdash B$.

In any paraconsistent logic with few logical resources it cannot be that all contradictions are logically equivalent, otherwise the principle of explosion would hold. Indeed, suppose that for any A and B, $A \wedge \lnot A \dashv \vdash B \wedge \lnot B$. Then, $A \wedge \lnot A \vdash B \wedge \lnot B$, and by conjunction-elimination, $A \wedge \lnot A \vdash B$. Rephrased contrapositively, this means that if a logic is paraconsistent, then it has some pairs of non-equivalent contradictions. This nonequivalence between contradictions fits the idea that in real-life contexts of reasoning some contradictions are more relevant than others. In such contexts, information contradicting a proposition that has been conclusively established as true is immediately rejected as false. Hence, it seems natural to have a connective able to distinguish ‘different kinds’ of contradictions, separating the contradictions that do not lead to explosion from those that do.

The idea that leads to the restriction of explosion—separating propositions into those for which some logical property holds and those for which it does not—is generalizable. In particular, excluded middle may be restricted in an analogous way. A Logic of Formal Undeterminedness (LFU) is a logic such that its language is extended by a new unary connective , where means that A is (in some sense) determined.¹⁷ Excluded middle does not hold, that is

• for some $\varGamma$, A and B: $\varGamma , A \vdash B, \varGamma , \lnot A \vdash B \text{ but } \varGamma \nvdash B,$

while the following always hold:

• for every $\varGamma$, A and B: if $\varGamma , A \vdash B \text{ and } \varGamma , \lnot A \vdash B$, then .

As we have seen above, it cannot be that all contradictions are equivalent in a paraconsistent logic. Similarly, in a paracomplete logic in which transitivity and $\vee I$ hold (BLE for example), it cannot be that all instances of $A \vee \lnot A$ are equivalent, otherwise excluded middle would be unconditionally valid. A proof of this follows. Let A be any theorem. Since $A \vdash A \vee \lnot A$, if for any A and B, $A \vee \lnot A \dashv \vdash B \vee \lnot B$, by transitivity it follows that $A \vdash B \vee \lnot B$. As A is a theorem, we conclude $\vdash B \vee \lnot B$. This, however, contradicts the definition of a paracomplete logic.

4.2 The logic $\textit{LET}_{J}$

An LFI and an LFU may be combined in an LFIU—a Logic of Formal Inconsistency and Undeterminedness. In a context that is at the same time paraconsistent and paracomplete, we may recover at once explosion and excluded middle with respect to a given formula A. Since consistency and determinateness are recovered simultaneously, we change the symbol to $\circ$. An LFIU is obtained by adding the following inference rules to the logic BLE:

We call $\textit{LET}_{J}$ the logic defined by the addition of $EXP^{\circ }$ and $PEM^{\circ }$ to BLE. The name $\textit{LET}_{J}$ stands for ‘logic of evidence and truth based on positive intuitionistic propositional logic’. The language $L_{1}$ of $\textit{LET}_{J}$ is the language $L_{0}$ of BLE plus the unary connective $\circ$. The definition of the set $S_{1}$ of formulas of $L_{1}$, and the other definitions, are analogous. $\textit{LET}_{J}$ enjoys properties P1 to P5 of Lemma 1, and is also a Tarskian logic. Notice that $EXP^{\circ }$ and $PEM^{\circ }$ may be considered elimination-rules for $\circ$, but it is not by accident that there is no introduction-rule for $\circ$ (we will return to this point soon).

In $\textit{LET}_{J}$, the connective $\circ$ works as a classicality operator in the sense that $\circ A$ recovers classical logic for any formula that depends only on A and is formed with $\lnot$, $\wedge$, $\rightarrow$ and $\vee$ (see Fact 18 below). From ‘outside’ of the system, $\circ A$ may be informally understood as saying that the truth-value of A has been (or may be) conclusively established. So,

• ‘$\circ A \wedge A$ holds’ means ‘A is true’,

• ‘$\circ A \wedge \lnot A$ holds’ means ‘A is false’.

It is important to emphasize that the particular way in which the truth or falsity of a proposition is going to be established is not a problem of logic. Truth comes from outside the formal system. The latter is no more than a tool that allows the recovering of classical consequence, and thus truth-preservation, with respect to some formulas. If classical logic holds for A, it cannot be the case that there is still conflicting evidence for A and for $\lnot A$. If A has been established as true, any evidence for $\lnot A$ is canceled (mutatis mutandis when A is false).

It is also worth noting that in $\textit{LET}_{J}$ classical and paraconsistent logic coexist pacifically. $\circ$ works like an indicator of a context switch: for formulas marked with $\circ$ the context is classical, otherwise, the context is paraconsistent and paracomplete. There is, thus, no rivalry between classical and paraconsistent approaches, and this is made possible by the fact that, according to the proposed interpretation, classic and paraconsistent logics are ‘talking about different things’.

4.3 A semantics for $\textit{LET}_{J}$

In order to extend the semantics presented in Sect. 3.3 to $\textit{LET}_{J}$ we need only to add the clause

• 9. $s(\circ A)=1$ implies [$s(\lnot A)= 1$ iff $s(A)=0$]

to Definition 2. Clause 9 above says that if $\circ A$ holds, we secure classical conditions for negation, but not the converse. Indeed, there may be a valuation such that $s(\lnot A)= 1$ and $s(A)=0$ (or vice-versa) but $\circ A$ still does not hold. Informally, this is understood as saying that there may be evidence only for A, or only for $\lnot A$, but such evidence is non-conclusive. The semantics so obtained is sound, complete, and yields a decision procedure for $\textit{LET}_{J}$.

Theorem 11

Soundness and completeness: $\varGamma \vDash _{\textit{LET}_{j}} A$ iff $\varGamma \vdash _{\textit{LET}_{j}} A$.

Proof

In order to prove completeness, the proof of Sect. 3.3.2 is modified to include clause $9'$ below:

$9'.$ :

$\circ A \in \varDelta$ implies $\lnot A \in \varDelta$ iff $A \notin \varDelta$.

For soundness, it suffices to modify the proof of Sect. 3.3.1, showing that the rules $EXP^{\circ }$ and $PEM^{\circ }$ are sound with respect to clause 9 above. Details are left to the reader. $\square$

Theorem 12

Derivability in $\textit{LET}_{J}$ is decidable.

Proof

The argument is similar to the proof of the decidability of BLE (Theorem 8). The set $Sub^{*}$ is finite, so the number of valuations, and the quasi-matrices, are also finite. The only difference concerns clause 9 above. All checking procedures involved are clearly computable. Hence, in view of completeness and soundness, derivability in $\textit{LET}_{J}$ is decidable. $\square$

4.4 Some facts about $\textit{LET}_{J}$

The logic $\textit{LET}_{J}$ has features that fit the intuitive interpretation based on evidence and truth presented here. We show some of them below.

Fact 13

A bottom particle $\bot$ (that is, a formula that by itself trivializes the system) is definable in $\textit{LET}_{J}$.

Proof

Define $\bot ~{\mathop {=}\limits ^{\text {{\tiny def }}}}~\circ A \wedge A \wedge \lnot A$. It can be proved in a few steps that $\bot \vdash B$ for any B. $\square$

Fact 14

$\textit{LET}_{J}$ has no trivial models, hence $\textit{LET}_{J}$ does not prove $\bot$.

Proof

Semantic clause 9 relates $\circ$ and $\lnot$ in such a way that trivial models are excluded. In other words, in $\textit{LET}_{J}$ there is no valuation v such that for every formula A of $L_{1}$, $v(A) = 1$. As a consequence, given soundness, $\textit{LET}_{J}$ does not prove $\bot$, as defined in Fact 13. $\square$

The above result is the paraconsistent counterpart of the usual consistency proofs. Since triviality in paraconsistent logic is not equivalent to freedom from contradiction, the relevant result, tantamount to proving consistency (as freedom from contradiction) when the underlying logic is classical, is to prove that $\bot$, or whatever would entail triviality, is not a theorem.

Fact 15

$\lnot (A \wedge \lnot A)$ and $A \vee \lnot A$ are logically equivalent in $\textit{LET}_{J}$. But neither of them is logically equivalent to $\circ A$.

Proof

Since DN (double negation) holds, $A \vee \lnot A$ is equivalent to $\lnot A \vee \lnot \lnot A$, and the latter, in its turn, is easily proved to be equivalent to $\lnot (A \wedge \lnot A)$. In $\textit{LET}_{J}$, $\circ A \vdash \lnot (A \wedge \lnot A)$. Suppose $\circ A$. So, $A \vee \lnot A$. The latter implies $\lnot A \vee \lnot \lnot A$, which is equivalent to $\lnot (A \wedge \lnot A)$. To see that neither $\lnot (A \wedge \lnot A)$ nor $A \vee \lnot A$ implies $\circ A$, take $v(A) = 1$, $v(\lnot A) = 0$ and $v(\circ A) = 0$. $\square$

It is worth noting that the above non-equivalence fits the intuitive interpretation proposed here: it may be the case that $\lnot (A \wedge \lnot A)$ holds even if $\circ A$ does not hold. Accordingly, there may be a situation such that there is some non-conclusive evidence for the truth of A but no evidence for the falsity of A. In this case, $v(\lnot (A \wedge \lnot A))=1$, although $v(\circ A) = 0$, since the evidence available is non-conclusive. On the other hand, if $v(\circ A) = 1$, there are only two possibilities: either $v(A) = 1$ and $v(\lnot A) = 0$, or $v(A) = 0$ and $v(\lnot A) = 1$.

Fact 16

The formulas $A \wedge \lnot A$ and $\circ (A \wedge \lnot A)$ jointly trivialize the consequence relation of $\textit{LET}_{J}$.

Proof

$A \wedge \lnot A$ implies $\lnot A$. Applying $\vee I$ we get $A \vee \lnot A$, that is equivalent to $\lnot (A \wedge \lnot A)$, and triviality follows from Fact 13, since $A \wedge \lnot A$, $\circ (A \wedge \lnot A)$ and $\lnot (A \wedge \lnot A)$ define a bottom particle. $\square$

Given that according to the intuitive interpretation proposed here a true contradiction is expressed in $\textit{LET}_{J}$ by $(A \wedge \lnot A) \wedge \circ (A \wedge \lnot A)$, the consequence relation of $\textit{LET}_{J}$ trivializes in the presence of a true contradiction. Therefore, Fact 16 implies that $\textit{LET}_{J}$ is anti-dialetheist in the sense that it cannot tolerate any true contradiction.

Fact 17

The logic $\textit{LET}_{J}$ does not have any theorem of the form $\circ A$.

Proof

The strategy of this proof is to show that $\circ A$ is independent of the rules and therefore cannot be a consequence of the rules of $\textit{LET}_{J}$. Consider for this purpose the following alternative semantics: for the connectives $\vee$, $\wedge$, $\rightarrow$ and $\lnot$, the classical conditions over $\lbrace 0, 1\rbrace$; for $\circ$, $v(\circ A) = 0$ for any value of A. According to this semantics, no rule of $\textit{LET}_{J}$ yields a conclusion with value 0 if all premises have value 1, that is, the rules are sound w.r.t. this new semantics. On the other hand, a formula $\circ A$ receives 0 for any A. Hence, such a formula is independent of the rules, and cannot be proved in $\textit{LET}_{J}$. $\square$

This result is in accordance with the intuitive idea that the attribution of $\circ$ to a formula A may be done only from outside the formal system. It is the user of the system who establishes under which circumstances a formula may be marked with $\circ$. That there is no introduction rule for $\circ$ is an intentional limitation of the formal system. What constitutes evidence for a given proposition A, and whether or not such evidence is conclusive and A may be established as true, are problems that depend on the specific area of knowledge being dealt with. These problems must be kept outside the formal system.

Fact 18

If $\circ A_{1}$, $\circ A_{2}$, ...$\circ A_{n}$ hold, then all formulas that depend only on $A_{1}$, $A_{2}$, ...$A_{n}$ and are formed with $\rightarrow$, $\wedge$, $\vee$ and $\lnot$ behave according to classical logic.

Proof

Let $A_{1}, A_{2}, \ldots A_{n}$ be any formulas and $B = \phi (A_{1}, A_{2}, \ldots A_{n})$ be any composed formula formed by one or more formulas among $A_{1}, A_{2}, \ldots A_{n}$ through $\lnot$, $\rightarrow$, $\wedge$ and $\vee$. We prove below by induction on the complexity of B that if $\circ A_{1}, \circ A_{2}, \ldots \circ A_{n}$ hold, then the rules

hold. Therefore, all such formulas behave according to classical logic.

Base$B = A_{i}$ (for any i). The proof is straightforward.

Inductive step

Case 1$B = \lnot C$. We prove PEM. The inductive hypothesis is the rule below:

In order to prove that

holds, we need only an application of DN. The proof of EXP is left to the reader.

Case 2$B = C \vee D$.

We prove EXP. The inductive hypothesis is:

The proof of PEM and the remaining cases ($\wedge$ and $\rightarrow$) are left to the reader. $\square$

A corollary of Fact 18 is that once a formula A is marked with $\circ$, no contradiction is allowed with respect to formulas with $\lnot$, $\vee$, $\wedge$ and $\rightarrow$ that depend only on A. However, from this, it does not follow that any formula that depends only on A is also marked with $\circ$. Again, the point is that the attribution of $\circ$ to any formula can be done only from outside the formal system. It must always be a proposition added to the theory at stake by means of non-logical means. Classicality does not propagate through the connectives.

It is also worth mentioning that a corollary of Fact 18 is a perspicuous form of a derivability adjustment theorem (DAT). The purpose of a DAT is to establish a relationship between two logics in the sense of restoring inferences that are lacking in one of them.¹⁸ The basic idea is that we have to ‘add some information’ to the premises in order to restore the inferences that are otherwise lacking. The general form of a DAT is the following:

• For all $\varGamma$ and B, there is a $\varDelta$ such that: $\varGamma \vdash _{L} B$ iff $\varGamma , \varDelta \vdash _{L*} B$.

Suppose that the logic L above is classical logic and $L *$ is $\textit{LET}_{J}$. The result above is tantamount to a DAT that specifies how classical logic may be recovered: the ‘information’ required (represented by the set $\varDelta$) consists of the atomic propositions that occur in $\varGamma$, marked with $\circ$.

5 On some issues related to paraconsistency as preservation of evidence

5.1 A remark on Restall’s approach to logical pluralism

What we have done here clearly indicates an approach to logical pluralism: different accounts of logical consequence may preserve different properties of propositions. We do not think that logical consequence has to be always identified with preservation of truth. Thus, classical, paracomplete (e.g. intuitionistic) and paraconsistent logics may be interpreted as being concerned with preservation of, respectively, truth, availability of a constructive proof (a notion stronger than truth) and availability of evidence (a notion weaker than truth).

Restall (2014) presents a proof-theoretic approach to logical pluralism in terms of different standards of proof based on the duality between paraconsistency and paracompleteness, a point also emphasized by us (see Carnielli and Rodrigues 2016). A detailed analysis of Restall’s arguments is outside the scope of this text. But his approach differs significantly from ours for two main reasons. First, as much as in Beall and Restall (2006), what is at stake in Restall (2014) is truth-preservation.¹⁹ The same argument can be valid in one sense and invalid in another, but in both cases truth is the property of propositions being preserved (Restall 2014, p. 280). Second, although interesting from the technical point of view, Restall’s approach does not seem to be an attempt to represent inferences accepted in real-life argumentative scenarios.

The dual-intuitionistic logic in Restall (2014) is a paraconsistent logic obtained by restricting inference rules of classical sequent calculus in such a way that at most one formula occurs in the left hand side of a sequent (Restall 2014, p. 283). Restall’s approach sheds light on interesting features of the duality between paraconsistency and paracompleteness. But it is not clear that the paraconsistent logic so obtained really intends to correspond to real argumentative contexts. However, this does not make Restall’s dual-intuitionistic logic uninteresting; it just makes his approach different from ours. Instead, the approach to paraconsistency worked out here has tried, from the beginning, to find a way to interpret contradictions that appear in real-life contexts of reasoning. From the guiding question what does it mean to acceptAand$\lnot A$simultaneously without accepting their truth? we reached the notion of evidence. The next step was to find inference rules appropriate to express preservation of evidence.

The view we endorse w.r.t. the duality between paraconsistency and paracompleteness is that logics intended to represent real-life argumentative contexts have a common core (e.g. PIL) to which dual inference rules (and perhaps something else) are added. Excluded middle and explosion are dual inference rules in the sense that anything follows from $A \wedge \lnot A$, while $A \vee \lnot A$ follows from anything (see Carnielli and Rodrigues 2016, Sect. 2).

5.2 A remark on the problem of ‘just true, just false’

Under the intended interpretation, $\textit{LET}_{J}$ is immune to the problem of ‘just true, just false’, faced by the so-called ‘glut-theorists’ (see, e.g. Beall 2013). We do not need to distinguish a scenario in which a formula A is just true (or just false) from a scenario in which A is both true and false because the latter is avoided in the intuitive interpretation proposed here: the simultaneous truth and falsity of A is expressed by $(A \wedge \circ A) \wedge (\lnot A \wedge \circ A)$, and this formula in $\textit{LET}_{J}$ implies triviality. It may happen that in $\textit{LET}_{J}$A and $\lnot A$ hold together, but only if $\circ A$ does not—and in this case it does not mean that A is both true and false, but only that there is conflicting evidence w.r.t. A.

It is worth noting, however, that nothing a fortiori prevents the formal system of $\textit{LET}_{J}$ of being interpreted differently, even in a dialetheist way. So, in such an alternative interpretation, it is remarkable that $\textit{LET}_{J}$ would have the means to solve the problem of ‘just true, just false’ just by assuming that $A \wedge \lnot A$ means that A is both true and false, while $\circ A \wedge A$ (resp. $\circ A \wedge \lnot A$) means that A is only true (resp. only false).

5.3 Evidence versus constructive falsity

Nelson (1949), extending a proposal of Kleene (1945), suggested a constructive interpretation for the first-order number theory based on the formal system N of ‘constructible negation’. Nelson (1959) introduced a paraconsistent system called S (not yet the well-known N4), and remarked that “In both the intuitionistic and classical logic all contradictions are equivalent. This makes it impossible to consider such entities at all in mathematics” (Nelson 1959, p. 209, our emphasis). Later, Almukdad and Nelson proposed the logic $N^-$, saying only that it is “a constructive logic which may be applied to inconsistent subject matter without necessarily generating a trivial theory” (Almukdad and Nelson 1984, p. 231). The difference between N and $N^-$ is that explosion does not hold in the latter, but holds in the former. Following Odintsov (2003, 2008), the propositional fragments of Nelson’s logics N and $N^-$ have been dubbed, respectively, as N3 and N4, and the latter became the standard presentation of Nelson’s paraconsistent logic.

The notion of realizability (Kleene 1945) can be understood as the formal side of the BHK interpretation of intuitionistic logic. Since in BHK the idea of proof is informal, the notion of realizability defines a formal notion of ‘proof’ by appealing to the notion of ‘realizers’ (see Rose 1953). The property of realizability is thus a kind of ‘intuitionistic notion of truth’ for intuitionistic number-theoretic statements. According to Kleene’s formulation, formulas of intuitionistic arithmetic are realized by (inductively defined) Gödel numbers of constants and of general recursive functions. Nelson (1949) extended Kleene’s approach, defining both a notion of ‘positive’ and ‘negative’ realizability. The latter adds a new feature to intuitionistic logic: formulas can also be constructively falsified.²⁰ So, Nelson’s motivation for proposing a constructive negation was to overcome non-constructive features of the intuitionistic negation. Indeed, negations in both N3 and N4 satisfy De Morgan’s laws, as well as the following meta-property:

$$\begin{aligned} \vdash \lnot (A \wedge B) \ \text{ implies } \ \vdash \lnot A \ \text{ or } \ \vdash \lnot B. \end{aligned}$$

It seems plausible, from the constructive viewpoint, that if $A \wedge B$ has been proved false, then either a proof of the falsity of A or a proof of the falsity of B is available. The constructive negation of N3 (and, of course, of N4) may be also interpreted as refutability (see López-Escobar 1972). By treating constructive falsity independently of constructive truth, refutability becomes not complementary to provability—i.e. constructive falsity does not coincide with the complement of constructive truth (an ‘asymmetry’ similar to that between positive and negative evidence).

It is clear, thus, that Nelson was interested in constructive mathematics: this was the framework in which N3 and N4 were conceived. The motivation for BLE is quite different. Its inference rules have been established according to the question posed in Sect. 3: supposing the availability of evidence for the premises, we ask whether an inference rule yields a conclusion for which evidence is available.²¹BLE expresses, as we have seen in Sect. 3, four different scenarios corresponding to positive evidence, absence of positive evidence, negative evidence and absence of negative evidence. On the other hand, the similarity between the intended interpretation of BLE and Nelson’s notion of constructive falsity lies in the fact that the notion of evidence for the falsity of A is not complementary to the notion of evidence for the truth of A: absence of evidence for falsity does not count as evidence for truth, and vice-versa. So, the notion of evidence for falsity is primitive in the sense that it does not coincide with the complement of evidence for truth.

BLE is not able to express, in the intended intuitive interpretation, a scenario in which the evidence for A is conclusive. This can be done by $\textit{LET}_{J}$, by means of the classicality operator: $A \wedge \circ A$ means that A holds and behaves classically. But in such a case, A is true—mutatis mutandis for the falsity of A, expressed in $\textit{LET}_{J}$ by $\lnot A \wedge \circ A$. That is precisely the point of $\textit{LET}_{J}$: since the formulas marked with $\circ$ behave classically, we may say that they are true (or false) and that there is conclusive evidence for their truth (or falsity). So, in $\textit{LET}_{J}$, if $\circ A$ holds, the notions of truth and falsity turn out to be complementary: either A is true, or A is false.

6 Final remarks

We have presented here an approach to paraconsistency that explicitly rejects dialetheism. According to the intended interpretation of $\textit{LET}_{J}$, true contradictions are not allowed because they imply triviality (see remarks on Fact 16). There is no way to explain a context of reasoning in which a pair of propositions A and $\lnot A$ simultaneously hold, without being dialetheist or metaphysically neutral, unless a property weaker than truth is attributed to A and $\lnot A$. Our proposal here (our answer to question Q posed in Sect. 1) is that evidence, in the sense explained in the Sect. 2, may be such a property. Thus, the principle of explosion is rejected because a circumstance such that there is (non-conclusive) evidence for both A and $\lnot A$, while there is no evidence for some proposition B, is completely feasible. This is an epistemic approach since evidence is an epistemic concept. But we can go one step further and say that our approach to paraconsistency is radically epistemic because true contradictions are not tolerated—as we have seen, they imply triviality as much as they do in classical logic.

We believe, however, that no philosophical, a priori argument can conclusively confirm or reject the claim that some aspects of reality need contradictory propositions in order to be described. In fact, ‘real contradictions’ seem to be quite impossible, but of course we cannot, and do not intend to, prove that. The intuitive interpretation proposed for the formal system $\textit{LET}_{J}$ would fail if it were confirmed someday that real contradictions do exist. But in such an improbable scenario, a considerable part of science, and also of philosophy, would collapse altogether.