A Method of Defining Paraconsistent Tableaus

Abstract

The aim of this paper is to show how to simply define paraconsistent tableau systems by liberalization of construction of complete tableaus. The presented notions allow us to list all tableau inconsistencies that appear in a complete tableau. Then we can easily choose these inconsistencies that are effects of interactions between premises and a conclusion, simultaneously excluding other inconsistencies. A general technique we describe is presented here for the case of Propositional Logic, as the simplest one, but it can be easily extended to more complex cases. In other words, a kind of paraconsistent consequence relation is being studied here, and a simple tableau system is shown to exist that captures that consequence relation.

This work was completed with the support of Polish National Center of Science NCN UMO-2012/05/E/HS1/03542.

1 Introduction and Overview

In this article, we study some kind of paraconsistent consequence relation that is determined by tableau system. That is why we start with some remarks on tableau methods and a strategy we implement.

Usually, tableau methods are at the same time effective but rather intuitive and nonformal. One of the many problems of this is that when we develop a tableau, we can many times obtain the same expressions or apply rules to branches that contain inconsistent expressions. It is a reason why a formal approach to tableau methods that exclude such situations are studied.

Although we prepared a formal theory of tableaus [2] that prevents from a jeJune way of application of tableau rules—among others, they cannot be applied to branches that contain inconsistent expressions—here we defined rules as blind. It means that tableau inconsistencies that occur in tableaus do not stop developing of a given tableau. We do not stop a proof, till we decompose all expressions. It is because in the case of paraconsistent arguments we look for a special kind of inconsistency that follows from incompatibility of premises and a negated conclusion. In order to identify suitable inconsistencies in a tableau, we need to decompose all expressions to the level of literals in such a way that it would give an answer to the question whether there is a collision between premises and a negated conclusion or not.

In Sect. 14.3, we describe a mechanism of building such tableaus and choosing suitable inconsistencies. In further parts, we analyze some metatheoretical properties of this proposal and a paraconsistent consequence relation that it captures.

In the article, we consider the simplest case, the case of Propositional Logic, and its paraconsistent subrelation determined by described tableaus. This type of approach can be applied to other logics, being generalized as long as tableau rules are defined in the proposed style.

Finally, let us add that in our paper the tableau tools are treated as a fully syntactical method of checking whether arguments are correct and—as a counterpart of a consequence relation—defined semantically.

2 Basic Notions

In this part of paper, we remind some semantical notions and basic tableau notions we need to formulate and prove facts about paraconsistent tableaus that define a paraconsistent subrelation of the classical propositional consequence relation.

2.1 Classical Propositional Consequence Relation

Let $\textsf {For}$ be the set of all formulas build over the following alphabet: $\textsf {Var} \cup \{\lnot , \wedge , \vee , \rightarrow , \leftrightarrow \}$. Let $V: \textsf {For} \longrightarrow \{0, 1\}$ be a valuation of formulas, so for any A, $B \in \textsf {For}$ the function V satisfies conditions:

• $V(\lnot A) = 1$ iff $V(A) = 0$

• $V(A \wedge B) = 1$ iff $V(A) = 1$ and $V(B) = 1$

• $V(A \vee B) = 1$ iff $V(A)=1$ or $V(B) = 1$

• $V(A \rightarrow B)$ iff $V(A) = 0$ or $V(B) = 1$

• $V(A \leftrightarrow B)$ iff $V(A) = V(B)$.

Let ${{\mathbf {\mathsf{{V}}}}}$ be a set of all valuations of formulas. Having a set of formulas X and a valuation V we say that X is true in V (in short: $V(X) = 1$) iff for all $A \in X$, $V(A) = 1$. If a set of formulas X is not true in V, we say that is false in V and write $V(X) = 0$.

We define classical consequence relation $\models$ on $2^{\textsf {For}} \times \textsf {For}$ in a standard way. Hence, for any formula A and set of formulas X we say that A is a consequence of X (in short: $X \models A$) iff $\forall _{V \in {{\mathbf {\mathsf{{V}}}}}} (V(X) = 1 \Longrightarrow V(A) = 1)$.

We say that a set of formulas X is inconsistent iff for any valuation $V(X) = 0$. Otherwise, we call X consistent.¹ Now, by definition of classical consequence relation $\models$, we have a conclusion that expresses a vulnerability of classical logic to inconsistent sets of premises.

Corollary 14.2.1

