Paraconsistency, resolution and relevance

TL;DR

This paper explores a novel logical framework using digraphs and semikernels to handle inconsistent theories, providing sound and complete resolution-based reasoning that avoids classical fallacies and Ex Falso.

Contribution

It introduces a subset of well-behaved semikernels for nontrivial models of inconsistent theories and adapts classical resolution for this semantics with specific weakenings.

Findings

Semikernels yield models for inconsistent theories.

Resolution with weakening is sound and complete for the new semantics.

Reasoning without weakening avoids relevance fallacies.

Abstract

Digraphs provide an alternative syntax for propositional logic, with digraph kernels corresponding to classical models. Semikernels generalize kernels and we identify a subset of well-behaved semikernels that provides nontrivial models for inconsistent theories, specializing to the classical semantics for the consistent ones. Direct (instead of refutational) reasoning with classical resolution is sound and complete for this semantics, when augmented with a specific weakening which, in particular, excludes Ex Falso. Dropping all forms of weakening yields reasoning which also avoids typical fallacies of relevance.

Equations

$$x\leftrightarrow \underset{i\in [n_x]}{\bigwedge }\neg y_i,\text{vspace}\ast -.5ex$$

$$\begin{array}[]{l@{\hspace*{1.5em}}l@{\ \iff\ }l}\hfil\hskip 15.00002pt&a^{\prime}\hfil\ \leftrightarrow&\neg a\\ \mbox{(a) This statemenet is not false.}\hfil\hskip 15.00002pt&a\hfil\ \leftrightarrow&\neg a^{\prime}\\ \mbox{(b) The previous and the next statement are false.}\hfil\hskip 15.00002pt&b\hfil\ \leftrightarrow&\neg a\land\neg c\\ \mbox{(c) The next statement is false.}\hfil\hskip 15.00002pt&c\hfil\ \leftrightarrow&\neg d\\ \mbox{(d) The next statement is false.}\hfil\hskip 15.00002pt&d\hfil\ \leftrightarrow&\neg e\\ \mbox{(e) Statement (c) is false.}\hfil\hskip 15.00002pt&e\hfil\ \leftrightarrow&\neg c\end{array}\vspace*{-.5ex}$$