Let X be an inconsistent set of formulas. Then $X \models A$, for all $A \in \textsf {For}$.

Of course, no paraconsistent logic should have the above property.

2.2 Tableau System for Propositional Logic

In work [3] and especially in [2], we presented a formal theory of tableau systems for a class of logics defined by some syntactical and semantical conditions.² Hence, we have precise tableau notions that incorporate standard, intuitive notions. The precise notions (of a tableau rule and various kinds of branches, tableaus etc.) with a notion of tableau system are necessary, when we generalize results, looking for some abstract properties of tableau methods.

However, here we dealt with tableaus for Boolean language, so we just use well-known intuitive tableau notions presented in many publications, for example in [1]. We remind them in turn giving a handful of nonformal but instructive definitions as usually authors do.

We assume that a set of formulas X are t-inconsistent iff for some $A \in \textsf {For}$, X contains A and $\lnot A$. A set of formulas X is t-consistent iff X are not t-inconsistent. By $\mathbf R$ we denote a set of all standard tableau rules for Boolean connectives. We have nine rules in $\mathbf R$: four positive rules (for $\wedge$, $\vee$, $\rightarrow$, $\leftrightarrow$) and five negative (for $\lnot \lnot$, $\lnot \wedge$, $\lnot \vee$, $\lnot \! \rightarrow$, $\lnot \!\leftrightarrow$).³

A root is a set that contains premises and a negation of conclusion. A branch is a sequence of formulas that starts from a root. The rest of the branch contains results of applying of rules to former formulas. A branch is complete iff all applicable tableau rules were used.⁴ A branch is incomplete iff it is not complete. Branches can be also closed or open. A branch is closed iff it contains t-incosistent set of formulas; it is open iff is not closed.

Tableau can be treated as sets of branches with the same roots. Tableaus that include all suitable and only complete branches are called complete. Complete tableaus can be closed or open. A tableau is closed iff it is complete and all branches that includes are closed; it is open iff is not closed.

Now, for any set of formulas X and a formula A, we define a tableau classical consequence relation $\vartriangleright$, by putting:

Definition 14.2.2

$X \vartriangleright A$ iff there exist a finite subset Y of X and a closed tableau with a root $Y \cup \{\lnot A \}$.

Of course, the relation $\vartriangleright$ is fully determined by tableau rules of $\mathbf R$. Therefore, by $\langle \textsf {For}, \vartriangleright \rangle$ we understand a tableau system determined by classical tableau rules $\mathbf R$. The tableau system defines Propositional Logic, since it is well-known that:

Fact 14.2.3

For all $X \subseteq \textsf {For}$, $A \in \textsf {For}$, $X \vartriangleright A$ iff $X \models A$.

3 Paraconsistent Tableaus

As we said our aim is to define a paraconsistent tableau inference that defines some paraconsistent subrelation of classical propositional consequence relation. However, first we introduce some auxiliary notions.

Let $\mathbb {N}$ be the set of natural numbers—the set of indexes $\mathbb {I} = \mathbb {N} \cup \{ 0 \}$. We distinguish an index zero: 0 for conclusions of a given tableau proof.

Next, we define a set of formulas indexed by superscripts: $\textsf {For}' = \{ A^{i}: A \in \textsf {For}, i \in \mathbb {N}\}$. The expressions from $\textsf {For}'$ will represent formulas from $\textsf {For}$ in tableau proofs. Notice that no formula in $\textsf {For}'$ has a superscript 0.

By the function $\bullet : \textsf {For}' \cup \{A^{0}: A \in \textsf {For} \} \longrightarrow \mathbb {N} \cup \{ 0\}$, defined with the condition $\bullet (A^{i}) = i$, we can choose superscripts that occur in formulas $\textsf {For}'$ and of those formulas that have a superscript 0.

Let X be a subset of $\textsf {For}$. By X(x) we mean such a non-empty subset of powerset of $\textsf {For}'$ that for all $Y \in X(x)$ and all $A, B \in \textsf {For}$ the conditions are fulfilled:

• 1. $A \in X$ iff for some $i \in \mathbb {N}$, $A^{i} \in Y$

• 2. for any $i, j \in \mathbb {N}$, if $A^{i}, B^{j} \in Y$ then one of the below holds:

  • (a) $A \ne B$ and $i \ne j$

  • (b) $A = B$ and $i = j$.

Of course, for a set of formulas X there are usually many sets satisfying X(x)–conditions, so writing $Y \in X(x)$ we mean some arbitrary, but fixed set from X(x) that we take into consideration.

Now we give a notion of a particular kind of t-inconsistency. We mean an inconsistency that is a result of expressions with some fixed indexes. Surely, this notion is based on a usual notion of inconsistency (defined here Sect. 14.2.2), so it is still about a set of formulas that contains A and $\lnot A$, for some formula A, but additionally both inconsistent formulas should have indexes of some kind. Formally, let $i, j \in \mathbb {I}$ and $X \subseteq \textsf {For}'\cup \{A^{0}: A \in \textsf {For} \}$. X is $t^{i, j}$-inconsistent iff for some A, B:

• 1. $\{A, B \} \subseteq X$

• 2. $\{A, B \}$ is a t-inconsistent set of formulas

• 3. $\{ \bullet (A), \bullet (B)\} = \{i, j \}$.

It is a particular kind of t-inconsistency, because it refers to some superscripts omitting t-inconsistencies with other superscripts. Hence, a set Y of formulas with superscripts can be t-inconsistent, but not $t^{i, j}$-inconsistent, for some $i, j \in \mathbb {I}$, since no pair of t-inconsistent formulas in Y contains superscripts i, j. On the other hand, the opposite relationship holds: if a set is $t^{i, j}$-inconsistent, for some $i, j \in \mathbb {I}$, it is also just t-inconsistent.

Now, we reformulate the tableau rules of $\mathbf R$. A new set of rules $\mathbf R '$ is defined on $\textsf {For}' \cup \{A^{0}: A \in \textsf {For} \}$. For all $i \in \mathbb {I}$ the schemas of new rules are as below:

$R_{\wedge }\!:$ $\frac{(A \wedge B)^{i}}{ A^{i}, B^{i}}$       $R_{\vee }\!:$ $\frac{(A \vee B)^{i}}{ A^{i} || B^{i} }$       $R_{\rightarrow }\!:$ $\frac{(A \rightarrow B)^{i}}{ \lnot A^{i} || B^{i}}$

$R_{\leftrightarrow }\!:$ $\frac{(A \leftrightarrow B)^{i}}{A^{i}, B^{i} || \lnot A^{i}, \lnot B^{i} }$       $R_{\lnot \lnot }\!:$ $\frac{ \lnot \lnot A^{i}}{ A^{i}}$       $R_{\lnot \wedge }\!:$ $\frac{\lnot ( A \wedge B)^{i}}{\lnot A^{i} || \lnot B^{i}}$

$R_{\lnot \vee }\!:$ $\frac{ \lnot (A \vee B)^{i}}{\lnot A^{i}, \lnot B^{i}}$       $R_{\lnot \, \rightarrow }\!:$ $\frac{\lnot (A \rightarrow B)^{i}}{ A^{i}, \lnot B^{i}}$       $R_{\lnot \, \leftrightarrow }\!:$ $\frac{\lnot (A \leftrightarrow B)^{i}}{\lnot A^{i}, B^{i} || A^{i}, \lnot B^{i} }$

The tableau rules in $\mathbf R '$ have such a property that they preserve superscripts. For example, when we decompose a formula $\lnot \lnot p^{1}$ by rule for $\lnot \lnot$, we obtain $p^{1}$; if we decompose a formula $(p \rightarrow q)^{0}$ by rule for $\rightarrow$, we obtain on the left branch $\lnot p^{0}$ and on the right branch $q^{0}$ etc. The technique allows us to trace a process of decomposition of formulas and find out the origin of t-inconsistencies.

As we already said, we resign here from internal mechanism nested in rules that blocks applying rules to branches including t-inconsistencies (it was one of distinguishing features of our last works [2, 3]). Here, we want to develop branches as long as it is possible in order to get all t-consistencies that a branch can generate. Now it is clear why we call these rules ‘blind’—they just do not see that a branch is closed, which normally is a sufficient fact to stop applying rules.

Moreover, we assume all definitions for tableaus for Propositional Logic—obviously, now the notions depend on the new set of tableau rules $\mathbf R '$. However, we add one more definition for testing its properties.

Definition 14.3.1

Let $Y \in X(x)$, for some $X \subseteq \textsf {For}$, and let $B \in \textsf {For}$. A tableau T with a root $Y \cup \{ \lnot B^{0} \}$ is paraconsistently closed iff:

• 1. T is complete