$${\mathbf{D}}:\raisebox{3.01385pt}{\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 6.41293pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern 0.0pt\offinterlineskip\halign{\entry@#!@&&\entry@@#!@\cr&&&&&\crcr}}}\ignorespaces{\hbox{\kern-6.41293pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{a^{\prime}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 16.37157pt\raise 2.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 16.37157pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{a\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 6.41295pt\raise-2.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 37.61609pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{b\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 27.65746pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 57.86638pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 57.86638pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{c\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 78.15256pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 78.15256pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{d\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 99.31606pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 99.31606pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{e.\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{}{}{{}{}{}{}{}{}{}}{}\ignorespaces\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{{}{}{{}}{{}{}{}}{}}}}\ignorespaces{}\ignorespaces{}{}{}{{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}}{\hbox{\kern 68.19556pt\raise 2.53654pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{{}{}{}{{}}{{}{}{}\lx@xy@spline@}{}}}}\ignorespaces{}\ignorespaces\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{{}{}{{}}{{}{}{}}{}}}}\ignorespaces{}\ignorespaces}}}}\ignorespaces}\vspace*{-.5ex}$$

$$\begin{array}[]{rrcl}(a)&x\in\alpha^{\bf 1}&\Leftrightarrow&\forall y\in A_{\scriptscriptstyle{G}}(x):y\in\alpha^{\bf 0}\\ (b)&x\in\alpha^{\bf 0}&\Leftrightarrow&\exists y\in A_{\scriptscriptstyle{G}}(x):y\in\alpha^{\bf 1}.\end{array}\vspace*{-.5ex}$$

$$CMod(\Gamma )=\{⟨{\alpha }^1,{\alpha }^0⟩\in \mathcal{P}(G)\times \mathcal{P}(G)\mid {\alpha }^1\in Ker(G),{\alpha }^0=A_G^{-}({\alpha }^1)\}.\text{vspace}\ast -.5ex$$

$$A_G(S)\text{accentset}(a)\subseteq A_G^{-}(S)\text{accentset}(b)\subseteq G\setminus S.\text{vspace}\ast -.5ex$$

$$\begin{array}[]{rrcl@{\hspace*{2em}}l}(a)&x\in\alpha^{\bf 1}&\Rightarrow&\forall y\in A_{\scriptscriptstyle{G}}(x):y\in\alpha^{\bf 0}\hfil\hskip 20.00003pt&A_{\scriptscriptstyle{G}}(\alpha^{\bf 1})\subseteq\alpha^{\bf 0}\\ (b)&x\in\alpha^{\bf 0}&\Leftrightarrow&\exists y\in A_{\scriptscriptstyle{G}}(x):y\in\alpha^{\bf 1}\hfil\hskip 20.00003pt&\alpha^{\bf 0}=A^{-}_{\scriptscriptstyle{G}}(\alpha^{\bf 1})\\ (c)&x\in\alpha^{\bot}&\Leftrightarrow&x\in G\setminus(\alpha^{\bf 1}\cup\alpha^{\bf 0})\hfil\hskip 20.00003pt&\alpha^{\bot}=G\setminus(\alpha^{\bf 1}\cup\alpha^{\bf 0}).\end{array}\vspace*{-.5ex}$$

$$S\in SK(G):A_G^{-}(A_G^{-}[S])\subseteq A_G^{-}[S].\text{vspace}\ast -.5ex$$

$$\forall R\subseteq G:R\mathrm{satsfies}(\text{ref}M2)\Rightarrow {\mathrm{A}}_{\mathrm{G}}^{-}[\mathrm{S}]\not\subset {\mathrm{A}}_{\mathrm{G}}^{-}[\mathrm{R}].\text{vspace}\ast -.5ex$$

$$\begin{array}[]{r@{\hspace*{-.01cm}}l}Mod(G)=&\{S\in SK(G)\mid A^{-}_{\scriptscriptstyle{G}}(A^{-}_{\scriptscriptstyle{G}}[S])\subseteq A^{-}_{\scriptscriptstyle{G}}[S]\ \land\ \forall R\subseteq G:\\[2.15277pt] &\ R\in SK(G)\!\land A^{-}_{\scriptscriptstyle{G}}(A^{-}_{\scriptscriptstyle{G}}[R])\subseteq\!A^{-}_{\scriptscriptstyle{G}}[R]\mathrel{\Rightarrow}A^{-}_{\scriptscriptstyle{G}}[S]\not\subset A^{-}_{\scriptscriptstyle{G}}[R]\}\end{array}\vspace*{-.5ex}$$

$$⟨{\alpha }^1,{\alpha }^0,{\alpha }^{\perp }⟩\models A\overline{B}\iff A\cap {\alpha }^1\ne \varnothing \vee B\cap {\alpha }^0\ne \varnothing \vee (AB\subseteq {\alpha }^{\perp }\ne \varnothing ).\text{vspace}\ast -.5ex$$

$$\begin{array}[]{rrcl@{\hspace*{2em}}l}(a)&x\in\alpha^{\bf 1}&\Rightarrow&\forall y\in A_{\scriptscriptstyle{G}}(x):y\in\alpha^{\bf 0}\hfil\hskip 20.00003pt&A_{\scriptscriptstyle{G}}(\alpha^{\bf 1})\subseteq\alpha^{\bf 0}\\ (b)&x\in\alpha^{\bf 0}&\Leftrightarrow&\exists y\in A_{\scriptscriptstyle{G}}(x):y\in\alpha^{\bf 1}\hfil\hskip 20.00003pt&\alpha^{\bf 0}=A^{-}_{\scriptscriptstyle{G}}(\alpha^{\bf 1})\\ (c)&x\in\alpha^{\bot}&\Leftrightarrow&\forall y\in A_{\scriptscriptstyle{G}}(x):y\in\alpha^{\bot}\hfil\hskip 20.00003pt&\alpha^{\bot}=A_{\scriptscriptstyle{G}}[\alpha^{\bot}]\end{array}\vspace*{-.5ex}$$

$$\begin{array}[]{ll}(i)&A_{\scriptscriptstyle{G}}(\alpha^{\bot})\subseteq\alpha^{\bot}\\ (ii)&A^{-}_{\scriptscriptstyle{G}}(\alpha^{\bf 1}\cup\alpha^{\bf 0})\subseteq\alpha^{\bf 1}\cup\alpha^{\bf 0}\end{array}\vspace*{-.5ex}$$

$$\alpha \in mpSK(G)\iff \alpha \in pSK(G)\wedge \forall \beta \in pSK(G):{\alpha }^0\cup {\alpha }^1\not\subset {\beta }^0\cup {\beta }^1.\text{vspace}\ast -.5ex$$

$$\begin{array}[]{lcl}\Delta&=&\{aa^{\prime},\overline{aa}^{\prime},bac,\overline{ba},\overline{bc},cd,\overline{cd},de,\overline{de},ec,\overline{ec}\}\\ {\mathbf{D}}^{\bot}&=&\{c,d,e\}\\ {\mathbf{D}}^{ok}&=&\{a^{\prime},a,b\}\hfill\mbox{-- or the induced subgraph }\raisebox{3.01385pt}{\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 6.41293pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern 0.0pt\offinterlineskip\halign{\entry@#!@&&\entry@@#!@\cr&&\crcr}}}\ignorespaces{\hbox{\kern-6.41293pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{a^{\prime}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 16.37157pt\raise 2.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 16.37157pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{a\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 6.41295pt\raise-2.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 37.61609pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{b\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 27.65746pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces}}}}\ignorespaces}\\ \Delta^{ok}&=&\{aa^{\prime},\overline{aa}^{\prime},ba,\overline{ba},\overline{b}\}\\ brd({\mathbf{D}}^{ok})&=&\{b\}\\ \mbox{$\mathcal{C}$}({\mathbf{D}}^{ok})&=&\{aa^{\prime},\overline{aa}^{\prime},ba,\overline{ba}\}\mbox{\ -- clausal theory of the induced subgraph ${\mathbf{D}}^{ok}$}\end{array}$$

$$CMod({\Gamma }^{ok})=\{L\in Ker(G^{ok})\mid brd(G^{ok})\subseteq A_G^{-}(L)\}.\text{vspace}\ast -.5ex$$

$$\forall \alpha \in Mod(G):{\alpha }^{\perp }=G^{\perp }.\text{vspace}\ast -.5ex$$

$$(aW)\ \mbox{$\displaystyle{{\Gamma\vdash_{\!\!\!\tiny{}}B}\over{\Gamma\vdash_{\!\!\!\tiny{}}B\cup C}}$}B\not\subseteq\ddot{G}^{\bot}\hskip 10.00002pt(bW)\ \mbox{$\displaystyle{{\Gamma\vdash_{\!\!\!\tiny{}}\bot(a)\ \ \forall a\in A\not=\emptyset}\over{\Gamma\vdash_{\!\!\!\tiny{}}A}}$}\hskip 20.00003pt(cW)\ \mbox{$\displaystyle{{\Gamma\vdash_{\!\!\!\tiny{}}B}\over{\Gamma\vdash_{\!\!\!\tiny{}}B\cup C}}$}$$

$$(i)\neg a\vee a\vee \neg b.$$

Full text

1 Introduction

Numerous approaches to paraconsistency seem to agree on one thing: modifications of the classical logic, made to avoid explosion in the face of inconsistency, should be as limited as possible. We provide a paraconsistent semantics and reasoning satisfying this objective in an unusually strong sense: models and consequences of consistent theories are exactly their classical models and consequences, while reasoning applies only classical resolution. Following [4, 3], we give an equivalent formulation of propositional syntax as digraphs and of classical semantics as digraph kernels, which are generalized to semikernels. Semikernels underlie a uniform, general concept of a model, which gives classical models for consistent theories as a special case. For each theory, this general concept yields a unique set of atoms involved into inconsistency, which is empty when the theory is consistent.

The new semantics is the main contribution of the paper. Its significance is supported further by some informal justification as well as the fact that classical resolution provides sound and complete reasoning. Paraconsistency of direct (instead of refutational) resolution was applied in [10] to infinitary logic. However, that work lacked the semantic counterpart which is now provided. Direct resolution, applied here to finitary (usual) propositional logic, deviates from refutational resolution primarily by the exclusion of Ex Falso. The graph syntax we use, expressed in the language of clauses, makes Ex Falso a special case of weakening. An appropriate adjustment of weakening prevents then explosion from a contradiction, allowing for its unrestricted applicability when the theory is consistent.

Section 2 presents the background from [3, 10], explaining the applicability of digraphs as propositional syntax, their kernels as classical models, and semikernels as a generalization of kernels. Section 3 presents the main contribution: a semantics defined in terms of well-behaved semikernels, assigning a nonempty set of models to every theory and specializing to the classical semantics for consistent theories. The main theorem 3.10 shows that every inconsistent theory has a unique set of bad atoms, contributing to inconsistency. The consequence relation also specializes to the classical consequence for consistent theories. Unlike most formalisms, but in agreement with the natural tendency of informal discourse, it disregards inconsistent parts of statements whenever it is possible to extract from them also meaningful elements, to which truth-values can be consistently assigned. Section 4 shows soundness and completeness of resolution with appropriate weakening rules. Section 5 identifies elements of relevance reasoning and their semantics, arising when resolution is used without any form of weakening.

2 Digraphs as propositional syntax

A propositional formula is in graph normal form, GNF, when it has the form

[TABLE]

where all $x,y_{i}$ are atoms (propositional variables), $n_{x}\in\omega$ and $[n]=\{1,...,n\}$. When $n_{x}=0$, the corresponding formula is $x$. A theory is in GNF if all formulae are in GNF, and every atom of the theory occurs exactly once unnegated, i.e., on the left of $\leftrightarrow$.111The formula $a\leftrightarrow\neg b$ is in GNF but the theory $\{a\leftrightarrow\neg b\}$ is not, due to the loose $b$. Such cases can be treated as abbreviations, here, with a fresh atom $b^{\prime}$ and two additional formulae $b\leftrightarrow\neg b^{\prime}$ and $b^{\prime}\leftrightarrow\neg b$. As an example we will use the formalization $\Delta$, to the right, of the discourse to the left. The statement (a) requires introduction of a fresh atom $a^{\prime}$, to conform to GNF:

[TABLE]

GNF is indeed a normal form: every theory in (infinitary) propositional logic has an equisatisfiable one in GNF, [3] (new variables are typically needed to obtain GNF, as $a^{\prime}$ above). The classical semantics is defined in the usual way.

GNF allows a natural reading of its equivalences as propositional instances of the T-schema, expressing that the atom $x$ is true if and only if what it says, $\bigwedge_{i\in[n_{x}]}\neg y_{i}$, is true. Taken in this light, a theory in GNF represents a collection of T-schemata for the actual statements with possible, also indirect, self-references. We therefore call a theory in GNF a discourse and define paradox as an inconsistent discourse. Plausibility of this definition, implicit in [4], was argued and exemplified in [6, 10] and is witnessed by the increasing popularity of the corresponding graph representation in the analysis of paradoxes, [2, 4, 6, 7, 9, 10].222GNF finds also another application in argumentation theory in its AI-variant following [5]. In that context, our notion of the (maximal) consistent subdiscourse amounts to a new semantics based on admissible sets, whereby the acceptable extensions are the stable sets of the maximally consistent subdiscourse of the original digraph (argumentation framework).

Theories in GNF and graphs are namely easily transformed into each other. A graph (meaning here “directed graph”, unless qualified otherwise) is a pair $G=\langle G,A_{\scriptscriptstyle{G}}\rangle$ with $A_{\scriptscriptstyle{G}}\subseteq G\times G$. (Overloading the notation $G$, for a graph and its set of vertices, should not cause any confusion.) We denote $A_{\scriptscriptstyle{G}}(x)=\{y\in G\mid A_{\scriptscriptstyle{G}}(x,y)\}$, $A^{-}_{\scriptscriptstyle{G}}(x)=\{y\in G\mid x\in A_{\scriptscriptstyle{G}}(y)\}$, and extend pointwise such notation to sets, i.e., $A^{-}_{\scriptscriptstyle{G}}(X)=\bigcup_{x\in X}A^{-}_{\scriptscriptstyle{G}}(x)$, etc. $A^{*}_{\scriptscriptstyle{G}}/A^{{\underline{*}}}_{\scriptscriptstyle{G}}$ denote reflexive, transitive closure of $A_{\scriptscriptstyle{G}}/A^{-}_{\scriptscriptstyle{G}}$.

A GNF theory $\Gamma$ gives a graph $G$ with all atoms as vertices and edges from every $x$ on the left side of its GNF formula to each $y_{i}$ on its righ side, i.e., $A_{\scriptscriptstyle{G}}=\{\langle x,y_{i}\rangle\mid x\in G,i\in[n_{x}]\}$. The graph for $\Delta$ from (2.2) is:

[TABLE]

Conversely, the theory of a graph $\langle G,A\rangle$ is \mbox{\mathcal{T}}(G)=\{x\leftrightarrow\bigwedge_{y\in A(x)}\neg y\mid x\in G\}. (When $x$ is a sink, $A(x)=\emptyset$, this becomes $x\leftrightarrow\top$, i.e., $x$ is included in \mbox{\mathcal{T}}(G).) The two are inverses, so we ignore usually the distinction between theories (in GNF) and graphs, viewing them as alternative presentations.

The equivalence of graphs and GNF theories is not only a syntactic transformation. The classical models of GNF theories can be defined equivalently as kernels of the corresponding graphs, [4, 3]. A kernel of a graph $G$ is a subset $K\subseteq G$ which is independent (no edges between vertices in $K$) and absorbing its complement (every $y\in G\setminus K$ has an edge to some $x\in K$), i.e., such that $A^{-}_{\scriptscriptstyle{G}}(K)=G\setminus K$. $Ker(G)$ denotes kernels of $G$.

Kernel of a graph $G$ can be defined equivalently as a 2-partition $\alpha=\langle\alpha^{\bf 1},\alpha^{\bf 0}\rangle$ of the vertices $G$, such that $\forall x\in G:$

[TABLE]

A 2-partition $\alpha$ satisfies (2.4) iff $\alpha^{\bf 1}\in Ker(G)$. On the other hand, satisfaction of (2.4) at every $x\in G$ is equivalent to the satisfaction of the respective GNF theory \Gamma=\mbox{\mathcal{T}}(G). So, for corresponding graph $G$ and theory $\Gamma$, we identify also kernels of the former and models of the latter. In short, graphs provide syntax for propositional logic, while their kernels are its classical semantics.

$CMod(\Gamma)$ denotes classical models of $\Gamma$, each represented as a partition $\alpha=\langle\alpha^{\bf 1},\alpha^{\bf 0}\rangle$ of $G$, where $\alpha^{\bf 1}/\alpha^{\bf 0}$ are atoms assigned ${\bf 1}/{\bf 0}$. The classical satisfaction, $\models_{c}$, is obtained by the standard extension to complex formulae of the basis for atoms $a\in G:\langle\alpha^{\bf 1},\alpha^{\bf 0}\rangle\models_{c}a$ iff $a\in\alpha^{\bf 1}$ and $\langle\alpha^{\bf 1},\alpha^{\bf 0}\rangle\models_{c}\neg a$ iff $a\in\alpha^{\bf 0}$. $C$ is a classical consequence of $\Gamma$, $\Gamma\models_{c}C$ if $\forall\alpha\in CMod(\Gamma):\alpha\models_{c}C$.

The exact correspondence between kernels of $G$ and models of the respective theory $\Gamma$ is as follows: 333Sufficient conditions for absence of paradox, expressed in terms of the properties of the graph representing the discourse, can be thus imported from kernel theory, as illustrated in [6]. They confirm that the liar, as a minimal odd cycle, is the paradigmatic pattern of a finitary paradox: a finitely branching graph without odd cycles has a kernel. For the infinitary case, it is natural to conjecture that one also has to exclude some form of a Yablo pattern. Such a generalization is proposed in [11] and, in an equivalent formulation, in [2]. The proof of its special case in [11] demonstrates the difficulty of the problem.

[TABLE]

Conditions (a) and (b) of (2.4) are equivalent for total $\alpha$ (with $\alpha^{\bf 0}=G\setminus\alpha^{\bf 1}$), but we will also consider more general structures, arising from the notion of a semikernel, [8], namely, a subset $S\subseteq G$ satisfying:

[TABLE]

By (a), each $x\in G$ with an edge from $S$ has an edge back to $S$ and, by (b), $S$ is independent. $SK(G)$ denotes all semikernels of $G$. A semikernel $S$ is a kernel of the induced subgraph $A^{-}_{\scriptscriptstyle{G}}[S]=A^{-}_{\scriptscriptstyle{G}}(S)\cup S$. (An induced subgraph, or a subgraph induced by ${H}\subseteq G$ is ${H}=\langle{H},A_{\scriptscriptstyle{\scriptscriptstyle{G}}}\cap({H}\times{H})\rangle$.)

Example 2.7

The graph ${\mathbf{D}}$ from (2.3) possess no kernel, as can be seen trying to assign values at $\{c,d,e\}$ conforming to (2.4). Its induced subgraph $\{c,d,e\}$ does not even possess a semikernel, but the whole graph ${\mathbf{D}}$ possesses two, namely, $\alpha^{\bf 1}=\{a\}$ and $\beta^{\bf 1}=\{a^{\prime}\}$.

A semikernel can be defined equivalently as a 3-partition $\alpha=\langle\alpha^{\bf 1},\alpha^{\bf 0},\alpha^{\bot}\rangle$ of $G$ such that $\forall x\in G:$

[TABLE]

A 3-partition $\alpha$ satisfies (2.8) iff $\alpha^{\bf 1}$ is a semikernel. $\alpha^{\bf 1}$ is a kernel iff $\alpha^{\bf 1}$ is a semikernel and $\alpha^{\bot}=\emptyset$.

3 Semantics of inconsistency

Models of an arbitrary theory, i.e., of a graph possibly without any kernel, are required to satisfy three conditions which we now briefly motivate.

In the graph ${\mathbf{D}}$ from (2.3), the subgraph induced by $\{c,d,e\}$ has no semikernel, but the subgraph induced by $\{a^{\prime},a,b\}$ – the meaningful subdiscourse – has two kernels: $\alpha^{\bf 1}=\{a\}$ and $\beta^{\bf 1}=\{a^{\prime},b\}$. The latter does not seem adequate as a model, because it should function in the context of the whole original theory, and not only after removal of its inconsistent part. In the context of the whole ${\mathbf{D}}$, $b$ negates not only $a$ but also $c$, so to conform to (2.4), or even just (2.8), $b\in\beta^{\bf 1}$ would require $c\in\beta^{\bf 0}$. Choosing $\alpha^{\bf 1}$ instead, $b\in\alpha^{\bf 0}$ complies with (2.8) since $a\in A_{\scriptscriptstyle{{\mathbf{D}}}}(b)\cap\alpha^{\bf 1}$.

This suggests semikernels as a semantic basis in the presence of inconsistency: $\alpha^{\bf 1}\in SK({\mathbf{D}})$, while $\beta^{\bf 1}\not\in SK({\mathbf{D}})$. A semikernel $\alpha^{\bf 1}$ makes all $x\in\alpha^{\bf 1}$ fully justfied, in the sense that $A_{\scriptscriptstyle{G}}(x)\subseteq\alpha^{\bf 0}$. This excludes $\beta^{\bf 1}$ from possible models. For $x\in\alpha^{\bf 0}$, on the other hand, it suffices that $A_{\scriptscriptstyle{G}}(x)\cap\alpha^{\bf 1}\not=\emptyset$, allowing other out-neighbours of $x$ to be arbitrary – possibly paradoxical. Such paradoxical elements form the third part $\alpha^{\bot}$ of the model.

There are, however, too many semikernels. In the graph ${\mathbf{D}}$, each among $\{a\}$, $\{a^{\prime}\}$ and $\emptyset$ (giving $\alpha^{\bf 1}=\alpha^{\bf 0}=\emptyset$ and $\alpha^{\bot}={\mathbf{D}}$) is a semikernel. Such a semantics is too liberal and we have to choose semikernels more carefully.

To explain next restriction, it will be helpful to consider two simple examples. “This statement is false and the sun is not a star” is represented by $F_{1}$:      \textstyle{f\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{s.} Here, $f$ seems false, negating the true statement $s$. Indeed, $F_{1}$ has a unique kernel, $\alpha^{\bf 1}=\{s\}$, which yields $f\in\alpha^{\bf 0}=F_{1}\setminus\alpha^{\bf 1}$. Now, consider “This statement is false and the sun is a star” – represented by $F_{2}$:      \textstyle{f\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{y\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{s.} Now $f$ appears to be paradoxical, since $F_{2}$ is a contingent liar, ceasing to be paradoxical only if the sun is not a star, which it is. The only semikernel of $F_{2}$, $\alpha^{\bf 1}=\{s\}$, gives $\alpha^{\bf 0}=\{y\}$, but this leads to the irresolvability of the paradox “at” $f$. In short, $f$ is paradoxical because $s$ happens to be true. Hence, also $s$ is involved in the paradox at $f$, not as a standalone atom but as a member of the formula for $y$, which in turn features in the formula of the contingently paradoxical $f$.

The paradox “at” $f$ – “referring to” $s$ by denying $y$ – involves $s$ and $y$ as much as it involves self-reference. If we are not prepared to admit this, we should hardly regard $F_{1}$ as nonparadoxical, since the problematic self-reference at $f$ is exactly the same in both $F_{1}$ and $F_{2}$. If the truth of $s$ prevents paradox in $F_{1}$ then, in the same way, it contributes to it in $F_{2}$.

This is not to suggest that “the sun is a star” is paradoxical on its own, only that its token contributes to the paradoxical whole when combined with the contingent liar as in $F_{2}$. Consistency and paradox are genuinely holistic. Or put differently: the token of “the sun is a star” is unproblematic in $F_{1}$, but its token in $F_{2}$ becomes paradoxical by contributing to the appearance of the paradox: if there were no $s$, there would be no paradox. When trying to repair this paradox, removing the loop at $f$ is as good as removing $s$.

The absence of any single culprit among $\{f,y,s\}$ is just as it was with $\{c,d,e\}$ in (2.2). A nonobvious informal lesson could be: if an inconsistency, occurring “at” some $f$, depends on some $s$ (in the sense of $s\in A^{*}_{\scriptscriptstyle{G}}(f)$), then $s$ is “a part of” this inconsistency. Consequently, we should not rest satisfied with an arbitrary semikernel, like $\{s\}\in SK({F_{2}})$. Exactly the semikernel we choose (combined with other factors, like the loop at $f$) can be the reason for the inconsistency, which could be possibly prevented by another choice. A satisfactory semikernel $S$ should not contribute to any inconsistency occuring above it in the graph. Put precisely, a model is not only a semikernel but an $A^{-}_{\scriptscriptstyle{G}}$-closed semikernel, i.e.:

[TABLE]

This views all $\{f,y,s\}$ as inconsistent (contributing to the inconsistency) in $F_{2}$, making the empty semikernel the only interpretation. For ${\mathbf{D}}$ from (2.3), the semikernel $\{a^{\prime}\}$ is rejected, as it is not $A^{-}_{\scriptscriptstyle{G}}$-closed, leaving only $\{a\}$.

The above condition still admits the empty semikernel, even when there are nonempty ones. To avoid this we require $A^{-}_{\scriptscriptstyle{G}}[S]$ to be maximal:

[TABLE]

This condition can be seen as a minimization of inconsistencies, typical for preferential models, like LPm and many other examples. But here most of such minimization is done by the two earlier conditions; this one excludes only specific degenerate cases. We thus obtain the main definition: models of a graph $G$ (or its theory $\Gamma$) are $A^{-}_{\scriptscriptstyle{G}}$-closed, maximal semikernels:

[TABLE]

The consequence relation $\models$ generalizes $\models_{c}$ to 3-partitions $\alpha_{S}=\langle\alpha^{\bf 1}_{S},\alpha^{\bf 0}_{S},\alpha^{\bot}_{S}\rangle$ $=\langle S,A^{-}_{\scriptscriptstyle{G}}(S),G\setminus A^{-}_{\scriptscriptstyle{G}}[S]\rangle$, arising from all independent $S\subseteq G$, in particular, models of $G:\Gamma\models C$ if $\forall S\in Mod(G):\alpha_{S}\models C$. As formulae, we use clauses and let $A\overline{B}$ denote a clause with atoms $A$ and negated atoms $B$. Such a clause is satisfied by a 3-partition $\alpha$ according to the following rule:

[TABLE]

The third disjunct may appear less intuitive than the first two, but we comment it below. When $\alpha^{\bot}=\emptyset$, this reduces to the classical satisfaction and consequence with respect to $CMod(G)$, cf. (2.5). In the extreme case of a $\Gamma$ where all atoms are involved in inconsistency, there is only one model $\langle\emptyset,\emptyset,G\rangle$, arising from the empty semikernel, and satisfying every clause (over the atoms $G$). On the other hand, the empty theory has the empty graph, with only one, empty kernel, giving the only model $\langle\emptyset,\emptyset,\emptyset\rangle$, which does not satisfy any formula. This deviation from classical logic is only a question of preference, since for this special case we could define the models in the classical way. However, since our logic is a logic of consequences rather than of tautologies, it appears plausible that nothing follows from saying nothing.

According to (3.4), an $\alpha$ satisfies a clause $C$ either for some “healthy” reasons, when some of its literals are true, or because the clause is “completely nonsensical”, with all atoms involved into inconsistency. In natural discourse, we tend to focus on its meaningful parts, simply ignoring occasional nonsense. A statement “The sun is a planet; or else this (part of this) statement is false.” may be judged nonsensical (as it would be in SK or LP, where ${\bf 0}\lor\bot=\bot$). But if we grant the interlocutor the benefit of doubt and are willing to ignore the partial nonsense, we can also say that it is false, since so is its meaningful part. When, however, unable to discern any sense whatsoever, like in the liar or in (c)-(d)-(e) from (2.2), we “accept” the claim as much as we “accept” its negation. Relation (3.4) can be read as such an acceptance which treats clauses containing healthy literals according to these literals, ignoring the nonsensical part. Faced with a complete nonsense, however, it becomes as confused as we are when, in the face of the liar, we find it equally (im)plausible to accept its “truth” and its “falsehood”. This does not imply any semantic dialetheism, since nonsensical atoms are excluded from the healthy considerations and relegated to $\alpha^{\bot}$. (They can be seen as gluts, since both the atom and its negation are provable, but also as gaps, being irrelevant for the value of clauses containing also healthy literals.) A significant point is that this acceptance relation is not used for defining the models, which are chosen using (3.3), but only for determining their consequences. As it happens, the members of $Mod(G)$ do satisfy the graph’s theory according to (3.4), but they need not be all 3-partitions doing this.

Typically, $Mod(G)$ contains nontrivial models also for inconsistent $\Gamma$. In fact, these are classical models of the appropriate subgraph. Given an $\alpha^{\bf 1}\in Mod(G)$, and projecting away the third component from its partition $\langle\alpha^{\bf 1},A^{-}_{\scriptscriptstyle{G}}(\alpha^{\bf 1}),G\setminus A^{-}_{\scriptscriptstyle{G}}[\alpha^{\bf 1}]\rangle$, leaves $\langle\alpha^{\bf 1},A^{-}_{\scriptscriptstyle{G}}(\alpha^{\bf 1})\rangle\in CMod(A^{-}_{\scriptscriptstyle{G}}[\alpha^{\bf 1}])$, i.e., $\alpha^{\bf 1}\in Ker(A^{-}_{\scriptscriptstyle{G}}[\alpha^{\bf 1}])$ – a classical model of the theory for the induced subgraph $A^{-}_{\scriptscriptstyle{G}}[\alpha^{\bf 1}]$. Interestingly, each two of such models $\alpha^{\bf 1},\beta^{\bf 1}\in Mod(G)$ classify the same vertices as inconsistent, assigning boolean values to the same subset of $G$, namely, $A^{-}_{\scriptscriptstyle{G}}[\alpha^{\bf 1}]=A^{-}_{\scriptscriptstyle{G}}[\beta^{\bf 1}]$.

Proving this will take the rest of this section and requires some preliminary observations. When $S\in SK(G)$, $\alpha_{S}=\langle S,A^{-}_{\scriptscriptstyle{G}}(S),G\setminus A^{-}_{\scriptscriptstyle{G}}[S]\rangle$ satisfies conditions (a) and (b) from (2.8), repeated below:

[TABLE]

Condition (c) in (2.8) was a mere definition of $\alpha^{\bot}=G\setminus(\alpha^{\bf 1}\cup\alpha^{\bf 0})$, while here it expresses that $S$ is $A^{-}_{\scriptscriptstyle{G}}$-closed, since its complement $\alpha^{\bot}$ is $A_{\scriptscriptstyle{G}}$-closed. Obviously, $A^{-}_{\scriptscriptstyle{G}}(A^{-}_{\scriptscriptstyle{G}}[S])\subseteq(A^{-}_{\scriptscriptstyle{G}}[S])$ implies $\alpha_{S}^{\bot}\supseteq A_{\scriptscriptstyle{G}}[\alpha_{S}^{\bot}]$. The opposite implication of (c) follows then from (a) and (b), while $\alpha_{S}^{\bot}\subseteq A_{\scriptscriptstyle{G}}[\alpha_{S}^{\bot}]$ holds by definition $A_{\scriptscriptstyle{G}}[X]=X\cup A_{\scriptscriptstyle{G}}(X)$. (Unlike in (a) and (b), the two formulations in (c) are not equivalent.) Hence for every $A^{-}_{\scriptscriptstyle{G}}$-closed $S\in SK(G)$, $\alpha_{S}$ satisfies (3.5), and $pSK(G)$ denotes all such 3-partitions.

Conversely, every 3-partition $\alpha\in pSK(G)$ satisfies (2.8), so that $\alpha^{\bf 1}\in SK(G)$. Such an $\alpha$ satisfies also the following closure property:

[TABLE]

Point (i) follows from condition (c) of (3.5) while point (ii) is equivalent to (i), since $\alpha^{\bot}=G\setminus(\alpha^{\bf 0}\cup\alpha^{\bf 1})$. When $\alpha^{\bf 1}\in SK(G)$, (ii) is the condition (3.1). Thus pSK partitions correspond exactly to $A^{-}_{\scriptscriptstyle{G}}$-closed semikernels, (3.1), so that $Mod(G)$ correspond exactly to maximal pSK partitions, namely:

[TABLE]

In addition, the following fact is used in the proof of the next, crucial lemma.

Fact 3.8

For every graph $G$,

If $T\subseteq S\in SK(G)$ then $(S\cap A^{*}_{\scriptscriptstyle{G}}(T))\in SK(G)$. 2. 2.

If $S\in SK(G)$, $T\in SK(G)$ and $A^{-}_{\scriptscriptstyle{G}}(S)\subseteq G\setminus T$, then $(S\cup T)\in SK(G)$.

Proof.

1. For any $x\in A_{\scriptscriptstyle{G}}(t)\subseteq A_{\scriptscriptstyle{G}}(T)\subseteq A_{\scriptscriptstyle{G}}(S)\subseteq A^{-}_{\scriptscriptstyle{G}}(S)$, and $s\in S$ with $x\in A^{-}_{\scriptscriptstyle{G}}(s)$, we have $s\in A^{*}_{\scriptscriptstyle{G}}(t)\subseteq A^{*}_{\scriptscriptstyle{G}}(T)$, i.e., $x\in A^{-}_{\scriptscriptstyle{G}}(S\cap A^{*}_{\scriptscriptstyle{G}}(T))$. This gives the first inclusion below, while the second one follows since $S\in SK(G)$:

$A_{\scriptscriptstyle{G}}(S\cap A^{*}_{\scriptscriptstyle{G}}(T))\subseteq A^{-}_{\scriptscriptstyle{G}}(S\cap A^{*}_{\scriptscriptstyle{G}}(T))\subseteq G\setminus S\subseteq G\setminus(S\cap A^{*}_{\scriptscriptstyle{G}}(T))$.

$A_{\scriptscriptstyle{G}}(S\cup T)\subseteq A_{\scriptscriptstyle{G}}(S)\cup A_{\scriptscriptstyle{G}}(T)\subseteq A^{-}_{\scriptscriptstyle{G}}(S)\cup A^{-}_{\scriptscriptstyle{G}}(T)=A^{-}_{\scriptscriptstyle{G}}(S\cup T)$. For the next inclusion, we note that $A^{-}_{\scriptscriptstyle{G}}(S)\subseteq G\setminus T$ implies here also the dual $A^{-}_{\scriptscriptstyle{G}}(T)\subseteq G\setminus S$, for if for some $t\in T,s\in S:t\in A_{\scriptscriptstyle{G}}(s)$, then $t\in A^{-}_{\scriptscriptstyle{G}}(S)$ since $S\in SK(G)$. Hence

$A^{-}_{\scriptscriptstyle{G}}(S)\cup A^{-}_{\scriptscriptstyle{G}}(T)\subseteq((G\setminus S)\cap(G\setminus T))\cup((G\setminus T)\cap(G\setminus S))=G\setminus(S\cup T)$.

Consequently, distinct $A^{-}_{\scriptscriptstyle{G}}$-closed semikernels, disagreeing on at least one paradoxical element, can be combined as in the proof of the following lemma.

Lemma 3.9

For all graphs $G:$

$\forall\alpha,\beta\in pSK(G)\ \exists\gamma\in pSK(G):\beta^{\bf 1}\cup\beta^{\bf 0}\not\subseteq\alpha^{\bf 1}\cup\alpha^{\bf 0}\mathrel{\Rightarrow}\alpha^{\bf 1}\cup\alpha^{\bf 0}\subset\gamma^{\bf 1}\cup\gamma^{\bf 0}$.

Proof. For arbitrary $\alpha,\beta\in pSK(G)$ with $\beta^{\bf 1}\cup\beta^{\bf 0}\not\subseteq\alpha^{\bf 1}\cup\alpha^{\bf 0}$, we have that $(\beta^{\bf 1}\cup\beta^{\bf 0})\cap\alpha^{\bot}\not=\emptyset$, so define $Q=\beta^{\bf 1}\cap\alpha^{\bot}$ and $R=\beta^{\bf 0}\cap\alpha^{\bot}$. We show that $S=\alpha^{\bf 1}\cup Q$, with $Q\not=\emptyset$, is an $A^{-}_{\scriptscriptstyle{G}}$-closed semikernel, i.e., the desired $\gamma^{\bf 1}$.

• (a)

$R\subseteq A_{\scriptscriptstyle{G}}(Q)$, by $\beta^{\bf 1}\in SK(G)$ and 3.6.(i) – hence also $Q\not=\emptyset$.

• (b)

$A^{*}_{\scriptscriptstyle{G}}(Q)\subseteq A^{*}_{\scriptscriptstyle{G}}(\alpha^{\bot})\subseteq\alpha^{\bot}$, by 3.6.(i).

• (c)

$Q$ is a semikernel, because $\beta^{\bf 1}\cap A^{*}_{\scriptscriptstyle{G}}(Q)\in SK(G)$ by Fact 3.8.(1), while $Q=\beta^{\bf 1}\cap A^{*}_{\scriptscriptstyle{G}}(Q)$ by (b): $\beta^{\bf 1}\cap\alpha^{\bot}\subseteq\beta^{\bf 1}\cap A^{*}_{\scriptscriptstyle{G}}(Q)\subseteq\beta^{\bf 1}\cap\alpha^{\bot}$.

• (d)

$A^{-}_{\scriptscriptstyle{G}}(Q)\subseteq G\setminus\alpha^{\bf 1}$, by $Q\subseteq\alpha^{\bot}$ and $\alpha^{\bf 1}\in SK(G)$ (so that $A^{-}_{\scriptscriptstyle{G}}(\alpha^{\bot})\cap\alpha^{\bf 1}=\emptyset$).

• (e)

$S\in SK(G)$, by Fact 3.8.(2) (applicable by (c)-(d) above).

• (f)

$S$ is $A^{-}_{\scriptscriptstyle{G}}$-closed, i.e., $A^{-}_{\scriptscriptstyle{G}}(A^{-}_{\scriptscriptstyle{G}}[S])\subseteq A^{-}_{\scriptscriptstyle{G}}[S]$. If $x\in S\subseteq A^{-}_{\scriptscriptstyle{G}}[S]$, then trivially $A^{-}_{\scriptscriptstyle{G}}(x)\subseteq A^{-}_{\scriptscriptstyle{G}}[S]$. If $x\in A^{-}_{\scriptscriptstyle{G}}(S)$, we have two cases.

• (i)

$x\in A^{-}_{\scriptscriptstyle{G}}(\alpha^{\bf 1})$. Since $\alpha$ is a pSK partition, (3.5): $A^{-}_{\scriptscriptstyle{G}}(x)\cap\alpha^{\bot}=\emptyset$. Since $G\setminus A^{-}_{\scriptscriptstyle{G}}[S]\subseteq\alpha^{\bot}:A^{-}_{\scriptscriptstyle{G}}(x)\subseteq A^{-}_{\scriptscriptstyle{G}}[S]$, as desired.

• (ii)

$x\in A^{-}_{\scriptscriptstyle{G}}(Q)$. $\alpha$ satisfies (3.5) and $\beta$ (2.8), so $A^{-}_{\scriptscriptstyle{G}}(Q)\subseteq\beta^{\bf 0}\cap(\alpha^{\bot}\cup\alpha^{\bf 0})$.

If $x\in\alpha^{\bf 0}$ then $A^{-}_{\scriptscriptstyle{G}}(x)\subseteq\alpha^{\bf 1}\cup\alpha^{\bf 0}$, because $\alpha$ satisfies (3.5). Hence $A^{-}_{\scriptscriptstyle{G}}(x)\subseteq A^{-}_{\scriptscriptstyle{G}}[S]$. If $x\in\beta^{\bf 0}\cap\alpha^{\bot}$ then $A^{-}_{\scriptscriptstyle{G}}(x)\subseteq(\beta^{\bf 1}\cup\beta^{\bf 0})\cap(\alpha^{\bot}\cup\alpha^{\bf 0})$. For any $y\in A^{-}_{\scriptscriptstyle{G}}(x)$:

$y\in(\beta^{\bf 1}\cup\beta^{\bf 0})\cap\alpha^{\bf 0}\subseteq A^{-}_{\scriptscriptstyle{G}}(\alpha^{\bf 1})\subseteq A^{-}_{\scriptscriptstyle{G}}(S)$, or

$y\in\beta^{\bf 1}\cap\alpha^{\bot}=Q\subseteq A^{-}_{\scriptscriptstyle{G}}[S]$, or

$y\in\beta^{\bf 0}\cap\alpha^{\bot}$ – then $\exists z\in\beta^{\bf 1}:y\in A^{-}_{\scriptscriptstyle{G}}(z)$, since $\beta^{\bf 1}\in SK(G)$. Since $z\in A_{\scriptscriptstyle{G}}(y)$, so $z\in\alpha^{\bot}$ by 3.6.(i), which means that $z\in Q$ so that $y\in A^{-}_{\scriptscriptstyle{G}}(Q)\subseteq A^{-}_{\scriptscriptstyle{G}}(S)$.

So, if $\alpha,\beta\in mpSK(G)$ while $\alpha^{\bot}\not=\beta^{\bot}$, then $\beta^{\bf 1}\cup\beta^{\bf 0}\not=\alpha^{\bf 1}\cup\alpha^{\bf 0}$, in particular, $\beta^{\bf 1}\cup\beta^{\bf 0}\not\subseteq\alpha^{\bf 1}\cup\alpha^{\bf 0}$ (since $\subset$ would contradict (3.7) for $\beta$). There is then $\gamma\in pSK(G):\alpha^{\bf 1}\cup\alpha^{\bf 0}\subset\gamma^{\bf 1}\cup\gamma^{\bf 0}$, contradicting (3.7) for $\alpha$. We thus obtain:

Theorem 3.10

For all graphs $G$ and all $S,R\in Mod(G):A^{-}_{\scriptscriptstyle{G}}[S]=A^{-}_{\scriptscriptstyle{G}}[R]$.

Since every $S\in SK(G)$ is a kernel of the subgraph induced by $A^{-}_{\scriptscriptstyle{G}}[S]$, our $Mod(G)$ satisfy quite a strog property: they are namely kernels of one specific subgraph of $G$, given by $A^{-}_{\scriptscriptstyle{G}}[S]$, for any maximal $A^{-}_{\scriptscriptstyle{G}}$-closed semikernel $S$. When the theory is consistent, $A^{-}_{\scriptscriptstyle{G}}[S]=G$ and $Mod(G)=Ker(G)$, i.e., the models are exactly the classical ones.

The induced subgraph $A^{-}_{\scriptscriptstyle{G}}[S]$, for any $S\in Mod(G)$, gives the maximal consistent subdiscourse of $G$. Since the graph provides the syntax of a theory, a (typically induced) subgraph corresponds to a kind of subtheory, referred to as a subdiscourse. This concept differs from a subtheory seen as a subset of the formulae. In the graph ${\mathbf{D}}$ from (2.3), $Mod({\mathbf{D}})\subseteq Ker({H})$, where ${H}$ is the induced subgraph

\textstyle{a^{\prime}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{a\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{b\ignorespaces\ignorespaces\ignorespaces\ignorespaces} with the theory \mbox{\mathcal{T}}({H})=\{b\leftrightarrow\neg a, $a\leftrightarrow\neg a^{\prime},a^{\prime}\leftrightarrow\neg a\}$. Its formula $b\leftrightarrow\neg a$ does not occur in the original theory \Delta=\mbox{\mathcal{T}}({\mathbf{D}}) from (2.2), which has instead $b\leftrightarrow\neg a\land\neg c$. A subdiscourse, as an induced subgraph, amounts not only to a subset of the formulae but also, for each retained formula, possibly only a subset of the (negated) atoms under the conjunction in its right side.

Definition (3.3) chooses as $Mod({\mathbf{D}})$ only $\{a\}\in Ker({H})$, making $a={\bf 1}$ and $b={\bf 0}=f$. The other kernel $\{a^{\prime},b\}\in Ker({H})$ is not a semikernel of ${\mathbf{D}}$, while the other semikernel $\{a^{\prime}\}$ of ${\mathbf{D}}$ is not $A^{-}_{\scriptscriptstyle{{\mathbf{D}}}}$-closed. The exact subset of kernels of ${H}$ constituting the models of ${\mathbf{D}}$ can be captured as the classical models $CMod$ from (2.5) – not, however, of ${H}$ but of its appropriate modification, namely, as the kernels of

\textstyle{a^{\prime}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{a\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{b\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\ .} The new loop at $b$ keeps track of the edge $b\mathrel{\rightarrow}c$, which disappeared in ${H}$ but prevents $b$ from being ${\bf 1}$. After all, in the original ${\mathbf{D}}$, $b$ negates $c$ which is not unproblematically ${\bf 0}$. Theorem 4.9 below shows that models of every discourse are exactly the classical models of such a modification of its maximal consistent subdiscourse.

4 Reasoning

The system RES consists of the axiom $\vdash_{\!\!\!\tiny{}}a\overline{a}$, for every atom $a$, and the resolution rule, $\displaystyle{{\Gamma\vdash_{\!\!\!\tiny{}}Aa\ \ \ \ \Gamma\vdash_{\!\!\!\tiny{}}B\overline{a}}\over{\Gamma\vdash_{\!\!\!\tiny{}}AB}}$. Clauses are obtained from the two implications of GNF formulae (2.1). For each $x\in G$, they are of two kinds:

[TABLE]

In terms of a graph $G$, its clausal theory \mbox{\mathcal{C}}(G) contains, for every $x\in G$, the or-clause $A_{\scriptscriptstyle{G}}[x]=\{x\}\cup A_{\scriptscriptstyle{G}}(x)$ and for every $y\in A_{\scriptscriptstyle{G}}(x)$, the nand-clause $\overline{xy}$. For the graph ${\mathbf{D}}$ from (2.3), its clausal theory is:

\mbox{\mathcal{C}}({\mathbf{D}})=\{aa^{\prime},\overline{aa}^{\prime},bac,\overline{ba},\overline{bc},cd,\overline{cd},de,\overline{de},ec,\overline{ec}\}.

We treat clauses as (finite) sets of literals, with overbars marking the negative ones, i.e., we write $A\overline{B}$ for a clause with atoms $A$ and negated atoms $B$. Initial uppercase letters $A,B,C...$ denote typically arbitrary clauses, which is sometimes marked by $C\subseteq\ddot{G}$, where $\ddot{G}=G\cup\{\overline{x}\mid x\in G\}$. For a clause $C$, $C^{-}$ denotes the set of unary clauses with its complementary literals.

Of primary interest to us are graphs (GNF theories) but several results hold for arbitrary clausal theories (sets of finite clauses). By “every $\Gamma$” we mean such theories. (For graphs, the axiom schema is not needed, being provable for every vertex with outgoing edges, e.g., in \mbox{\mathcal{C}}({\mathbf{D}}), resolving $bac$ with $\overline{ba}$ and $\overline{bc}$ yields $b\overline{b}$, etc.) The following gathers some relevant facts about resolution:

Fact 4.1

For every $\Gamma$ over atoms $G$ and a clause $C\subseteq\ddot{G}:$

$\Gamma\vdash_{\!\!\!\tiny{}}{C}\mathrel{\Rightarrow}\Gamma\models_{c}{C}$, 2. 2.

$CMod(\Gamma)=\emptyset\Leftrightarrow\Gamma\vdash_{\!\!\!\tiny{}}\{\}$, 3. 3.

$\Gamma\models_{c}C\Leftrightarrow\Gamma,{C}^{-}\vdash_{\!\!\!\tiny{}}\{\}$, 4. 4.

$\Gamma\models_{c}{C}\Leftrightarrow\exists{B}\subseteq{C}:\Gamma\vdash_{\!\!\!\tiny{}}{B}$, 5. 5.

$\Gamma\vdash_{\!\!\!\tiny{}}\{\}\Leftrightarrow\exists a\in G:\Gamma\vdash_{\!\!\!\tiny{}}a\land\Gamma\vdash_{\!\!\!\tiny{}}\overline{a}$* denoted $\Gamma\vdash_{\!\!\!\tiny{}}\bot(a)$,* 6. 6.

Denoting $\mbox{RES}(\Gamma)=\{C\mid\Gamma\vdash_{\!\!\!\tiny{}}C\}$:

$\mbox{RES}(\Gamma,A^{-})=\mbox{RES}(\Gamma)\cup A^{-}\cup\{P\setminus B\mid\Gamma\vdash_{\!\!\!\tiny{}}P\ {\rm and}\ B\subseteq A\}.$**

For diagnosing inconsistency of $\Gamma$, pinpointing the problem to specific atoms is not necessary, and it suffices that $\Gamma\vdash_{\!\!\!\tiny{}}\{\}$, as guaranteed by point 2. This point implies also refutational completeness with respect to all classical consequences, 3. But we consider instead only direct (not refutational) derivability, i.e., we ask if $\Gamma\vdash_{\!\!\!\tiny{}}C$, instead of $\Gamma,C^{-}\vdash_{\!\!\!\tiny{}}\{\}$. This gives weakened completeness, 4, which could be repaired by adding the weakening rule. But its absence, and the consequent inadmissibility of Ex Falso, arise now as virtues rather than vices. They give a paraconsistent ability to contain paradox and reason about the subdiscourse unaffected by it.

As a simple example, for $\Gamma=\{x,\overline{x},s\}$, we have $\Gamma\vdash_{\!\!\!\tiny{}}\{\}$ but also $\Gamma\not\vdash_{\!\!\!\tiny{}}\overline{s}$. Its graph –

\textstyle{x\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\ \ \ s} – justifies this: the liar $x$ is in no way “connected” to $s$. This is the essence of the phenomenon, which we now describe in more detail.

Example 4.2

*The closure of $F_{2}:$       \textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces f\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{y\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{s,} that is, of its clausal theory $\Gamma_{2}=\{\overline{f},fy,ys,\overline{ys},s\}$ contains, besides $\{\}$, all literals.

The clausal theory \mbox{\mathcal{C}}({\mathbf{D}})=\{aa^{\prime},\overline{aa}^{\prime},bac,\overline{ba},\overline{bc},cd,\overline{cd},de,\overline{de},ec,\overline{ec}\} is provably paradoxical, but neither $b$, $a^{\prime}$ nor $\overline{a}$ are provable. Its deductive closure contains $\bot(x)$ for each $x\in\{c,d,e\}$ and, besides that, only $\overline{b}$, $a$ and $\overline{a}^{\prime}$. It determines thus the only member of $Mod({\mathbf{D}})$.*

This is no coincidence – RES derives clauses satisfied by all $Mod(G)$ and, extended with appropriate weakening, exactly these clauses, but proving this will take the rest of this section. First, we register soundness of RES for all 3-partitions.

Fact 4.3

For every 3-partition $\alpha$ of $G$, every $a\in G$ and $A,B\subseteq\ddot{G}:$

$\alpha\models a\overline{a}$* and $\alpha\models Aa\land\alpha\models B\overline{a}\mathrel{\Rightarrow}\alpha\models AB$.*

Proof. Let $\alpha=\langle\alpha^{\bf 1},\alpha^{\bf 0},\alpha^{\bot}\rangle$ be an arbitrary 3-partition of $G$. Obviously, $\alpha\models a\overline{a}$, for if $a\not\in\alpha^{\bf 1}\cup\alpha^{\bf 0}$, then $a\in\alpha^{\bot}$. Assume that $\alpha\models Aa$ and $\alpha\models B\overline{a}$. If $AB\subseteq\alpha^{\bot}$, then $\alpha\models AB$, also when $AB=\{\}$, since then both $\alpha\models a$ and $\alpha\models\overline{a}$, which imply $a\in\alpha^{\bot}$. Assuming $AB\not\subseteq\alpha^{\bot}$, either $A\not\subseteq\alpha^{\bot}$ or $B\not\subseteq\alpha^{\bot}$. Wlog., assume $A\not\subseteq\alpha^{\bot}$. If $B\subseteq\alpha^{\bot}$, then $a\in\alpha^{\bf 0}\cup\alpha^{\bot}$ because $\alpha\models B\overline{a}$. Then $A$ contains a literal which witnesses to its truth (positive in $\alpha^{\bf 1}$ or negative in $\alpha^{\bf 0}$), and to the truth of the conclusion. If $B\not\subseteq\alpha^{\bot}$, then either $a\in\alpha^{\bf 0}$, and the conclusion follows as in the previous case, or $B$ contains a literal witnessing to its truth, and to the truth of the conclusion.

Consequently, our semantics agrees with the classical one as to which theories count as inconsistent and RES proves inconsistency for exactly these theories:

(a) $\Gamma\models\{\}\Leftrightarrow\Gamma\models_{c}\{\}$

(b) $\Gamma\models\{\}\Leftrightarrow\Gamma\vdash_{\!\!\!\tiny{}}\{\}$.

(a) follows by $\Gamma\models_{c}\{\}\Leftrightarrow CMod(\Gamma)=\emptyset\stackrel{{\scriptstyle\ref{RES}.\ref{ref}}}{{\mathrel{\Rightarrow}}}\Gamma\vdash_{\!\!\!\tiny{}}\{\}\stackrel{{\scriptstyle\ref{sound}}}{{\mathrel{\Rightarrow}}}\Gamma\models\{\}$. Conversely, if $\Gamma\models\{\}$ then for every $\alpha\in Mod(\Gamma):\alpha^{\bot}\not=\emptyset$, i.e., $CMod(\Gamma)=\emptyset$, so $\Gamma\models_{c}\{\}$. Combining (a) with $\Gamma\vdash_{\!\!\!\tiny{}}\{\}\Leftrightarrow\Gamma\models_{c}\{\}$ from Fact 4.1.(2) yields (b).

The rest of this section is concerned primarily with the situations when $\Gamma\vdash_{\!\!\!\tiny{}}\{\}$ and $\exists x\in G:\Gamma\not\vdash_{\!\!\!\tiny{}}\bot(x)$. The constructions and results are general, but they trivialize when one of these conditions is violated. Given an arbitrary $\Gamma$, we construct $\Gamma^{ok}$ – the maximal consistent subdiscourse, with the additional requirement on its border vertices, which refer to the inconsistent elements. ($\Gamma^{ok}$ is empty if all atoms are inconsistent and coincides with $\Gamma$, if none is.) The classical models of $\Gamma^{ok}$ turn out to be the models of $\Gamma$, Theorem 4.9. This leads to the completeness of RES, where every clause satisfied by all $Mod(G)$ has a nonempty provable witness, Corollary 4.11. Augmenting RES with appropriate weakening yields then a strongly complete reasoning system. Some technicalities below, originating from [10], are adjusted to the present context and repeated to make the paper self-contained. The main results, Theorem 4.9 and Corollary 4.11, are new.

For a clausal theory $\Gamma\subseteq{\mathcal{P}}(\ddot{G})$ and $X\subseteq G$, the operation

$\Gamma\mathop{\setminus\!\!\setminus}X=\{C\setminus\ddot{X}\mid C\in\Gamma\}\setminus\{\{\}\}$

removes all literals over atoms $X$ from all clauses of $\Gamma$, removing also the empty clause, if it appears. It satisfies the following important property, relating consequences of $\Gamma$ to consequences of $\Gamma\mathop{\setminus\!\!\setminus}X$.

Lemma 4.4

For each $\Gamma$ and $A\not\subseteq\ddot{X}:\Gamma\vdash_{\!\!\!\tiny{}}A\Rightarrow\exists B\subseteq A\setminus\ddot{X}:\Gamma\mathop{\setminus\!\!\setminus}X\vdash_{\!\!\!\tiny{}}B$.

Proof. If $\Gamma\mathop{\setminus\!\!\setminus}X\vdash_{\!\!\!\tiny{}}\{\}$ the claim follows, so we assume that this is not the case and proceed by induction on the length of the proof $\Gamma\vdash_{\!\!\!\tiny{}}A$, with axioms introducing ${A\setminus\ddot{X}}$ instead of $A$. A step $\displaystyle{{\Gamma\vdash_{\!\!\!\tiny{}}A_{1}a\ \ \ \ \Gamma\vdash_{\!\!\!\tiny{}}A_{2}\overline{a}}\over{\Gamma\vdash_{\!\!\!\tiny{}}A_{1}A_{2}}}$, where $A=A_{1}A_{2}$, has by IH the corresponding proofs $\Gamma\mathop{\setminus\!\!\setminus}X\vdash_{\!\!\!\tiny{}}(A_{1}a)\setminus\ddot{X}$ and $\Gamma\mathop{\setminus\!\!\setminus}X\vdash_{\!\!\!\tiny{}}(A_{1}a)\setminus\ddot{X}$. If $a\in\ddot{X}$, either of these proofs can serve as the conclusion. Otherwise, conclusion follows by the deduction $\displaystyle{{\Gamma\vdash_{\!\!\!\tiny{}}(A_{1}\setminus\ddot{X})a\ \ \ \ \Gamma\vdash_{\!\!\!\tiny{}}(A_{2}\setminus\ddot{X})\overline{a}}\over{\Gamma\vdash_{\!\!\!\tiny{}}A_{1}A_{2}\setminus\ddot{X}}}$.

Hence, if $\Gamma\vdash_{\!\!\!\tiny{}}C$ and $C$ contains at least one literal not in $\ddot{X}$, Then $\Gamma\mathop{\setminus\!\!\setminus}X\vdash_{\!\!\!\tiny{}}C^{\prime}$ for some nonempty $C^{\prime}\subseteq C$: removing literals from $\Gamma$ using $\mathop{\setminus\!\!\setminus}$, results at most in sharpening the information about the remaining atoms. Let us denote:

$G^{\bot}=\{x\in G\mid\Gamma\vdash_{\!\!\!\tiny{}}x\land\Gamma\vdash_{\!\!\!\tiny{}}\overline{x}\}$

$\Gamma^{ok}=\Gamma\mathop{\setminus\!\!\setminus}G^{\bot}=\{C\setminus G^{\bot}\mid C\in\Gamma\}\setminus\{\{\}\}$

$G^{ok}=G\setminus G^{\bot}=\bigcup\Gamma^{ok}$.

$G^{\bot}$ contains all provably paradoxical atoms, while its complement $G^{ok}$ could be taken as the atomic extension of the consistency-operator, if we were aiming at a logic of formal inconsistency. As we will see, it coincides with the domain of the maximal consistent subdiscourse, $A^{-}_{\scriptscriptstyle{G}}[S]$, for any $S\in Mod(G)$. For now, we only note that $G^{\bot}$ is $A_{\scriptscriptstyle{G}}$-closed, Fact 4.5, and that $\Gamma^{ok}$ remains consistent alongside $G^{\bot}$ and conservative over $\Gamma$ with respect to the nonparadoxical atoms $G^{ok}$, as made precise by Fact 4.6.

Fact 4.5

For every $\Gamma$ and $x\in G:$ $\Gamma\vdash_{\!\!\!\tiny{}}\bot(x)\mathrel{\Rightarrow}\forall y\in A_{\scriptscriptstyle{G}}(x):\Gamma\vdash_{\!\!\!\tiny{}}\bot(y)$.

Proof. $\Gamma\vdash_{\!\!\!\tiny{}}x$ and the axiom $\overline{xy}_{i}$, for each $y_{i}\in A_{\scriptscriptstyle{G}}(x)$, give $\Gamma\vdash_{\!\!\!\tiny{}}\overline{y}_{i}$. Resolving then $xy_{1}...y_{n}$ with $\overline{x}$ and $\overline{y}_{j}$, for all $j\not=i$, gives $\Gamma\vdash_{\!\!\!\tiny{}}\overline{y}_{i}$ for each $y_{i}\in A_{\scriptscriptstyle{G}}(x)$.

Fact 4.6

For $\Gamma$ with $G^{ok}\not=\emptyset$:

$\forall A\in\Gamma^{ok}:\Gamma\vdash_{\!\!\!\tiny{}}A$, so $\forall C\subseteq\ddot{G}^{ok}:\Gamma^{ok}\vdash_{\!\!\!\tiny{}}C\mathrel{\Rightarrow}\Gamma\vdash_{\!\!\!\tiny{}}C$. 2. 2.

$\Gamma^{ok}\not\vdash_{\!\!\!\tiny{}}\{\}$. 3. 3.

$\forall x\in G^{ok}:\Gamma^{ok}\vdash_{\!\!\!\tiny{}}x\Leftrightarrow\Gamma\vdash_{\!\!\!\tiny{}}x$* and $\Gamma^{ok}\vdash_{\!\!\!\tiny{}}\overline{x}\Leftrightarrow\Gamma\vdash_{\!\!\!\tiny{}}\overline{x}$.* 4. 4.

$\exists x\in G^{ok}:\Gamma^{ok}\not\vdash_{\!\!\!\tiny{}}\overline{x}$, hence also $\Gamma\not\vdash_{\!\!\!\tiny{}}\overline{x}$. 5. 5.

$\forall x\in G^{ok}:\Gamma^{ok}\not\vdash_{\!\!\!\tiny{}}\overline{x}\mathrel{\Rightarrow}A_{\scriptscriptstyle{G}}(x)\subseteq G^{ok}$* (when $\Gamma$ is a graph).*

Proof. 1. Since for each atom $a\not\in G^{ok}$, both $\Gamma\vdash_{\!\!\!\tiny{}}a$ and $\Gamma\vdash_{\!\!\!\tiny{}}\overline{a}$, such atoms can be resloved away from every clause of $\Gamma$. Each clause of $\Gamma^{ok}$ is obtained exactly by such an operation.

2. $\Gamma^{ok}\vdash_{\!\!\!\tiny{}}\{\}\stackrel{{\scriptstyle\ref{RES}.\ref{xnotx}}}{{\mathrel{\Rightarrow}}}\exists x\in G^{ok}:\Gamma^{ok}\vdash_{\!\!\!\tiny{}}x\land\Gamma^{ok}\vdash_{\!\!\!\tiny{}}\overline{x}\stackrel{{\scriptstyle\ref{it:a}.}}{{\mathrel{\Rightarrow}}}\Gamma\vdash_{\!\!\!\tiny{}}x\land\Gamma\vdash_{\!\!\!\tiny{}}\overline{x}\mathrel{\Rightarrow}x\not\in G^{ok}$.

3. Implications to the right follow by point 1, while to the left by Lemma 4.4 and point 2.

4. If $\forall x\in G^{ok}:\Gamma^{ok}\vdash_{\!\!\!\tiny{}}\overline{x}$, then also $\forall y\in G:\Gamma\vdash_{\!\!\!\tiny{}}\overline{y}$, and then $\forall y\in G:\Gamma\vdash_{\!\!\!\tiny{}}y$, contradicting $G^{ok}\not=\emptyset$.

5. If $x\in G^{ok}$ has a $y\in A_{\scriptscriptstyle{G}}(x)\cap G^{\bot}$, then $\Gamma\vdash_{\!\!\!\tiny{}}y\mathrel{\Rightarrow}\Gamma\vdash_{\!\!\!\tiny{}}\overline{x}\stackrel{{\scriptstyle\ref{it:single}.}}{{\mathrel{\Rightarrow}}}\Gamma^{ok}\vdash_{\!\!\!\tiny{}}\overline{x}$.

When $\Gamma$ represents a graph $G$, $\Gamma^{ok}$ is almost the theory of its induced subgraph $G^{ok}$, except for a difference at its border $brd(G^{ok})=\{x\in G^{ok}\mid A_{\scriptscriptstyle{G}}(x)\not\subseteq G^{ok}\}$. For instance, for our discourse {\mathbf{D}}=\raisebox{3.01385pt}{\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 6.41293pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern 0.0pt\offinterlineskip\halign{\entry@#!@&&\entry@@#!@\cr&&&&&\crcr}}}\ignorespaces{\hbox{\kern-6.41293pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{\textstyle{a^{\prime}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 16.37157pt\raise 2.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 16.37157pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{\textstyle{a\ignorespaces\ignorespaces\ignorespaces\ignorespaces}}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 6.41295pt\raise-2.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 37.61609pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{\textstyle{b\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 27.65746pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 57.86638pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 57.86638pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{\textstyle{c\ignorespaces\ignorespaces\ignorespaces\ignorespaces}}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 78.15256pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 78.15256pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{\textstyle{d\ignorespaces\ignorespaces\ignorespaces\ignorespaces}}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 99.31606pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 99.31606pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{\textstyle{e\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{}{}{{}{}{}{}{}{}{}{}{}{}{}{}{}}{}\ignorespaces\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{{}{}{{}}{{}{}{}}{}}}}\ignorespaces{}\ignorespaces{}{}{}{{}{}{}{}{}{}{}{}{}{}{}{}{}{}}{\hbox{\kern 68.1913pt\raise 2.6074pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{{}{}{}{{}}{{}{}{}\lx@xy@spline@}{}}}}\ignorespaces{}\ignorespaces\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{{}{}{{}}{{}{}{}}{}}}}\ignorespaces{}\ignorespaces}}}}\ignorespaces}:

[TABLE]

As in this example so generally, border vertices enter as negative literals into \Gamma^{ok}=\mbox{\mathcal{C}}(G^{ok})\cup(brd(G^{ok}))^{-}, according to Fact 4.6.(5). One can thus view $\Gamma^{ok}$ as (the theory of) the subgraph induced by $G^{ok}$, with a loop added at each border vertex. It is consistent, Fact 4.6.(2), so its models are kernels of $G^{ok}$ excluding border vertices:

[TABLE]

These classical models of $\Gamma^{ok}$ are actually the models $Mod(\Gamma)$ from (3.3). To show this, we first register a preliminary observation.

Fact 4.8

$CMod(\Gamma^{ok})\subseteq SK(G)$.

Proof. Since each $L\in CMod(\Gamma^{ok})$ is a kernel of $G^{ok}$, it is obviously independent in $G^{ok}$ and, since $G^{ok}$ is an induced subgraph of $G$ (only with additional loops), so $L$ is independent also in $G$. Hence $A^{-}_{\scriptscriptstyle{G}}(L)\subseteq G\setminus L$.

By soundness of RES, if $a\in L$ then $\Gamma^{ok}\not\vdash_{\!\!\!\tiny{}}\overline{a}$, which by Fact 4.6.(5) means that $A_{\scriptscriptstyle{G}}(a)\subseteq G^{ok}$, so that $A_{\scriptscriptstyle{G}}(a)=A_{\scriptscriptstyle{G^{ok}}}(a)\subseteq A^{-}_{\scriptscriptstyle{G^{ok}}}(L)$, where the inclusion follows since $L\in Ker(G^{ok})$. Obviously, $A^{-}_{\scriptscriptstyle{G^{ok}}}(L)\subseteq A^{-}_{\scriptscriptstyle{G}}(L)$. Combining the two yields $A_{\scriptscriptstyle{G}}(L)\subseteq A^{-}_{\scriptscriptstyle{G}}(L)\subseteq G\setminus L$, i.e., $L\in SK(G)$.

Writing $S\models\Gamma$ or $S\in pSK(G)$, for an $S\in SK(G)$, we mean $\alpha_{S}\models\Gamma$ or $\alpha_{S}\in pSK(G)$, for $\alpha_{S}=\langle S,A^{-}_{\scriptscriptstyle{G}}(S),G\setminus A^{-}_{\scriptscriptstyle{G}}[S]\rangle$. The bijection in the theorem, $CMod(\Gamma^{ok})\simeq Mod(G)$, means then $A^{-}_{\scriptscriptstyle{G^{ok}}}(S)=A^{-}_{\scriptscriptstyle{G}}(S)$, for relevant $S$, and

• (\mathrel{\ooalign{\raise 0.86108pt\hbox{\supset}\cr\raise-3.44444pt\hbox{\scalebox{0.8}{\sim}}\cr}})

$\forall\langle S,A^{-}_{\scriptscriptstyle{G}}(S),G\setminus A^{-}_{\scriptscriptstyle{G}}[S]\rangle\in Mod(G):\langle S,A^{-}_{\scriptscriptstyle{G}}(S)\rangle\in CMod(G^{ok})$ and

• (\mathrel{\ooalign{\raise 0.86108pt\hbox{\subset}\cr\raise-3.44444pt\hbox{\scalebox{0.8}{\sim}}\cr}})

$\forall\langle S,A^{-}_{\scriptscriptstyle{G^{ok}}}(S)\rangle\in CMod(\Gamma^{ok}):\langle S,A^{-}_{\scriptscriptstyle{G}}(S),G\setminus A^{-}_{\scriptscriptstyle{G}}[S]\rangle\in Mod(G)$.

Theorem 4.9

For every theory $\Gamma$ with graph $G:CMod(\Gamma^{ok})\simeq Mod(G)$.

Proof. (\mathrel{\ooalign{\raise 0.86108pt\hbox{\supset}\cr\raise-3.44444pt\hbox{\scalebox{0.8}{\sim}}\cr}}). follows using Fact 4.3 but first we show that (1a) if $S\in Mod(G)$ then $S\models\Gamma$. This and (1b) hold actually for every $S\in pSK(G)$:

(1a) $S\in pSK(G)\mathrel{\Rightarrow}S\models\Gamma$. For each $y\in A_{\scriptscriptstyle{G}}(x)$, i.e., $\overline{xy}$, we have one of four cases, each yielding $S\models\overline{xy}$:

• (i)

$y\in S\mathrel{\Rightarrow}x\in A^{-}_{\scriptscriptstyle{G}}(S)$,

• (ii)

$x\in S\mathrel{\Rightarrow}y\not\in S$ and, since $S\in SK(G)$, $y\in A^{-}_{\scriptscriptstyle{G}}(S)$,

• (iii)

$x\in A^{-}_{\scriptscriptstyle{G}}(S)$ or $y\in A^{-}_{\scriptscriptstyle{G}}(S)$,

• (iv)

$\{x,y\}\subseteq G\setminus A^{-}_{\scriptscriptstyle{G}}[S]$.

For each $A_{\scriptscriptstyle{G}}[x]=\{x\}\cup Y$, we have one of five cases, each giving $S\models A_{\scriptscriptstyle{G}}[x]$:

• (i)

$\exists y\in Y:y\in S$,

• (ii)

$x\in S$,

• (iii)

$x\in A^{-}_{\scriptscriptstyle{G}}(S)\mathrel{\rightarrow}\exists y\in Y:y\in S$,

• (iv)

$\exists y\in Y:y\in A^{-}_{\scriptscriptstyle{G}}(S)$, since $S\in pSK(G)$, so $x\in A^{-}_{\scriptscriptstyle{G}}[S]$ and $S\models A_{\scriptscriptstyle{G}}[x]$ by (ii) or (iii),

• (v)

$A_{\scriptscriptstyle{G}}[x]\subseteq G\setminus A^{-}_{\scriptscriptstyle{G}}[S]$.

(1b) $\forall S\in pSK(G):\Gamma\vdash_{\!\!\!\tiny{}}\bot(x)\mathrel{\Rightarrow}x\not\in A^{-}_{\scriptscriptstyle{G}}[S]$.

By (1a) $S\in pSK(G)\mathrel{\Rightarrow}S\models\Gamma$ so, by soundness Fact 4.3, for any clause $C:\Gamma\vdash_{\!\!\!\tiny{}}C\mathrel{\Rightarrow}S\models C$. Hence, $\Gamma\vdash_{\!\!\!\tiny{}}\bot(x)\mathrel{\Rightarrow}S\models\bot(x)$, i.e., $x\in G\setminus A^{-}_{\scriptscriptstyle{G}}[S]$.

(1c) We show that $S\in Mod(G)$ satisfies (4.7). By Fact 4.6.(2), $\Gamma^{ok}\not\vdash_{\!\!\!\tiny{}}\{\}$ so, by Fact 4.1.(2), there is some $K\in Ker(G^{ok})$, i.e., one with $A^{-}_{\scriptscriptstyle{G}}[K]=G^{ok}$. By (2a-b) below, $K\in pSK(G)$; since $S\in mpSK(G)$ (as $S\in Mod(G)$ and (3.7)), so $A^{-}_{\scriptscriptstyle{G}}[S]\supseteq A^{-}_{\scriptscriptstyle{G}}[K]=G^{ok}$. By (1b), $x\in A^{-}_{\scriptscriptstyle{G}}[S]\mathrel{\Rightarrow}x\not\in G^{\bot}\mathrel{\Rightarrow}x\in G^{ok}$, i.e., $A^{-}_{\scriptscriptstyle{G}}[S]\subseteq G^{ok}$, so that $A^{-}_{\scriptscriptstyle{G}}[S]=G^{ok}$. By (3.6), $A^{-}_{\scriptscriptstyle{G}}(G^{ok})\subseteq G^{ok}$, so since $G^{ok}$ is induced subgraph of $G:A^{-}_{\scriptscriptstyle{G^{ok}}}(S)=A^{-}_{\scriptscriptstyle{G}}(S)$ and then, since $S\cap A^{-}_{\scriptscriptstyle{G}}(S)=\emptyset$ as $S\in SK(G)$, so $A^{-}_{\scriptscriptstyle{G^{ok}}}(S)=G^{ok}\setminus S$ – showing that $S\in Ker(G^{ok})$.

If $x\in brd(G^{ok})$ then $\Gamma\vdash_{\!\!\!\tiny{}}\overline{x}$, so $S\models\overline{x}$, i.e., $x\not\in S$ and, since $S\in Ker(G^{ok}):x\in G^{ok}\setminus S=A^{-}_{\scriptscriptstyle{G}}[S]\setminus S=A^{-}_{\scriptscriptstyle{G}}(S)$. Thus $brd(G^{ok})\subseteq A^{-}_{\scriptscriptstyle{G}}(S)$.

(\mathrel{\ooalign{\raise 0.86108pt\hbox{\subset}\cr\raise-3.44444pt\hbox{\scalebox{0.8}{\sim}}\cr}}). (2a) $CMod(\Gamma^{ok})\subseteq SK(G)$ is Fact 4.8.

(2b) By Fact 4.5, $\Gamma\vdash_{\!\!\!\tiny{}}\bot(x)\mathrel{\Rightarrow}\forall y\in A_{\scriptscriptstyle{G}}(x):\Gamma\vdash_{\!\!\!\tiny{}}\bot(y)$, so $A_{\scriptscriptstyle{G}}(G^{\bot})\subseteq G^{\bot}$. Hence $A^{-}_{\scriptscriptstyle{G}}(G\setminus G^{\bot})\subseteq(G\setminus G^{\bot})$, i.e., $A^{-}_{\scriptscriptstyle{G}}(G^{ok})\subseteq G^{ok}$ and so

\begin{array}[]{rcl}A^{-}_{\scriptscriptstyle{G}}(A^{-}_{\scriptscriptstyle{G}}[G^{ok}])&=&A^{-}_{\scriptscriptstyle{G}}(A^{-}_{\scriptscriptstyle{G}}(G^{ok})\cup G^{ok})\\ &=&A^{-}_{\scriptscriptstyle{G}}(A^{-}_{\scriptscriptstyle{G}}(G^{ok}))\cup A^{-}_{\scriptscriptstyle{G}}(G^{ok})\subseteq A^{-}_{\scriptscriptstyle{G}}(G^{ok})\cup G^{ok}=A^{-}_{\scriptscriptstyle{G}}[G^{ok}].\end{array}

(2c) When $S\in Ker(G^{ok})$ then $A^{-}_{\scriptscriptstyle{G}}[S]=G^{ok}$ and $S\in pSK(G)$, by (2a-b). If $S\not\in mpSK(G)$, i.e., $\exists R\in pSK(G):A^{-}_{\scriptscriptstyle{G}}[R]\not\subseteq A^{-}_{\scriptscriptstyle{G}}[S]$, Lemma 3.9 yields a strict extension $A^{-}_{\scriptscriptstyle{G}}[Q]\supset A^{-}_{\scriptscriptstyle{G}}[S]$. This requires adding some $E\subseteq G^{\bot}$, but by (1b) no $e\in E$ can belong to any $A^{-}_{\scriptscriptstyle{G}}[Q]$ with $Q\in pSK(G)$, since $\Gamma\vdash_{\!\!\!\tiny{}}\bot(e)$.

The theorem implies that $\langle\alpha^{\bf 1},\alpha^{\bf 0},\alpha^{\bot}\rangle\in Mod(G)$ iff $\langle\alpha^{\bf 1},\alpha^{\bf 0}\rangle\in CMod(\Gamma^{ok})$, giving the middle equality: $G\setminus\alpha^{\bot}=\alpha^{\bf 1}\cup\alpha^{\bf 0}=G^{ok}=G\setminus G^{\bot}$, which yields:

[TABLE]

Thus RES proves both $a$ and $\overline{a}$ exactly for the atoms $a$ falling outside the healthy, boolean domain of every model. The following completeness of RES for $\models$ is the counterpart of its classical completeness for $\models_{c}$ from Fact 4.1.(4).

Corollary 4.11

For every $\Gamma$ and clause $A\subseteq\ddot{G}:$

\begin{array}[]{ll}\Gamma\models A\ \ \Longleftrightarrow\ \ A\subseteq G^{\bot}\not=\emptyset\ \text{ or }\ \exists B\not=\{\}:B\subseteq A\cap\ddot{G}^{ok}\land\Gamma\vdash_{\!\!\!\tiny{}}B.\end{array}**

Proof. $\Rightarrow$) Assume that $\Gamma\models A$. If $A\subseteq\ddot{G}^{\bot}$ then $G^{\bot}\not=\emptyset$ by (3.4) and we are done. If $A\not\subseteq\ddot{G}^{\bot}$, i.e., $C=A\setminus\ddot{G}^{\bot}\not=\emptyset$, then $C\subseteq A\cap\ddot{G}^{ok}$ and, by (3.4), $\Gamma\models C$ (since $\forall\alpha\in Mod(\Gamma):G^{\bot}=\alpha^{\bot}$ by (4.10)). Hence, by Theorem 4.9, $\Gamma^{ok}\models_{c}C$ which, by Fact 4.1.(4), implies $\exists B\subseteq C:\Gamma^{ok}\vdash_{\!\!\!\tiny{}}B$. By Fact 4.6.(2), $B\not=\{\}$, while by 4.6.(1), $\Gamma\vdash_{\!\!\!\tiny{}}B$, yielding the conclusion, since $B\subseteq A\cap\ddot{G}^{ok}$.

$\Leftarrow$) If $A\subseteq G^{\bot}\not=\emptyset$ then $\Gamma\models A$ directly by (3.4). Otherwise, as $\Gamma\vdash_{\!\!\!\tiny{}}B$ so $\Gamma\models B$ by Fact 4.3. Since $\emptyset\not=B\subseteq A\cap\ddot{G}^{ok}$, so $\Gamma\models A$ by (3.4).

Comparison with Fact 4.1.(4) shows that while in classical logic $\{\}$ witnesses to every clause by Ex Falso, in our logic all consequences of a theory have nonempty provable witnesses: $\Gamma\models\{\}$ iff $G^{\bot}\not=\emptyset$, i.e., $\exists x:\Gamma\vdash_{\!\!\!\tiny{}}x$ and $\Gamma\vdash_{\!\!\!\tiny{}}\overline{x}$, while $\Gamma\models A\not=\{\}$ is witnessed only by a proof from $\Gamma$ of either $\bot(a)$, for all $a\in A$, or of some nonempty subclause $B\subseteq A$.

The implication to the left in Corollary 4.11 specifies more closely the patterns of weakening admisible in our logic. Not only Ex Falso is excluded, but weakening has to preserve, so to say, the reason of satisfaction of its premise. The first case (right-to-left implication from the first disjunct in Corollary 4.11) allows to weaken the empty clause only to a disjunction of literals involved in inconsistency, reflecting the irrelevance of the empty clause for the consistent subdiscourse. The second case ensures that the resulting $A$ contains a healthy (i.e., not involving any paradox) $B\subseteq A$ witnessing to its satisfaction. Thus, adding to RES either both (aW) and (bW) or only (cW)

[TABLE]

yields a sound and strongly complete system for classical logic, with (cW), or for our paraconsistent logic, with (aW) and (bW). For consistent $\Gamma$, the two coincide. Since $G^{\bot}=\emptyset$, (bW) is inapplicable, while (aW) becomes exactly (cW), since then every $B\not\subseteq G^{\bot}$.

The conditions of (aW) and (bW), reflecting the right side of Corollary 4.11, prevent uncontrolled mixing of consistent and inconsistent elements. As an example, consider the usual derivation of Lewis’ “paradox”, recasting Ex Falso using disjunctive syllogism. Assuming $\Gamma\vdash_{\!\!\!\tiny{}}a$ and $\Gamma\vdash_{\!\!\!\tiny{}}\overline{a}$, we have

\displaystyle{{\mbox{\displaystyle{{\Gamma\vdash_{!!!\tiny{}}a}\over{\Gamma\vdash_{!!!\tiny{}}ab}}}\ (cW)\ \ \mbox{\displaystyle{\begin{array}[]{c}\ {\Gamma\vdash_{!!!\tiny{}}\overline{a}}\end{array}}}}\over{\Gamma\vdash_{\!\!\!\tiny{}}b}} (DS)

The step (DS) is an instance of resolution, but since $\{a\}\subseteq G^{\bot}$, (aW) can not be applied instead of (cW).

5 A remark on relevance

Rule (aW) is not very effective, requiring to find $b\in B$ for which $b$ or $\overline{b}$ is not provable, while rule (bW) joins nonsensical premises into a nonsensical disjunction. These rules, extending RES to a strongly complete system, provoke also the question: what do we lose by dropping them? RES remains complete in the sense of Corollary 4.11; if $a\lor b$ is a consequence of our theory, we may be able to prove $a$, but not necessarily $a\lor b$. Is it such a loss? If we know that $a$ is true, it is not particularly enlightening that so is $a\lor b$. In this way, the tautology $\neg a\lor a$ can be diluted to, say,

[TABLE]

With implication $x\mathrel{\rightarrow}y$ defined as $\neg x\lor y$, (i) represents some fallacies of relevance, typical for material implication, e.g., $a\mathrel{\rightarrow}(b\mathrel{\rightarrow}a)$ and $\neg a\mathrel{\rightarrow}(a\mathrel{\rightarrow}\neg b)$, for strict implication, e.g., $b\mathrel{\rightarrow}(a\mathrel{\rightarrow}a)$ or $b\mathrel{\rightarrow}(\neg a\lor a)$, or for the intutionistic one, $\neg(a\mathrel{\rightarrow}a)\mathrel{\rightarrow}b$. RES is immune against such fallacies, which arise in the language of clauses from disjunctive weakening. Note that while this rule may be indispensable in various systems of Gentzen or natural deduction, in RES it is not, since here its only contribution is dilution of provable facts. Dropping all forms of weakening, we lose such diluted consequences, but gain relevance, simplifying reasoning at the same time. The following remarks elaborate these gains. Without aiming at a logic of relevance, they only identify its elements in the present setting.

Let us first note that the language of clauses, viewed as sets of literals, identifies, for instance, $a\mathrel{\rightarrow}(a\mathrel{\rightarrow}b)$ and $a\mathrel{\rightarrow}b$, representing both as $\overline{a}b$ and enforcing their equivalence. One could see it as an unfortunate equivocation but, with the present semantics, it only eliminates spurious syntax.444RES with this language can be seen as a restriction of $RMI_{\scriptscriptstyle{\stackrel{{\scriptstyle\sim}}{{+}}}}$ with the usual sequential syntax, from [1]. The equivalence of $RMI_{\scriptscriptstyle{\stackrel{{\scriptstyle\sim}}{{+}}}}$ and $RMI_{\scriptscriptstyle{\stackrel{{\scriptstyle\sim}}{{\mathrel{\rightarrow}}}}}$ shows that the former’s disjunction (specializing to ours in the present context) yields in the latter a satisfactory relevant implication, defined by $A\mathrel{\rightarrow}B=\neg A\lor B$. To handle subtler aspects of relevant implication, such an extension of the syntax and RES, along with the associated semantic adjustments, might be needed.

The absence of weakening prevents RES from deriving, besides fallacies exemplified above, also some other problematic implications, for instance, $(a\mathrel{\rightarrow}b)\land(c\mathrel{\rightarrow}d)\not\vdash_{\!\!\!\tiny{}}(a\mathrel{\rightarrow}d)\lor(c\mathrel{\rightarrow}b)$. From the assumption, represented by the clauses $\overline{a}b,\overline{c}d$, nothing follows by resolution, in particular, not the undesired conclusion, $\overline{a}d\overline{c}b$, which only weakens either premise.

RES enjoys a specifically relevant form of deduction theorem. If $\Gamma,x\vdash_{\!\!\!\tiny{}}y$, it does not follow that $\Gamma\vdash_{\!\!\!\tiny{}}x\mathrel{\rightarrow}y$, i.e., $\Gamma\vdash_{\!\!\!\tiny{}}\overline{x}y$, without further ado. It may namely happen that $\Gamma\vdash_{\!\!\!\tiny{}}y$ without using $x$, and $\Gamma\not\vdash_{\!\!\!\tiny{}}\overline{x}y$. By Fact 4.1.(6), however, if the proof $\Gamma,x\vdash_{\!\!\!\tiny{}}y$ requires $x$, that is, $\Gamma\not\vdash_{\!\!\!\tiny{}}y$, then indeed $\Gamma\vdash_{\!\!\!\tiny{}}\overline{x}y$.

Just as our logic is concerned with consequences of a given theory rather than with tautologies, relevance is judged relatively to the actual context. From some $\Gamma$, (i) may be provable and from others it may not be. For instance

(i1) $\Gamma_{1}\vdash_{\!\!\!\tiny{}}ca\overline{b}$ and $\Gamma_{1}\vdash_{\!\!\!\tiny{}}\overline{a}a\overline{b}$, where $G_{1}=...c\leftarrow a\mathrel{\rightarrow}d\mathrel{\rightarrow}b...$, while

(i2) $\Gamma_{2}\vdash_{\!\!\!\tiny{}}\overline{a}a$  but  $\Gamma_{2}\not\vdash_{\!\!\!\tiny{}}\overline{a}a\overline{b}$, where $G_{2}=...c\leftarrow a\hskip 15.00002ptd\mathrel{\rightarrow}b...$,

where “$...$” indicates a surrounding graph, in which $a$ and $d$ have no incident edges except the indicated ones. The graph syntax makes explicit the reference structure, allowing to read an edge $x\mathrel{\rightarrow}y$ as $x$ “referring to” $y$, by negating $y$. Reference involves relevance, so that $y$, negated by $x$, is relevant for $x$. The atoms reachable by arbitrary paths from a given $x$ are then indirect references, relevant for $x$. This form of relevance is thus transitive, but context dependence and the graph syntax justify this fact. In (i1), $b$ is relevant for $a$, because of their connection through $d$. Making $b={\bf 0}$, forces $a={\bf 0}$. This notion, involving only context dependent interaction between some truth-values of $b$ and $a$, deviates from those attempting to capture some general meaning-connections, for instance, by variable-sharing. The two facts in “Water freezes or temperature is above 0∘C” do not share any variable but are connected by the background knowledge. The meaning-connections, already between atomic facts, are defined by the context $\Gamma$ and reflected by its undiluted consequences. Provability of $\overline{a}a\overline{b}$ in (i1) suggests such a connection of $b$ and $a$, while its unprovability in (i2) witnesses to its absence.

Relevance is more than reference – typically, it is symmetric. In our case, this amounts to following the paths also in the direction opposite to the edges:

\begin{array}[]{l@{\hspace*{3em}}l}\mbox{(a) This and the next statmenet are false.}\hfil\hskip 30.00005pt&a\leftrightarrow\neg a\land\neg b\\[6.45831pt] \mbox{(b) The next statmenet is false.}\hfil\hskip 30.00005pt&b\leftrightarrow\neg c\\[6.45831pt] \mbox{(c) The previous statmenet is false.}\hfil\hskip 30.00005pt&c\leftrightarrow\neg b\end{array}\hskip 20.00003pt\raisebox{28.45274pt}{\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 5.64294pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern 0.0pt\offinterlineskip\halign{\entry@#!@&&\entry@@#!@\cr\\\\\crcr}}}\ignorespaces{\hbox{\kern-5.64294pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{\textstyle{a\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{}{}{}{{}{{}{{}{{}{{}}{}{{}{{}}{}{{}{{}{{}}{}{{}{{}{{}}}}}}}}}}}{}\ignorespaces\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{{}{}{{}}{{}{}{}{}}{}}}}\ignorespaces{}\ignorespaces{}{}{}{}{{}{{}}{}{{}}{}{{}}{}{{}}{}{{}{{}}{}{{}{{}{{}{{}}{}{{}}{}{{}}}}}}}{\hbox{\kern 3.2935pt\raise-2.99599pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{{}{}{}{{}}{{}{}{}{}\lx@xy@spline@}{}}}}\ignorespaces{}\ignorespaces\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{{}{}{{}}{{}{}{}{}}{}}}}\ignorespaces{}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 0.0pt\raise-13.06146pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern-5.14583pt\raise-23.0059pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{\textstyle{b\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{}{}{{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}}{}\ignorespaces\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{{}{}{{}}{{}{}{}}{}}}}\ignorespaces{}\ignorespaces{}{}{}{{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}}{\hbox{\kern-5.16284pt\raise-38.80563pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{{}{}{}{{}}{{}{}{}\lx@xy@spline@}{}}}}\ignorespaces{}\ignorespaces\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{{}{}{{}}{{}{}{}}{}}}}\ignorespaces{}{\hbox{\kern-5.16377pt\raise-46.01181pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{\textstyle{c\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{}{}{{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}}{}\ignorespaces\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{{}{}{{}}{{}{}{}}{}}}}\ignorespaces{}\ignorespaces{}{}{}{{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}}{\hbox{\kern 2.721pt\raise-26.00526pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{{}{}{}{{}}{{}{}{}\lx@xy@spline@}{}}}}\ignorespaces{}\ignorespaces\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{{}{}{{}}{{}{}{}}{}}}}\ignorespaces{}\ignorespaces}}}}\ignorespaces}

In the only model, $b={\bf 1}$ and $a=c={\bf 0}$. But if we remove the loop at $a$, there will be also another model with $a=c={\bf 1}$ and $b={\bf 0}$. One could say that the loop at $a$ forces $b={\bf 1}$, since otherwise inconsistency would arise. Not only $b$, to which $a$ refers, is relevant for $a$, but also $a$ is relevant for $b$, forcing it to be true. In this sense, all “connections” – paths in the underlying graph (the undirected graph, obtained by forgetting directions of the edges) – mark potential relevance. It is thus both symmetric and transitive, so its horizon for an atom $x$ is the strong component of the underlying graph, containing $x$. Indeed, RES proves some clause with literals over atoms $x$ and $y$ if and only if $x$ and $y$ belong to one such component.555Distinct strong components have disjoint alphabets, with no axiomatic clauses containing literals from both; hence no provable clause can contain literals from both. Conversely, if there is a path $\langle x_{1},x_{2},...,x_{n}\rangle$ in the underlying graph, then for each pair $x_{i},x_{i+1}$, $1\leq i<n$, there is a negtive clause $N_{i}=\overline{x_{i}}\overline{x}_{i+1}$ and a positive one $P_{i}=...x_{i}x_{i+1}...$. Resolving $P_{1}$ with $N_{2}$ yields a clause $C_{3}$ containing $x_{1}$ and $\overline{x}_{3}$. Resolving $C_{3}$ with $P_{3}$ gives $C_{4}$ containing $x_{1}$ and $x_{4}$. A clause $C_{n}$, obtained after $n-2$ steps, contains $x_{1}$ and either $x_{n}$ or $\overline{x}_{n}$.

Still, this notion of relevance is too weak, as exemplified by the clause $\overline{a}a\overline{b}$ from (i1). Signaling a connection between $a$ and $b$, it does not impose any dependencies between the truth-values of $a$, $b$ and the whole clause. Its proof in RES is not a mere dilution of $\overline{a}a$, but the clause itself is such a dilution, which is always true because so is its subclause $\overline{a}a$. The sense of relevance should preclude us from saying such things which, even if true, do not add anything to something which is already said more concisely.

Let us therefore consider a clause $C$ relevant, in a given context $\Gamma$, denoted $\Gamma\models_{r}C$, if $\Gamma\models C$ and for each nonempty $B\subset C:\Gamma\not\models B$. For unhealthy atoms, such relevant clauses are the units $a$ and $\overline{a}$, and no other relevant clause contains such atoms. This reminds, once more, of the irrelevance of meaningless/inconsistent elements for the healthy part of a discourse. For each 2-partition $C=AB$ of a nonunit clause $C$ (with at least two literals), we can write $\Gamma\models C$ as $\Gamma\models\bigwedge A^{-}\mathrel{\rightarrow}\bigvee B$. If $\Gamma\models_{r}C$, this implication is not satisfied, so to say, vacuously, by $\Gamma$ having no models satisfying $\bigwedge A^{-}$, but by $\Gamma$ having such models, all satisfying also $\bigvee B$. A relevant $C$ witnesses thus to the influence, which some truth-values of any nonempty proper subclause $A\subset C$ have for its complement $B=C\setminus A$: whenever $\bigwedge A^{-}={\bf 1}$, then $\bigvee B={\bf 1}$, and there are cases when $\bigwedge A^{-}={\bf 1}$. This last proviso is the element of relevance. The relation is obviously symmetric: if $\bigwedge A^{-}\mathrel{\rightarrow}\bigvee B$, then also $\bigwedge B^{-}\mathrel{\rightarrow}\bigvee A$.

This is a much stronger notion than mere membership in the same component of the underlying graph. In the example (i1), $\Gamma_{1}\not\models_{r}\overline{a}a\overline{b}$ since $\overline{a}a\subseteq\overline{a}a\overline{b}$, so the fact that $\Gamma_{1}\models\overline{a}a\overline{b}$ does not imply relevance in this strong sense. On the other hand, $\Gamma_{1}\vdash_{\!\!\!\tiny{}}\overline{a}b$ and $\Gamma_{1}\models_{r}\overline{a}b$, so $\overline{a}$ and $b$ are relevant for each other: $\Gamma_{1}$ has then models with $b={\bf 0}$, in which $a={\bf 0}$, and models with $a={\bf 1}$, in which $b={\bf 1}$. If $\Gamma_{1}\not\models_{r}\overline{a}b$ then $\overline{a}$ and $b$ would cease to be mutually relevant, since then either $\Gamma_{1}\models\overline{a}$ or $\Gamma\models_{r}b$, irrespectively of each other.

This relevance relation is not transitive. In

\textstyle{G=...d}$$\textstyle{a\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{b\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{c...}$$\textstyle{e...}

(with appropriate assumptions about the undisplayed part, e.g., all $...$ starting mutually disjoint infinite paths), $b$ is relevant for $a$, since $\Gamma\models_{r}\overline{ab}$, and $c$ is relevant for $b$ since $\Gamma\models_{r}\overline{bc}$. But $c$ is no longer relevant for $a$, because any value at $c$ can be accompanied by any value at $a$. However, $c\lor e$ is relevant for $a$, since $\Gamma\models_{r}\overline{a}ce$.

The relevant clauses are exactly the minimal provable ones: 666First, for each nonunit clause $C\in Min(\Gamma)$ and nonempty $B\subset C:\Gamma^{ok},B^{-}\not\vdash_{\!\!\!\tiny{}}\{\}$. This follows because, by Fact 4.6.(2), $\Gamma^{ok}\not\vdash_{\!\!\!\tiny{}}\{\}$ and then, by Fact 4.1.(6), $\Gamma^{ok},B^{-}\not\vdash_{\!\!\!\tiny{}}\{\}$ iff $\forall E\subseteq B:\Gamma^{ok}\not\vdash_{\!\!\!\tiny{}}E$, which holds since $C\in Min(\Gamma)$. The main claim is trivial for unit clauses. Assuming now a nonunit $AB=C\in Min(\Gamma)$, the observation above implies existence of a classical model of $\Gamma^{ok}$ (i.e., a model of $\Gamma$), satisfying $B^{-}$, so that $\Gamma\not\models B$. Since $\Gamma^{ok}\vdash_{\!\!\!\tiny{}}C$, so $\Gamma\vdash_{\!\!\!\tiny{}}C$ by Fact 4.6.(1), and hence $\Gamma\models C$ by soundness. So $C\in Min(\Gamma)\mathrel{\Rightarrow}\Gamma\models_{r}C$. Conversely, if for a nonunit $C:\Gamma\models_{r}C$, then $C\cap\ddot{G}^{\bot}=\emptyset$, so that $\Gamma^{ok}\models_{c}C$. Then $\Gamma^{ok}\vdash_{\!\!\!\tiny{}}B$ for some $B\subseteq C$ by Fact 4.6.(4). But since $\Gamma\not\models B$, for every $B\subset C$ so, by soudness, $\Gamma\not\vdash_{\!\!\!\tiny{}}B$, and hence $\Gamma^{ok}\not\vdash_{\!\!\!\tiny{}}B$ by 4.6.(1), so $\Gamma^{ok}\vdash_{\!\!\!\tiny{}}C$ and $C\in Min(\Gamma)$.

\begin{array}[]{rcl}Min(\Gamma)&=&\{C\mid\Gamma\vdash_{\!\!\!\tiny{}}C\land\forall B\subset C:B\not=\{\}\mathrel{\Rightarrow}\Gamma\not\vdash_{\!\!\!\tiny{}}B\}\\ &=&\{C\mid\Gamma^{ok}\vdash_{\!\!\!\tiny{}}C\land\forall B\subset C:\Gamma^{ok}\not\vdash_{\!\!\!\tiny{}}B\}\cup\bigcup\{\{a,\overline{a}\}\mid\Gamma\vdash_{\!\!\!\tiny{}}\bot(a)\}.\end{array}

Thus each RES provable clause $C$ represents a form of relevance. Even if $C\not\in Min(\Gamma)$, all its atoms belong to one component of the underlying graph and, moreover, there is some nonempty $D\subset C$ with $D\in Min(\Gamma)$, witnessing to the determination – in some occurring cases – of the truth-value of one part of each 2-partition of $D$ by the truth-value of the other.