• 2. for any branch b in T there is such index $i \in \bullet (Y \cup \{ \lnot B^{0}\})$ that a $t^{i, 0}$-inconsistent set of formulas belongs to b.

Now, we explain the conditions in Definition 14.3.1 one by one. First, we have some set of formulas X and a formula B that is supposed to follow from X. We do not assume that X is a finite set, since by defining a suitable tableau consequence relation, we will impose a constraint that there must exist a finite set as a root for some complete and closed tableau (like in the case of classical tableau consequence relation Definition 14.2.2), so below we give examples only for finite cases.

We take a set $Y \in X(x)$, so Y has all and only formulas from X, each one with a different index. We build a complete tableau with the root $Y \cup \{ \lnot B^{0} \}$. Now, if on any branch there is a $t^{i, 0}$-inconsistency, for some $i \in \bullet (Y \cup \{ \lnot B^{0} \})$, then the tableau is paraconsistently closed. If for some branch there is no $t^{i, 0}$-inconsistency, for any $i \in \bullet (Y\cup \{ \lnot B^{0} \})$, then the tableau is not paraconsistently closed.

Now we present few simple examples of paraconsistently closed tableaus (according to our last Definition 14.3.1) for some key cases.

Example 14.3.1

Consider a set of premises $X = \{ p \wedge \lnot p \}$ and a possible conclusion q. We take a root $\{ (p \wedge \lnot p)^{1}, \lnot q^{0} \}$ and draw a tableau.

As we see it is not a paraconsistently closed tableau. In some branch (there is of course only one branch) there is no $t^{i,0}$-inconsistency, for any index i. Admittedly, we have a t-inconsistent set $\{ p^{1}, \lnot p^{1} \}$, but with no index 0. The example shows that a consequence relation completely determined by the notion of paraconsistently closed tableau Definition 14.3.1 is robust to unlimited ex falso quodlibet.

A positive point of the presented approach is also that we could sometimes infer a conclusion from a logically invalid formula, if a formula that is a conclusion follows from some part of it.

Example 14.3.2

Consider a set of premises $X = \{ p \wedge \lnot p \}$ and a possible conclusion p. We take a root $\{ (p \wedge \lnot p)^{1}, \lnot p^{0} \}$ and draw a tableau.

As we see it is a paraconsistently closed tableau by Definition 14.3.1. In any branch (there is of course only one branch) there is $t^{i,0}$-inconsistency, for some index i. Admittedly, we have a t-inconsistent set $\{ p^{1}, \lnot p^{0} \}$. The example shows that a consequence relation completely determined by the notion of paraconsistently closed tableau Definition 14.3.1 enables to infer parts of a contradictory formula.

Another positive point of the presented approach is that we can of course infer any classical tautology.

Example 14.3.3

Consider a set of premises $X = \emptyset$ and a possible conclusion $p\vee \lnot p$. We take a root $\{ \lnot ( p \vee \lnot p)^{0} \}$ and draw a tableau.

As we see it is a paraconsistently closed tableau by Definition 14.3.1. In any branch (there is of course only one branch) there is $t^{i,0}$-inconsistency, for some index i. Admittedly, we have a t-inconsistent set $\{ p^{0}, \lnot p^{0} \}$. The example shows that a consequence relation completely determined by the notion of paraconsistently closed tableau Definition 14.3.1 enables to infer parts of a contradictory formula.

However, we have some objections. First of all, we can accept that from $\{ p, \lnot p \}$ follows p and follows $\lnot p$, since some part of information in the set $\{ p, \lnot p \}$ must be true (either $\{ p \}$ or $\{ \lnot p \}$)—clearly, the inference also holds according to the Definition 14.3.1. But in the Example 14.3.2 we have an inference we do not accept, since a set $\{ p \wedge \lnot p \}$ cannot be true. One can say that sets $\{ p \wedge \lnot p \}$ and $\{ p, \lnot p \}$ are classically equivalent not because they are contradictory, but because in general sets $\{ A \wedge B \}$ and $\{ A, B \}$ are classically equivalent, for any formulas A, B. Our point of view is that the set $\{ p \wedge \lnot p \}$ is worthless. Contrary to the set $\{ p, \lnot p \}$ is not useless, if we do not know whether p or $\lnot p$, then we can suspend for a moment one of the premises and use the classical consequence relation to a noncontradictory set $\{ p \}$ or $\{ \lnot p \}$.

But the most striking fact and a fundamental weakness of that approach is pictured in the next example.

Example 14.3.4

Consider a set of premises $X=\{(p \wedge \lnot p)\vee q)\}$ and a possible conclusion q. We take a root $\{((p \wedge \lnot p)\vee q))^{1}, \lnot q^{0}\}$ and draw a tableau. The tableau is complete, since all possible rules of decomposition were used.

It is a classically closed tableau, but—according to the Definition 14.3.1—it is not a paraconsistently closed tableau, since on the left branch we do not have $t^{1, 0}$-inconsistency, and as a consequence the condition 2 of Definition 14.3.1 is not satisfied.

Since we cannot accept this situation, we propose a modification. This modification brings another additional benefit. Refusing inferences from inconsistent sets of premises, we can almost automatically define simple and intuitive semantics for the new tableaus. Obviously, one can say that a fact we refuse, for example, the inference from $\{ p \wedge \lnot p \}$ to p and simultaneously accept the inference from $\{ p, \lnot p \}$ to p is a cost we pay for natural semantics, but we also include such cases like the Example 14.3.4.

3.1 Paraconsistent Tableau Consequence Relation

Therefore we redefine the latter definition of paraconsistently closed tableau to capture some inferences we like, exclude some inferences we do not like, and at the same time have intuitive semantics.

Definition 14.3.2

Let $Y \in X(x)$, for some $X \subseteq \textsf {For}$, and let $B \in \textsf {For}$. A tableau T with a root $Y \cup \{ \lnot B^{0} \}$ is paraconsistently closed iff:

• 1. T is complete

• 2. for any branch b in T there are such indexes $i, j \in \bullet (Y \cup \{ \lnot B^{0}\})$ that $t^{i, j}$-inconsistent set of formulas belongs to b.

• 3. there is a branch b in T that for any pair of indexes $i, j \in \bullet (Y)$ no $t^{i, j}$-inconsistent set of formulas belongs to b.

Now, we explain the conditions in Definition 14.3.2 one by one. The first condition is identical to that in Definition 14.3.1. A novelty are the remaining two conditions.

In the second condition it is said that for some $i, j \in \bullet (Y \cup \{ \lnot B^{0}\})$ in all branches there must be $t^{i, j}$-inconsistent set of formulas. It means that at least on some branches a t-inconsistency may not contain index 0, so we capture cases like in the Example 14.3.4.

The third condition says that in a paraconsistently tableau at least on one branch there is no t-inconsistency generated on the ground of formulas from Y, which means that X is a consistent set of formulas itself. So although according to the former definition for $\{ p \wedge \lnot p, \lnot p \}$ we have a paraconsistently closed tableau (Example 14.3.3), according to the latter one we do not have, which is the most convincing.

Again we have some simple examples.

Example 14.3.5

We come back to Example 14.3.2. Consider a set of premises $X = \{ p \wedge \lnot p \}$ and a possible conclusion p. We take a root $\{ (p \wedge \lnot p)^{1}, \lnot p^{0} \}$ and draw a tableau.

As we see it is not a paraconsistently closed tableau according to Definition 14.3.2. On any branch (there is of course only one branch) there is $t^{i,0}$-inconsistency. Admittedly, we have a t-inconsistent set $\{ p^{1}, \lnot p^{0} \}$. But there is no branch on which for any pair of indexes $i, j \in \bullet (\{ (p \wedge \lnot p)^{1} \})$ no $t^{i, j}$-inconsistent set of formulas belongs to b (so the condition 3 is not satisfied), since on all branches we have $t^{1, 1}$-inconsistency—$\{ p^{1}, \lnot p^{1} \}$.

Example 14.3.6

Consider a set of premises $X = \{ p\}$ and a possible conclusion p. We take a root $\{ p^{1}, \lnot p^{0} \}$ and draw a tableau.

As we see it is a paraconsistently closed tableau according to Definition 14.3.2. On any branch (there is of course only one branch) there is $t^{i,0}$-inconsistency. Admittedly, we have a t-inconsistent set $\{ p^{1}, \lnot p^{0} \}$. And there is a branch on which for any pair of indexes $i, j \in \{ p^{1} \}$ no $t^{i, j}$-inconsistent set of formulas belongs to b (so the condition 3 is satisfied), since on the branch we do not have $t^{1, 1}$-inconsistency.

At the end we present an example, where the mentioned liberalization of rules really works.

Example 14.3.7

Consider a set of premises $X = \{ r, p \wedge \lnot p \}$ and a possible conclusion r. We take a root $\{r^{1}, (p \wedge \lnot p)^{2}, \lnot r^{0} \}$ and draw a tableau.

Classically, this is a closed and complete tableau, if we assume we cannot apply tableau rules to inconsistent sets of premisses. There is only one branch and we have $t^{1, 0}$-inconsistency on it. Moreover, on some branches there is no $t^{i, j}$-inconsistency for $i, j \in \bullet (\{r^{1}, (p \wedge \lnot p)^{2})$. So there it would seem like a paraconsistently closed tableau. But it is not true, we can still make the branch longer and obtain some interesting formulas as below:

As we see now it is not a paraconsistently closed tableau according to Definition 14.3.2, because on all branches we have $t^{i, j}$-inconsistency for $i, j \in \bullet (\{r^{1}, (p \wedge \lnot p)^{2})$ and the last condition of definition is not satisfied. The tableau we get, because we can apply tableau rules, even if we have t-inconsistencies. We should not worry about this, since as we have already said we shall define a paraconsistent tableau consequence relation in such a way that a formula A is a consequence of X iff for some finite subset Y of X we have a paraconsistently closed tableau. So although the example is not an example of paraconsistently closed tableau, from the premisses it follows the conclusion, because we can built a paraconsistently tableau with $\{r\}$—a finite subset of X.

Now, we have a conclusion that expresses a connection between usual, classical tableaus, and paraconsistent tableaus.

Corollary 14.3.3

Let $Y \in X(x)$, for some set of formulas X, and let B be a formula. A tableau $T_{1}$ with the root $Y \cup \{ \lnot B^{0} \}$ is paraconsistently closed iff

• 1. there is a complete and open tableau $T_{2}$ with a root X

• 2. there is a closed tableau $T_{3}$ with a root $X \cup \{ \lnot B\}$.

Proof

The proof is by conditions 2 and 3 of the Definition 14.3.2.$\Box$

It means that we could replace Definition 14.3.2 by the statements 1 and 2 of the Corollary 14.3.3 as definitional conditions. Theoretically, it would be simpler. However, practically it is difficult to choose a suitable subset of premises that generates complete and open tableau, but with a negated conclusion generates a closed tableau. In the presented approach, we consider all possible decompositions, tracking superscripts, and kinds of t-inconsistencies that appear, and finally we can choose a suitable and consistent set of premisses (if any exists) which on interaction with a negated conclusion generates some t-inconsistencies.

Now, we can define a paraconsistent tableau consequence relation $\vartriangleright '$.

Definition 14.3.4

Let $X \subseteq \textsf {For}$ and $A \in \textsf {For}$. $X \vartriangleright ' A$ iff there exist a finite subset Y of X and a paraconsistently closed tableau with a root $Z \cup \{\lnot A^{0} \}$, for some $Z \in Y(y)$.

One example of how to pass from a unsuccessful tableau to a paraconsistently closed one we give here.

Example 14.3.8

We consider a set of premisses $X = \{\lnot p\vee q, r\wedge \lnot r, \lnot q,\}$ and a conclusion $\lnot p$. The question is whether $X \vartriangleright ' \lnot p$?

The set X is a finite subset of X and the tableau with a root $\{(\lnot p\vee q)^{1}, (r\wedge \lnot r)^{2}, \lnot q^{3}, \lnot \lnot p^{0}\}$ is complete—all possible rules of decomposition were used.

The condition 1 and 2 of the Definition 14.3.2 are satisfied—the tableau is complete and on all branches we have $t^{i, j}$-inconsistency, for some $i, j \in \{ 1, 2, 3, 0 \}$. Unfortunately, the condition 3 of the Definition 14.3.2 is not satisfied, since on all branches we have $t^{i, j}$-inconsistency, for some $i, j \in \{ 1, 2, 3 \}$.

Hence, it is not an example of a paraconsistently closed tableau, but it does not mean that it is not $X \vartriangleright ' \lnot p$. When we take into account a subset of X, the subset $Y = \{\lnot p\vee q, \lnot q,\}$ we see that the conditions are fully satisfied. We can look at the latter tableau or draw another one.

The condition 1 and 2 of the Definition 14.3.2 are satisfied. Moreover at least on one branch—the left one—no $t^{i, j}$-inconsistency we have, for any $i, j \in \{ 1, 3\}$. Hence, it is an example of a closed tableau and simultaneously a paraconsistently closed tableau, and according to Definition 14.3.4 we have: $\{\lnot p\vee q, r\wedge \lnot r, \lnot q,\}\vartriangleright ' \lnot p$.

A demanded fact is that the paraconsistent, tableau consequence relation $\vartriangleright '$ is a proper subrelation of a classical tableau consequence relation $\vartriangleright$.

Corollary 14.3.5

$\vartriangleright ' \subset \vartriangleright$.

Proof

Let $X \vartriangleright ' A$, for some $X \subseteq \textsf {For}$ and $A \in \textsf {For}$. Then by Definition 14.3.4, there exist a finite subset Y of X and a paraconsistently closed tableau with a root $Z \cup \{\lnot A^{0} \}$, for some $Z \in Y(y)$.

By Corollary 14.3.3 there exist a finite subset Y of X and a closed tableau with a root $Y \cup \{\lnot A \}$. So, according to the Definition 14.2.2, $X \vartriangleright A$, and $\vartriangleright ' \subseteq \vartriangleright$.

On the other hand, we have an example of a closed tableau (Example 14.3.1), that is not paraconsistently closed. Hence, by Definitions 14.2.2 and 14.3.4, we get $\vartriangleright \not \subseteq \vartriangleright '$.$\Box$

Having the relation $\vartriangleright '$, we straightforwardly determine a paraconsistent tableau system $\langle \textsf {For}, \vartriangleright ' \rangle$ of a sublogic of Propositional Logic.

4 Semantics

As quick as there appears a question about semantics for $\langle \textsf {For}, \vartriangleright ' \rangle$, we get a natural answer. A natural and commonsense approach to the problem of paraconsistency in Boolean language is to define a paraconsistent semantic relation of consequence by a set of valuations ${{\mathbf {\mathsf{{V}}}}}$ as follows:

Definition 14.4.1

For all $X \subseteq \textsf {For}$ and $A \in \textsf {For}$, $X \models ' A$ iff there is such $Y \subseteq X$ that Y is a consistent set of formulas and $Y \models A$.

Surely, the relation $\models '$ is identical to our relation $\vartriangleright '$.

Theorem 14.4.2

$\models ' \,= \,\vartriangleright '$.

Proof

We take any $X \subseteq \textsf {For}$ and $A \in \textsf {For}$.

First, we assume that $X \models ' A$. Then, by Definition 14.4.1, there exists such $Y \subseteq X$ that Y is a consistent set of formulas, $Y \models A$ and Y is finite—by compactness of $\models$. By Fact 14.2.3 we have $Y \vartriangleright A$, so there is a closed tableau with a root $Y \cup \{\lnot A\}$. But because Y is a consistent set, so there is a complete and open tableau with a root Y. As a consequence, by Corollary 14.3.3, a tableau with a root $Z \cup \{\lnot A ^{0} \}$, for some $Z \in Y(y)$, is paraconsistently closed. Hence, by Definition 14.3.4, $X \vartriangleright ' A$.

Second, we assume that $X \vartriangleright ' A$. By Definition 14.3.4 there exist a finite subset Y of X and a paraconsistently closed tableau with a root $Z \cup \{\lnot A^{0} \}$, for some $Z \in Y(y)$. By Corollary 14.3.3 Y is consistent, since there is a complete and open tableau with a root Y, and $Y \vartriangleright ' A$. Hence, $Y \vartriangleright A$, by Corollary 14.3.5, and $Y \models A$, by Fact 14.2.3. As a consequence, since $Y \subseteq X$, Y is consistent and $Y \models A$, $X \models ' A$.$\Box$

By Theorem 14.4.2 and Corollary 14.3.5 we have some final conclusion:

Corollary 14.4.3

$\vartriangleright '\, =\, \vartriangleright \!\!\cap \, \{\langle X, A \rangle : \langle X, A \rangle \subseteq 2^{\textsf {For}} \times \textsf {For}, \exists _{Y} \subseteq X$, Y is consistent and $Y \models A\}$.

5 Further Applications

The presented mechanism can be used to other tableau systems/logics. Through a formal theory of tableau systems [2], we should aim at a general theorem:

if $\models = \,\vartriangleright$, then $\models ' = \,\vartriangleright '$

where $\models$ and $\vartriangleright$ are semantical and tableau consequence relations of a given logic, while $\models '$ and $\vartriangleright '$ are their paraconsistent tableau counterparts.