On the strongest three-valued paraconsistent logic contained in classical logic and its dual

TL;DR

This paper investigates the unique properties of a specific three-valued paraconsistent logic within classical logic, distinguishing it from many others using logical equivalence properties, and explores its paracomplete analogue.

Contribution

It identifies the strongest three-valued paraconsistent logic contained in classical logic and characterizes its unique logical equivalence properties among 8192 such logics.

Findings

LP^{ ext{supset}, ext{F}} is uniquely distinguished by its logical equivalence relation.

Only 32 of 8192 three-valued paraconsistent logics satisfy key algebraic laws.

The paracomplete analogue of LP^{ ext{supset}, ext{F}} also exhibits comparable properties.

Abstract

LP$^{\supset,\mathsf{F}}$ is a three-valued paraconsistent propositional logic which is essentially the same as J3. It has most properties that have been proposed as desirable properties of a reasonable paraconsistent propositional logic. However, it follows easily from already published results that there are exactly 8192 different three-valued paraconsistent propositional logics that have the properties concerned. In this paper, properties concerning the logical equivalence relation of a logic are used to distinguish LP$^{\supset,\mathsf{F}}$ from the others. As one of the bonuses of focussing on the logical equivalence relation, it is found that only 32 of the 8192 logics have a logical equivalence relation that satisfies the identity, annihilation, idempotent, and commutative laws for conjunction and disjunction. For most properties of LP$^{\supset,\mathsf{F}}$ that have been proposed as desirable properties of a reasonable paraconsistent propositional logic, its paracomplete analogue has a comparable property. In this paper, properties concerning the logical equivalence relation of a logic are also used to distinguish the paracomplete analogue of LP$^{\supset,\mathsf{F}}$ from the other three-valued paracomplete propositional logics with those comparable properties.

Tables

Table 1. Table 1: Hilbert-style deductive system for LP ⊃ , 𝖥 superscript LP superset-of 𝖥 \mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}

Table 2. Table 2: Distinguishing laws of logical equivalence for LP ⊃ , 𝖥 superscript LP superset-of 𝖥 \mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}

Table 3. Table 3: Additional laws of logical equivalence for LP ⊃ , 𝖥 superscript LP superset-of 𝖥 \mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}

Equations

$$\nu (\mathsf{F})$$

$$\nu (\neg A)$$

$$\nu (A\wedge B)$$

$$\nu (A\vee B)$$

$$\nu (A\supset B)$$

$$\begin{array}[]{@{}c@{}}\begin{array}[t]{@{}l@{}}\mathbin{\tilde{\land}}({\mathsf{t}},{\mathsf{t}})={\mathsf{t}}\;,\\ \mathbin{\tilde{\land}}({\mathsf{f}},b)={\mathsf{f}}\;,\\ \mathbin{\tilde{\land}}(b,{\mathsf{f}})={\mathsf{f}}\;,\\ \mathbin{\tilde{\land}}({\mathsf{\star}},{\mathsf{t}})\in\{{\mathsf{t}},{\mathsf{\star}}\}\;,\\ \mathbin{\tilde{\land}}({\mathsf{t}},{\mathsf{\star}})\in\{{\mathsf{t}},{\mathsf{\star}}\}\;,\\ \mathbin{\tilde{\land}}({\mathsf{\star}},{\mathsf{\star}})\in\{{\mathsf{t}},{\mathsf{\star}}\}\;,\\[1.29167pt] \end{array}\qquad\begin{array}[t]{@{}l@{}}\mathbin{\tilde{\lor}}({\mathsf{t}},{\mathsf{t}})={\mathsf{t}}\;,\\ \mathbin{\tilde{\lor}}({\mathsf{f}},{\mathsf{t}})={\mathsf{t}}\;,\\ \mathbin{\tilde{\lor}}({\mathsf{t}},{\mathsf{f}})={\mathsf{t}}\;,\\ \mathbin{\tilde{\lor}}({\mathsf{f}},{\mathsf{f}})={\mathsf{f}}\;,\\ \mathbin{\tilde{\lor}}({\mathsf{\star}},b)\in\{{\mathsf{t}},{\mathsf{\star}}\}\;,\\ \mathbin{\tilde{\lor}}(b,{\mathsf{\star}})\in\{{\mathsf{t}},{\mathsf{\star}}\}\;,\\[1.29167pt] \end{array}\qquad\begin{array}[t]{@{}l@{}}\mathbin{\tilde{\supset}}({\mathsf{t}},{\mathsf{t}})={\mathsf{t}}\;,\\ \mathbin{\tilde{\supset}}({\mathsf{f}},{\mathsf{t}})={\mathsf{t}}\;,\\ \mathbin{\tilde{\supset}}({\mathsf{t}},{\mathsf{f}})={\mathsf{f}}\;,\\ \mathbin{\tilde{\supset}}({\mathsf{f}},{\mathsf{f}})={\mathsf{t}}\;,\\ \mathbin{\tilde{\supset}}({\mathsf{\star}},{\mathsf{f}})={\mathsf{f}}\;,\\ \mathbin{\tilde{\supset}}({\mathsf{\star}},{\mathsf{t}})\in\{{\mathsf{t}},{\mathsf{\star}}\}\;,\\ \mathbin{\tilde{\supset}}(b,{\mathsf{\star}})\in\{{\mathsf{t}},{\mathsf{\star}}\}\;,\\[1.29167pt] \end{array}\qquad\begin{array}[t]{@{}l@{}}\mathbin{\tilde{\lnot}}({\mathsf{t}})={\mathsf{f}}\;,\\ \mathbin{\tilde{\lnot}}({\mathsf{f}})={\mathsf{t}}\;,\\ \mathbin{\tilde{\lnot}}({\mathsf{\star}})\in\{{\mathsf{t}},{\mathsf{\star}}\}\;.\\[1.29167pt] \end{array}\end{array}$$

$$\begin{array}[]{@{}c@{}}\begin{tabular}[]{l}$\tilde{\diamond}(b,{\mathsf{\star}})\neq{\mathsf{f}}$ iff $\tilde{\diamond}(b,{\mathsf{t}})={\mathsf{t}}$,\\ $\tilde{\diamond}({\mathsf{\star}},b)\neq{\mathsf{f}}$ iff $\tilde{\diamond}({\mathsf{t}},b)={\mathsf{t}}$,\\ $\tilde{\diamond}({\mathsf{\star}},{\mathsf{\star}})\neq{\mathsf{f}}$ iff $\tilde{\diamond}({\mathsf{t}},{\mathsf{t}})={\mathsf{t}}$;\end{tabular}\end{array}$$

$$\begin{array}[]{@{}l@{}}(25)\;\;A\land\lnot A\Leftrightarrow{\mathsf{F}}\qquad\;(26)\;\;A\lor\lnot A\Leftrightarrow{\mathsf{T}}\qquad\;(27)\;\;A\mathbin{\supset}B\Leftrightarrow\lnot A\lor B\;.\end{array}$$

$$\nu (A\supset B)$$

$$\begin{array}[]{@{}l@{}}A\mathrel{\vDash_{\mathrm{CL}}}B\;\;\mathrm{iff}\;\;A\mathrel{\vDash}B\lor\iota(A)\\ \phantom{A\mathrel{\vDash_{\mathrm{CL}}}B\;}\mathrm{and}\\ A\mathrel{\vDash_{\mathrm{CL}}}B\;\;\mathrm{iff}\;\;A\land\delta(B)\mathrel{\vDash}^{\star}B\;.\end{array}$$

$$\begin{array}[]{@{}c@{}}\begin{array}[t]{@{}l@{}}\mathbin{\tilde{\land}}({\mathsf{t}},{\mathsf{t}})={\mathsf{t}}\;,\\ \mathbin{\tilde{\land}}({\mathsf{f}},{\mathsf{t}})={\mathsf{f}}\;,\\ \mathbin{\tilde{\land}}({\mathsf{t}},{\mathsf{f}})={\mathsf{f}}\;,\\ \mathbin{\tilde{\land}}({\mathsf{f}},{\mathsf{f}})={\mathsf{f}}\;,\\ \mathbin{\tilde{\land}}({\mathsf{\star}},b)\in\{{\mathsf{f}},{\mathsf{\star}}\}\;,\\ \mathbin{\tilde{\land}}(b,{\mathsf{\star}})\in\{{\mathsf{f}},{\mathsf{\star}}\}\;,\\[1.29167pt] \end{array}\qquad\begin{array}[t]{@{}l@{}}\mathbin{\tilde{\lor}}({\mathsf{t}},b)={\mathsf{t}}\;,\\ \mathbin{\tilde{\lor}}(b,{\mathsf{t}})={\mathsf{t}}\;,\\ \mathbin{\tilde{\lor}}({\mathsf{f}},{\mathsf{f}})={\mathsf{f}}\;,\\ \mathbin{\tilde{\lor}}({\mathsf{\star}},{\mathsf{f}})\in\{{\mathsf{f}},{\mathsf{\star}}\}\;,\\ \mathbin{\tilde{\lor}}({\mathsf{f}},{\mathsf{\star}})\in\{{\mathsf{f}},{\mathsf{\star}}\}\;,\\ \mathbin{\tilde{\lor}}({\mathsf{\star}},{\mathsf{\star}})\in\{{\mathsf{f}},{\mathsf{\star}}\}\;,\\[1.29167pt] \end{array}\qquad\begin{array}[t]{@{}l@{}}\mathbin{\tilde{\supset}}({\mathsf{t}},{\mathsf{t}})={\mathsf{t}}\;,\\ \mathbin{\tilde{\supset}}({\mathsf{t}},{\mathsf{f}})={\mathsf{f}}\;,\\ \mathbin{\tilde{\supset}}({\mathsf{f}},b)={\mathsf{t}}\;,\\ \mathbin{\tilde{\supset}}({\mathsf{\star}},b)={\mathsf{t}}\;,\\ \mathbin{\tilde{\supset}}({\mathsf{t}},{\mathsf{\star}})\in\{{\mathsf{f}},{\mathsf{\star}}\}\;,\\[1.29167pt] \end{array}\qquad\begin{array}[t]{@{}l@{}}\mathbin{\tilde{\lnot}}({\mathsf{t}})={\mathsf{f}}\;,\\ \mathbin{\tilde{\lnot}}({\mathsf{f}})={\mathsf{t}}\;,\\ \mathbin{\tilde{\lnot}}({\mathsf{\star}})\in\{{\mathsf{f}},{\mathsf{\star}}\}\;.\\[1.29167pt] \end{array}\end{array}$$

$$\begin{array}[]{@{}c@{}}\begin{tabular}[]{l}$\nu(A\land B)={\mathsf{t}}$ iff $\nu(A)={\mathsf{t}}$ and $\nu(B)={\mathsf{t}}$,\\ $\nu(A\lor B)={\mathsf{t}}$ iff $\nu(A)={\mathsf{t}}$ or $\nu(B)={\mathsf{t}}$,\\ $\nu(A\mathbin{\supset}B)={\mathsf{t}}$ iff $\nu(A)\neq{\mathsf{t}}$ or $\nu(B)={\mathsf{t}}$,\\ $\nu(\lnot A)={\mathsf{t}}$\phantom{$\;B\;$} iff $\nu(A)\neq{\mathsf{t}}$ and $\nu(A)\neq{\mathsf{\star}}$.\end{tabular}\end{array}$$

$$\begin{array}[]{@{}c@{}}\begin{tabular}[]{l}$\nu(\lnot A)={\mathsf{t}}$ iff $\nu(A)\neq{\mathsf{t}}$ and $\nu(A)\neq{\mathsf{\star}}$ $\quad$ by $\quad$ $\nu(\lnot A)={\mathsf{t}}$ iff $\nu(A)\neq{\mathsf{t}}$.\end{tabular}\end{array}$$

$$\begin{array}[]{@{}c@{}}\begin{tabular}[]{l}$\mathbin{\tilde{\lnot}}({\mathsf{\star}})\in\{{\mathsf{f}},{\mathsf{\star}}\}$ $\quad$ by $\quad$ $\mathbin{\tilde{\lnot}}({\mathsf{\star}})\in\{{\mathsf{t}},{\mathsf{f}},{\mathsf{\star}}\}$.\end{tabular}\end{array}$$

$$\begin{array}[]{@{}c@{}}\begin{tabular}[]{l}$\tilde{\diamond}(b,{\mathsf{\star}})\neq{\mathsf{t}}$ iff $\tilde{\diamond}(b,{\mathsf{f}})={\mathsf{f}}$,\\ $\tilde{\diamond}({\mathsf{\star}},b)\neq{\mathsf{t}}$ iff $\tilde{\diamond}({\mathsf{f}},b)={\mathsf{f}}$,\\ $\tilde{\diamond}({\mathsf{\star}},{\mathsf{\star}})\neq{\mathsf{t}}$ iff $\tilde{\diamond}({\mathsf{f}},{\mathsf{f}})={\mathsf{f}}$;\end{tabular}\end{array}$$

Full text

1 Introduction

A set of propositions is contradictory if there exists a proposition such that both that proposition and the negation of that proposition are logical consequences of it. In classical propositional logic, every proposition is a logical consequence of every contradictory set of propositions. In a paraconsistent propositional logic, this is not the case.

$\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$ is the three-valued paraconsistent propositional logic LP [23] enriched with an implication connective for which the standard deduction theorem holds and a falsity constant. This logic, which is essentially the same as J3 [17], the propositional fragment of CLuNs [7] without bi-implication, and LFI1 [13], has most properties that have been proposed as desirable properties of a reasonable paraconsistent propositional logic. However, it follows easily from results presented in [1, 2, 13] that there are exactly 8192 different three-valued paraconsistent propositional logics that have the properties concerned. In this paper, properties concerning the logical equivalence relation of a logic are used to distinguish $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$ from the others.

It turns out that only 32 of those 8192 logics are logics of which the logical equivalence relation satisfies the identity, annihilation, idempotent, and commutative laws for conjunction and disjunction; and only 16 of them are logics of which the logical equivalence relation additionally satisfies the double negation law. $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$ is one of those 16 logics. Two additional classical laws of logical equivalence turn out to be sufficient to distinguish $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$ completely from the others.

The desirable properties of a reasonable paraconsistent propositional logic referred to above concern the logical consequence relation of a logic. It does not follow from those properties that the identity, annihilation, idempotent, and commutative laws for conjunction and disjunction are satisfied by the logical equivalence relation of the logic. Therefore, if closeness to classical propositional logic is considered important, it should be a desirable property of a reasonable paraconsistent propositional logic to have a logical equivalence relation that satisfies these classical laws of logical equivalence. This would reduce the potentially interesting three-valued paraconsistent propositional logics from 8192 to 32.

The dual notion of paraconsistency is paracompleteness. A paracomplete propositional logic is a propositional logic in which not every disjunction of a proposition and the negation of that proposition is a logical consequence of every set of propositions. I have coined the name $\mathrm{K3}^{\mathbin{\supset},{\mathsf{F}}}$ for the paracomplete analogue of $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$. This logic is considered to be the dual of $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$. For most properties of $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$ that have been proposed as desirable properties of a reasonable paraconsistent propositional logic, $\mathrm{K3}^{\mathbin{\supset},{\mathsf{F}}}$ has a comparable property. Those comparable properties are properties that any reasonable paracomplete propositional logic should have. In this paper, properties concerning the logical equivalence relation of a logic are also used to distinguish $\mathrm{K3}^{\mathbin{\supset},{\mathsf{F}}}$ from other three-valued paracomplete propositional logics with those comparable properties.

$\mathrm{K3}^{\mathbin{\supset},{\mathsf{F}}}$ is essentially the same as the propositional fragment of LPF [6, 15] without the constant that represents the truth value that is interpreted as neither true nor false. That is, LPF has a definedness connective, $\mathrm{\Delta}$, instead of the implication connective of $\mathrm{K3}^{\mathbin{\supset},{\mathsf{F}}}$, but these connectives can be defined in terms of each other (see e.g. Section 3.1.2 of [4]). LPF is well-known in the area of formal methods for software development. It is basic to formal specification and verified design in the software development method VDM [19].

In [10], a process algebra is presented that allows for dealing with contradictory states. In order to allow for this, the process algebra concerned is built on $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$. During the search for a paraconsistent propositional logic on which such a process algebra can be built, satisfaction of certain classical laws of logical equivalence turned out to be essential. $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$ is one of only four three-valued paraconsistent propositional logics with all of the desirable properties referred to above of which the logical equivalence relation satisfies the classical laws concerned. This finding triggered the more elaborate work on the logical equivalence relations of three-valued paraconsistent propositional logics presented in the current paper.

The structure of this paper is as follows. First, a survey of the paraconsistent propositional logic $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$ is given (Section 2). Next, the known properties of $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$ that have been proposed as desirable properties of a reasonable paraconsistent propositional logic are discussed (Section 3). Then, properties concerning the logical equivalence relation of a logic are used to distinguish $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$ from the other three-valued paraconsistent propositional logics with the properties discussed earlier (Section 4). After that, the logical equivalence relation of $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$ is examined further and its key role in the algebraization of $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$ is shown (Section 5). Thereafter, $\mathrm{K3}^{\mathbin{\supset},{\mathsf{F}}}$ is introduced (Section 6) and properties of $\mathrm{K3}^{\mathbin{\supset},{\mathsf{F}}}$ are presented that are comparable to properties of $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$ that have been presented in the preceding sections (Section 7). Finally, some concluding remarks are made (Section 8).

It is relevant to realize that the work presented in this paper is restricted to three-valued paraconsistent propositional logics that are truth-functional three-valued logics.

There is some overlap between this paper and [10]. This paper primarily generalizes and elaborates Section 2 of that paper in such a way that it may be of independent importance to the area of paraconsistent logics.

2 The Paraconsistent Logic $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$

A set of propositions $\Gamma$ is contradictory if there exists a proposition $A$ such that both $A$ and $\lnot A$ is a logical consequence of $\Gamma$. In classical propositional logic, every proposition is a logical consequence of a contradictory set of propositions. Informally, a paraconsistent propositional logic is a propositional logic in which not every proposition is a logical consequence of every contradictory set of propositions.

More precisely, a propositional logic $\mathcal{L}$ is a paraconsistent propositional logic if (a) its logical consequence relation $\mathrel{\vDash}_{\mathcal{L}}$ satisfies the condition that there exist formulas $A$ and $B$ of $\mathcal{L}$ such that $A,\lnot A\mathrel{\not{\!\vDash}}_{\mathcal{L}}B$ and (b) its negation connective $\lnot$ satisfies the condition that, for each propositional variable $p$, both $p\mathrel{\not{\!\vDash}}_{\mathcal{L}}\lnot p$ and $\lnot p\mathrel{\not{\!\vDash}}_{\mathcal{L}}p$.

In [23], Priest proposed the paraconsistent propositional logic LP (Logic of Paradox). The logic introduced in this section is LP enriched with a falsity constant and an implication connective for which the standard deduction theorem holds. This logic, called $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$, is in fact the propositional fragment of CLuNs [7] without bi-implications.

$\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$ has the following logical constants and connectives: a falsity constant ${\mathsf{F}}$, a unary negation connective $\lnot$, a binary conjunction connective $\land$, a binary disjunction connective $\lor$, and a binary implication connective $\mathbin{\supset}$. Truth and bi-implication are defined as abbreviations: ${\mathsf{T}}$ stands for $\lnot{\mathsf{F}}$ and $A\mathbin{\equiv}B$ stands for $(A\mathbin{\supset}B)\land(B\mathbin{\supset}A)$.

A Hilbert-style deductive system for $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$ is given in Table 1.

In this table, $A$, $B$, and $C$ are used as meta-variables ranging over the set of all formulas of $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$. This deductive system is obtained by adding the axiom schema ${\mathsf{F}}\mathbin{\supset}A$ to the Hilbert-style deductive system of Pac given in [4] on page 288. The axiom schemas on the left-hand side of the table, except for ${\mathsf{F}}\mathbin{\supset}A$, together with the single inference rule (modus ponens) constitute a Hilbert-style deductive system for the positive fragment of classical propositional logic. On the right-hand side of the table, the first three axiom schemas allow for the negation connective to be moved inwards, the fourth axiom schema is the double negation axiom schema, and the fifth axiom schema is the law of the excluded middle. The last-mentioned axiom can be thought of as saying that, for every proposition, the proposition or its negation is true, while leaving open the possibility that both are true. Replacement of this axiom schema by $(A\mathbin{\supset}\lnot A)\mathbin{\supset}\lnot A$, as in CLuNs [7], yields an equivalent deductive system for $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$. Addition of the axiom schema $\lnot A\mathbin{\supset}(A\mathbin{\supset}B)$, which says that any proposition follows from a contradiction, yields a Hilbert-style deductive system for classical propositional logic (see e.g. [4]). The symbol $\mathrel{\vdash}$ without decoration is used to denote the derivability relation induced by the axiom schemas and inference rule of the given deductive system for $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$.

The following outline of the semantics of $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$ is based on [4]. Like in the case of classical propositional logic, meanings are assigned to the formulas of $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$ by means of valuations. However, in addition to the two classical truth values ${\mathsf{t}}$ (true) and ${\mathsf{f}}$ (false), a third meaning ${\mathsf{\star}}$ (both true and false) may be assigned. A valuation for $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$ is a function $\nu$ from the set of all formulas of $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$ to the set $\{{\mathsf{t}},{\mathsf{f}},{\mathsf{\star}}\}$ such that for all formulas $A$ and $B$ of $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$:

[TABLE]

The classical truth-conditions and falsehood-conditions for the logical connectives are retained. Except for implications, a formula is classified as both-true-and-false exactly when it cannot be classified as true or false by the classical truth-conditions and falsehood-conditions. Implications deviate in order to satisfy the standard deduction theorem. The definition of a valuation given above shows that the logical connectives of $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$ are (three-valued) truth-functional, which means that each $n$-ary connective represents a function from $\{{\mathsf{t}},{\mathsf{f}},{\mathsf{\star}}\}^{n}$ to $\{{\mathsf{t}},{\mathsf{f}},{\mathsf{\star}}\}$.

For $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$, the logical consequence relation, denoted by $\mathrel{\vDash}$, is based on the idea that a valuation $\nu$ satisfies a formula $A$ if $\nu(A)\in\{{\mathsf{t}},{\mathsf{\star}}\}$. It is defined as follows: $\Gamma\mathrel{\vDash}A$ iff for every valuation $\nu$, either $\nu(A^{\prime})={\mathsf{f}}$ for some $A^{\prime}\in\Gamma$ or $\nu(A)\in\{{\mathsf{t}},{\mathsf{\star}}\}$. The given Hilbert-style deductive system for $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$ is sound and strongly complete with respect to the semantics of $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$, i.e. $\Gamma\mathrel{\vdash}A$ iff $\Gamma\mathrel{\vDash}A$. This follows immediately from Theorems 1, 2, and 3 in [7].

For all formulas $A$ of $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$ in which ${\mathsf{F}}$ does not occur, for all formulas $B$ of $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$ in which no propositional variable occurs that occurs in $A$,  $A,\lnot A\mathrel{\not{\!\vDash}}B$ if $\mathrel{\not{\!\vDash}}B$ (cf. Proposition 4.37 in [1]).111On the left-hand side of $\mathrel{\vDash}$, we write $A$ for $\{A\}$ and $\Gamma,\Delta$ for $\Gamma\cup\Delta$. Moreover, we leave out the left-hand side if it is $\emptyset$. We also write $\Gamma\mathrel{\not{\!\vDash}}A$ for not $\Gamma\mathrel{\vDash}A$. Moreover, the connective $\lnot$ satisfies the condition that, for each propositional variable $p$, both $p\mathrel{\not{\!\vDash}}\lnot p$ and $\lnot p\mathrel{\not{\!\vDash}}p$. Hence, $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$ is a paraconsistent logic.

The logical equivalence relation $\Leftrightarrow$ of $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$ is defined as it is defined for classical propositional logic: $A\Leftrightarrow B$ iff for every valuation $\nu$, $\nu(A)=\nu(B)$. Consistency of a formula of $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$ is defined as follows: $A$ is consistent iff for every valuation $\nu$, $\nu(A)\neq{\mathsf{\star}}$.

Unlike in classical propositional logic, it is not the case that $A\Leftrightarrow B$ iff $\mathrel{\vDash}A\mathbin{\equiv}B$. Take, for example, $p\lor\lnot p$ for $A$ and $q\lor\lnot q$ for $B$, where $p$ and $q$ are different propositional variables. Clearly, ${}\mathrel{\vDash}p\lor\lnot p\mathbin{\equiv}q\lor\lnot q$. Now, let $\nu$ be a valuation such that $\nu(p)={\mathsf{t}}$ and $\nu(q)={\mathsf{\star}}$. Then $\nu(p\lor\lnot p)={\mathsf{t}}$ and $\nu(q\lor\lnot q)={\mathsf{\star}}$ and consequently it is not the case that $p\lor\lnot p\Leftrightarrow q\lor\lnot q$. However, it is easy to check that $A\Leftrightarrow B$ only if ${}\mathrel{\vDash}A\mathbin{\equiv}B$.

3 Known Properties of $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$

In this section, the known properties of $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$ that have been proposed as desirable properties of a reasonable paraconsistent propositional logic are presented. Each of the properties in question has to do with logical consequence relations. The name CL is used to denote a version of classical propositional logic that has the same logical constants and connectives as $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$. The symbol $\mathrel{\vDash_{\mathrm{CL}}}$ is used to denote the logical consequence relation of CL.

The known properties of $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$ that have been proposed as desirable properties of a reasonable paraconsistent propositional logic are:

• (a)

containment in classical logic: ${\mathrel{\vDash}}\subseteq{\mathrel{\vDash_{\mathrm{CL}}}}$;

• (b)

proper basic connectives: for all sets $\Gamma$ of formulas of $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$ and all formulas $A$, $B$, and $C$ of $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$:

• (b1)

\Gamma,A\mathrel{\vDash}B$${}\land{}$$C iff $\Gamma\mathrel{\vDash}A\mathbin{\supset}B$,

• (b2)

$\Gamma\mathrel{\vDash}A\land B$,$C$ iff $\Gamma\mathrel{\vDash}A$ and $\Gamma\mathrel{\vDash}B$,

• (b3)

$\Gamma,A\lor B\mathrel{\vDash}C$ iff $\Gamma,A\mathrel{\vDash}C$ and $\Gamma,B\mathrel{\vDash}C$;

• (c)

weak maximal paraconsistency relative to classical logic: for all formulas $A$ of $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$ with $\mathrel{\not{\!\vDash}}A$ and $\mathrel{\vDash_{\mathrm{CL}}}A$, for the minimal consequence relation $\mathrel{\vDash^{\prime}}$ such that ${\mathrel{\vDash}}\subseteq{\mathrel{\vDash^{\prime}}}$ and $\mathrel{\vDash^{\prime}}A$, for all formulas $B$ of $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$, $\mathrel{\vDash^{\prime}}B$ iff $\mathrel{\vDash_{\mathrm{CL}}}B$;

• (d)

strongly maximal absolute paraconsistency: for all propositional logics $\mathcal{L}$ with the same logical constants and connectives as $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$ and a consequence relation $\mathrel{\vDash^{\prime}}$ such that ${\mathrel{\vDash}}\subset{\mathrel{\vDash^{\prime}}}$, $\mathcal{L}$ is not paraconsistent;

• (e)

internalized notion of consistency: $A$ is consistent iff ${}\mathrel{\vDash}(A\mathbin{\supset}{\mathsf{F}})\lor(\lnot A\mathbin{\supset}{\mathsf{F}})$;

• (f)

internalized notion of logical equivalence: $A\Leftrightarrow B$ iff ${}\mathrel{\vDash}(A\mathbin{\equiv}B)\land(\lnot A\mathbin{\equiv}\lnot B)$.

Properties (a)–(f) have been mentioned relatively often in the literature (see e.g. [1, 2, 3, 5, 7, 13]). Properties (a), (b1), (c), and (d) make $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$ an ideal paraconsistent logic in the sense made precise in [2]. By property (e), $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$ is also a logic of formal inconsistency according to Definition 23 in [13].222The set of formulas $\bigcirc(p)$ witnessing this is $\{(p\mathbin{\supset}{\mathsf{F}})\lor(\lnot p\mathbin{\supset}{\mathsf{F}})\}$.

Properties (a)–(c) indicate that $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$ retains much of classical propositional logic. In [10], properties (e) and (f) are considered desirable and essential, respectively, for a paraconsistent propositional logic on which a process algebra that allows for dealing with contradictory states is built.

From Theorem 4.42 in [1], it is known that there are exactly 8192 different three-valued paraconsistent propositional logics with properties (a) and (b). From Theorem 2 in [2], it is known that properties (c) and (d) are common properties of all three-valued paraconsistent propositional logics with properties (a) and (b1). From Fact 103 in [13], it is known that property (f) is a common property of all three-valued paraconsistent propositional logics with properties (a), (b) and (e). Moreover, it is easy to see that property (e) is a common property of all three-valued paraconsistent propositional logics with properties (a) and (b). Hence, each three-valued paraconsistent propositional logic with properties (a) and (b) has properties (c)–(f) as well.

From Corollary 4.74 in [1], it is known that $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$ is the strongest three-valued paraconsistent propositional logic with property (a) in the sense that each three-valued paraconsistent propositional logic with property (a) can be embedded in $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$.

4 Characterizing $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$ by Laws of Logical Equivalence

There are exactly 8192 different three-valued paraconsistent propositional logics with properties (a) and (b). This means that these properties, which concern the logical consequence relation of a logic, have little discriminating power. Properties (c)–(f), which also concern the logical consequence relation of a logic, do not offer additional discrimination because each of the 8192 three-valued paraconsistent propositional logics with properties (a) and (b) has these properties as well.

In this section, properties concerning the logical equivalence relation of a logic are used for additional discrimination. It turns out that 11 classical laws of logical equivalence, of which at least 9 are considered to belong to the most basic ones, are sufficient to distinguish $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$ completely from the other 8191 three-valued paraconsistent propositional logics with properties (a) and (b).

The logical equivalence relation of $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$ satisfies all laws given in Table 2.

Theorem 4.1

The logical equivalence relation of $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$ satisfies laws (1)–(11) from Table 2.

Proof

The proof is easy by constructing, for each of the laws concerned, truth tables for both sides. ∎

Moreover, among the 8192 three-valued paraconsistent propositional logics with properties (a) and (b), $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$ is the only one whose logical equivalence relation satisfies all laws given in Table 2.

Theorem 4.2

There is exactly one three-valued paraconsistent propositional logic with properties (a) and (b) of which the logical equivalence relation satisfies laws (1)–(11) from Table 2.

Proof

From Theorem 4.42 in [1], it is known that the 8192 three-valued paraconsistent propositional logics with properties (a) and (b) are induced by a matrix of which the set of truth values is $\{{\mathsf{t}},{\mathsf{f}},{\mathsf{\star}}\}$, the set of designated values is $\{{\mathsf{t}},{\mathsf{\star}}\}$, and the functions $\mathbin{\tilde{\land}}$, $\mathbin{\tilde{\lor}}$, $\mathbin{\tilde{\supset}}$, and $\mathbin{\tilde{\lnot}}$ on the set of truth values that correspond to the connectives $\land$, $\lor$, $\mathbin{\supset}$, and $\lnot$, respectively, are such that, for each $b\in\{{\mathsf{t}},{\mathsf{f}},{\mathsf{\star}}\}$:

[TABLE]

So, there are 8 alternatives for $\mathbin{\tilde{\land}}$, 32 alternatives for $\mathbin{\tilde{\lor}}$, 16 alternatives for $\mathbin{\tilde{\supset}}$, and 2 alternatives for $\mathbin{\tilde{\lnot}}$. Below, it will be shown that, for each of these functions, laws from Table 2 exclude all but one alternative.

Law (3) excludes $\mathbin{\tilde{\land}}({\mathsf{\star}},{\mathsf{t}})={\mathsf{t}}$, law (5) excludes $\mathbin{\tilde{\land}}({\mathsf{\star}},{\mathsf{\star}})={\mathsf{t}}$, and law (7) excludes $\mathbin{\tilde{\land}}({\mathsf{t}},{\mathsf{\star}})={\mathsf{t}}$. Hence, there is only one of the 8 alternatives for $\mathbin{\tilde{\land}}$ left. Law (2) excludes $\mathbin{\tilde{\lor}}({\mathsf{\star}},{\mathsf{t}})={\mathsf{\star}}$, law (4) excludes $\mathbin{\tilde{\lor}}({\mathsf{\star}},{\mathsf{f}})={\mathsf{t}}$, law (6) excludes $\mathbin{\tilde{\lor}}({\mathsf{\star}},{\mathsf{\star}})={\mathsf{t}}$, and law (8) excludes $\mathbin{\tilde{\lor}}({\mathsf{t}},{\mathsf{\star}})={\mathsf{\star}}$ and $\mathbin{\tilde{\lor}}({\mathsf{f}},{\mathsf{\star}})={\mathsf{t}}$. Hence, there is only one of the 32 alternatives for $\mathbin{\tilde{\lor}}$ left. Law (9) excludes $\mathbin{\tilde{\lnot}}({\mathsf{\star}})={\mathsf{t}}$. Hence, there is only one of the 2 alternatives for $\mathbin{\tilde{\lnot}}$ left. Law (10) excludes $\mathbin{\tilde{\supset}}({\mathsf{f}},{\mathsf{\star}})={\mathsf{\star}}$ and law (11) excludes $\mathbin{\tilde{\supset}}({\mathsf{\star}},{\mathsf{t}})={\mathsf{\star}}$, $\mathbin{\tilde{\supset}}({\mathsf{t}},{\mathsf{\star}})={\mathsf{t}}$, and $\mathbin{\tilde{\supset}}({\mathsf{\star}},{\mathsf{\star}})={\mathsf{t}}$ (in the case of the alternatives left for $\mathbin{\tilde{\lor}}$ and $\mathbin{\tilde{\lnot}}$). Hence, there is only one of the 16 alternatives for $\mathbin{\tilde{\supset}}$ left. ∎

The following is a clarifying reformulation of the conditions on the functions $\mathbin{\tilde{\land}}$, $\mathbin{\tilde{\lor}}$, $\mathbin{\tilde{\supset}}$, and $\mathbin{\tilde{\lnot}}$ of the matrices from the proof of Theorem 4.2:

• •

for each $\tilde{\diamond}\in\{\mathbin{\tilde{\land}},\mathbin{\tilde{\lor}},\mathbin{\tilde{\supset}},\mathbin{\tilde{\lnot}}\}$, the restriction of $\tilde{\diamond}$ to $\{{\mathsf{t}},{\mathsf{f}}\}$ is $\tilde{\diamond}$ from the matrix for classical propositional logic;

• •

for each $\tilde{\diamond}\in\{\mathbin{\tilde{\land}},\mathbin{\tilde{\lor}},\mathbin{\tilde{\supset}}\}$, for each $b\in\{{\mathsf{t}},{\mathsf{f}}\}$:

[TABLE]

• •

$\mathbin{\tilde{\lnot}}({\mathsf{\star}})\neq{\mathsf{f}}$.

This reformulation shows clearly that ${\mathsf{\star}}$ is just an alternative for ${\mathsf{t}}$ in the cases of $\mathbin{\tilde{\land}}$, $\mathbin{\tilde{\lor}}$, and $\mathbin{\tilde{\supset}}$, but not in the case of $\mathbin{\tilde{\lnot}}$.

It follows immediately from the proof of Theorem 4.2 that all proper subsets of laws (2)–(11) from Table 2 are insufficient to distinguish $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$ completely from the other three-valued paraconsistent propositional logics with properties (a) and (b). Notice that the logical equivalence relation of every three-valued paraconsistent propositional logics with properties (a) and (b) satisfies law (1) from Table 2. The next two corollaries also follow immediately from the proof of Theorem 4.2.

Corollary 1

There are exactly 16 three-valued paraconsistent propositional logics with properties (a) and (b) of which the logical equivalence relation satisfies laws (1)–(9) from Table 2.

Corollary 2

There are exactly 32 three-valued paraconsistent propositional logics with properties (a) and (b) of which the logical equivalence relation satisfies laws (1)–(8) from Table 2.

From a paraconsistent propositional logic with properties (a) and (b), it is only to be expected, because of paraconsistency and property (b1), that its negation connective and its implication connective deviate clearly from their counterpart in classical propositional logic. Corollary 2 shows that, among the 8192 three-valued paraconsistent propositional logics with properties (a) and (b), there are 8160 logics whose logical equivalence relation does not satisfy the identity, annihilation, idempotent, and commutative laws for conjunction and disjunction (laws (1)–(8) from Table 2).

5 More on the Logical Equivalence Relation of $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$

It turns out that the logical equivalence relation of $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$ does not only satisfy the identity, annihilation, idempotent, and commutative laws for conjunction and disjunction but also other basic classical laws for conjunction and disjunction, including the absorption, associative, distributive, and de Morgan’s laws. Actually, the logical equivalence relation of $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$ also satisfies all laws given in Table 3.

Theorem 5.1

The logical equivalence relation of $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$ satisfies laws (12)–(24) from Table 3.

Proof

The proof is straightforward by constructing, for each of the laws concerned, truth tables for both sides. ∎

Laws (1)–(9) and (12)–(21) axiomatize bounded normal i-lattices [20].333Bounded normal i-lattices are also (confusingly) called Kleene algebras (see e.g. [12]). Laws (10)–(11) and (22)–(24) are laws concerning the implication connective. Laws (10)–(11) and (22)–(24), like laws (1)–(9) and (12)–(21), are also satisfied by the logical equivalence relation of classical propositional logic. For all formulas $A^{\prime}$ and $A^{\prime\prime}$ of classical propositional logic, the logical equivalence relation of classical propositional logic satisfies $A^{\prime}\Leftrightarrow A^{\prime\prime}$ iff $A^{\prime}\Leftrightarrow A^{\prime\prime}$ follows from laws (1)–(9) and (12)–(21) and the laws

[TABLE]

However, laws (25)–(27) are not satisfied by the logical equivalence relation of $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$.

The fact that $A\Leftrightarrow B$ iff ${}\mathrel{\vDash}(A\mathbin{\equiv}B)\land(\lnot A\mathbin{\equiv}\lnot B)$ suggests that $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$ is Blok-Pigozzi algebraizable [11].

Theorem 5.2

$\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$* is finitely Blok-Pigozzi algebraizable with the equivalence formulas $\{p\mathbin{\supset}q,q\mathbin{\supset}p,\lnot p\mathbin{\supset}\lnot q,\lnot q\mathbin{\supset}\lnot p\}$ and the single defining equation $p=p\lor\lnot p$ ($p$ and $q$ are propositional variables).*

Proof

Because $A\Leftrightarrow B$ iff $\,\mathrel{\vDash}(A\mathbin{\equiv}B)\land(\lnot A\mathbin{\equiv}\lnot B)$, $A\mathbin{\equiv}B$ stands for $(A\mathbin{\supset}B)\land\linebreak[2](B\mathbin{\supset}A)$, and $\mathrel{\vDash}A\land B$ iff $\mathrel{\vDash}A$ and $\mathrel{\vDash}B$, it is the case that $A\Leftrightarrow B$ iff $\mathrel{\vDash}A\mathbin{\supset}B$ and $\mathrel{\vDash}B\mathbin{\supset}A$ and $\mathrel{\vDash}\lnot A\mathbin{\supset}\lnot B$ and $\mathrel{\vDash}\lnot B\mathbin{\supset}\lnot A$. Moreover, writing $A\mathbin{\leftrightarrow}B$ for $(A\mathbin{\equiv}B)\land(\lnot A\mathbin{\equiv}\lnot B)$, it is easily found that (i) $\mathrel{\vDash}A\mathbin{\leftrightarrow}A$, (ii) $A,A\mathbin{\leftrightarrow}B\mathrel{\vDash}B$, (iii) $A\mathbin{\leftrightarrow}B\mathrel{\vDash}\lnot A\mathbin{\leftrightarrow}\lnot B$, (iv) $A\mathbin{\leftrightarrow}B,A^{\prime}\mathbin{\leftrightarrow}B^{\prime}\mathrel{\vDash}A\diamond A^{\prime}\mathbin{\leftrightarrow}B\diamond B^{\prime}$ for $\diamond\in\{\land,\lor,\mathbin{\supset}\}$, and (v) $A\mathrel{\vDash}A\mathbin{\leftrightarrow}A\lor\lnot A$ and $A\mathbin{\leftrightarrow}A\lor\lnot A\mathrel{\vDash}A$. Therefore, by Corollary 3.6 from [18] and the fact that $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$ is a finitary logic, $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$ is Blok-Pigozzi algebraizable555In [18], Blok-Pigozzi algebraizable is called finitely algebraizable. with the equivalence formulas $\{p\mathbin{\supset}q,q\mathbin{\supset}p,\lnot p\mathbin{\supset}\lnot q,\lnot q\mathbin{\supset}\lnot p\}$ and the single defining equation $p=p\lor\lnot p$. ∎

The algebraization concerned is the quasi-variety generated by the expansion of the 3-element bounded normal i-lattice obtained by adding the unique binary operation $\mathbin{\supset}$ that satisfies ${\mathsf{F}}\mathbin{\supset}p={\mathsf{T}}$ and $(p\lor\lnot p)\mathbin{\supset}q=q$.

6 The Paracomplete Analogue of $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$

In this section, the paracomplete analogue of $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$ is introduced. In Section 7, properties of this logic are presented that are comparable to properties of $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$ that have been presented in the preceding sections.

Replacing the axiom schema $A\lor\lnot A$ by the axiom schema $\lnot A\mathbin{\supset}(A\mathbin{\supset}B)$ in the given Hilbert-style deductive system for $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$ yields a Hilbert-style deductive system for Kleene’s strong three-valued logic introduced in Section 64 of [21] with its implication connective replaced by an implication connective for which the standard deduction theorem holds and enriched with a falsity constant. The name $\mathrm{K3}^{\mathbin{\supset},{\mathsf{F}}}$ is used to denote this logic. It is perhaps clarifying that the axiom schemas involved in the above-mentioned replacement can be paraphrased as “$A$ or $\lnot A$ follows from anything” and “anything follows from $A$ and $\lnot A$”, respectively. Virtually all differences between $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$ and $\mathrm{K3}^{\mathbin{\supset},{\mathsf{F}}}$ can be traced to the fact that the third truth value ${\mathsf{\star}}$ is interpreted as both true and false in the former logic and as neither true nor false in the latter logic.

Like in the case of $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$, meanings are assigned to the formulas of $\mathrm{K3}^{\mathbin{\supset},{\mathsf{F}}}$ by means of valuations that are functions from the set of all formulas of $\mathrm{K3}^{\mathbin{\supset},{\mathsf{F}}}$ to the set $\{{\mathsf{t}},{\mathsf{f}},{\mathsf{\star}}\}$. The conditions that a valuation for $\mathrm{K3}^{\mathbin{\supset},{\mathsf{F}}}$ must satisfy differ from the conditions that a valuation for $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$ must satisfy only with respect to implication:

[TABLE]

The conditions that a valuation for $\mathrm{K3}^{\mathbin{\supset},{\mathsf{F}}}$ must satisfy uniquely characterize the set of valuations induced by the truth value that naturally corresponds to the falsity constant and the functions on the set of truth values that correspond to the different connectives according to Section 3.1 of [4]. The functions concerned, except the function that corresponds to the implication connective, are the same as the ones that are represented by the truth tables presented in Section 64 of [21].

The symbol $\mathrel{\vdash}^{\star}$ is used to denote the derivability relation induced by the axiom schemas and inference rule of the deductive system for $\mathrm{K3}^{\mathbin{\supset},{\mathsf{F}}}$ referred to above. The logical consequence relation of $\mathrm{K3}^{\mathbin{\supset},{\mathsf{F}}}$, denoted by $\mathrel{\vDash}^{\star}$, is based on the idea that a valuation $\nu$ satisfies a formula $A$ if $\nu(A)={\mathsf{t}}$. It is defined as follows: $\Gamma\mathrel{\vDash}^{\star}A$ iff for every valuation $\nu$, either $\nu(A^{\prime})\in\{{\mathsf{f}},{\mathsf{\star}}\}$ for some $A^{\prime}\in\Gamma$ or $\nu(A)={\mathsf{t}}$. The Hilbert-style deductive system for $\mathrm{K3}^{\mathbin{\supset},{\mathsf{F}}}$ referred to above is sound and strongly complete with respect to the semantics of $\mathrm{K3}^{\mathbin{\supset},{\mathsf{F}}}$, i.e. $\Gamma\mathrel{\vdash}^{\star}A$ iff $\Gamma\mathrel{\vDash}^{\star}A$. This is proved for the fragment of $\mathrm{K3}^{\mathbin{\supset},{\mathsf{F}}}$ without the falsity constant in Section 4 of [4]. The proof concerned easily generalizes to full $\mathrm{K3}^{\mathbin{\supset},{\mathsf{F}}}$.

It follows immediately from the definition of $\mathrel{\vDash}^{\star}$ that, for all formulas $A$ and $B$ of $\mathrm{K3}^{\mathbin{\supset},{\mathsf{F}}}$, $A,\lnot A\mathrel{\vDash}^{\star}B$. Hence, $\mathrm{K3}^{\mathbin{\supset},{\mathsf{F}}}$ is not a paraconsistent propositional logic. $\mathrm{K3}^{\mathbin{\supset},{\mathsf{F}}}$ is a paracomplete propositional logic instead.

A propositional logic $\mathcal{L}$ is a paracomplete propositional logic if (a) its logical consequence relation $\mathrel{\vDash}_{\mathcal{L}}$ satisfies the condition that there exists a formula $A$ of $\mathcal{L}$ such that $\mathrel{\not{\!\vDash}}_{\mathcal{L}}A\lor\lnot A$ and (b) its negation connective $\lnot$ satisfies the condition that, for each propositional variable $p$, both $p\mathrel{\not{\!\vDash}}_{\mathcal{L}}\lnot p$ and $\lnot p\mathrel{\not{\!\vDash}}_{\mathcal{L}}p$.

The logical equivalence relation $\Leftrightarrow$ of $\mathrm{K3}^{\mathbin{\supset},{\mathsf{F}}}$ is defined as it is defined for $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$ and classical propositional logic: $A\Leftrightarrow B$ iff for every valuation $\nu$, $\nu(A)=\nu(B)$. Definedness of a formula of $\mathrm{K3}^{\mathbin{\supset},{\mathsf{F}}}$ is defined as consistency of a formula of $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$ is defined: $A$ is defined iff for every valuation $\nu$, $\nu(A)\neq{\mathsf{\star}}$.

$\mathrm{K3}^{\mathbin{\supset},{\mathsf{F}}}$ is essentially the same as the propositional fragment of LPF (Logic of Partial Functions) [6, 15] without the constant representing ${\mathsf{\star}}$ (cf. Section 3.1.2 of [4]).

It is a notable fact that $\mathrm{K3}^{\mathbin{\supset},{\mathsf{F}}}$ and $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$ are dual in the way that classical logical consequences are reflected in these logics. Below, this is made more precise.

We write $V(A)$, where $A$ is a formula of CL, for the set of all propositional variables occurring in $A$.

Let $p_{1},\ldots,p_{n}$, where $n\geq 1$, be propositional variables, and let $A$ be a formula of CL such that $V(A)=\{p_{1},\ldots,p_{n}\}$. Then the inconsistency formula for $A$, written $\iota(A)$, is defined by $\iota(A)=(p_{1}\land\lnot p_{1})\lor\ldots\lor(p_{n}\land\lnot p_{n})$ and the definedness formula for $A$, written $\delta(A)$, is defined by $\delta(A)=(p_{1}\lor\lnot p_{1})\land\ldots\land(p_{n}\lor\lnot p_{n})$. The convention is used that $\iota(A)={\mathsf{F}}$ and $\delta(A)={\mathsf{T}}$ if $V(A)=\emptyset$. Clearly, $\mathrel{\vDash}\iota(A)\mathbin{\equiv}\lnot\delta(A)$ and $\mathrel{\vDash}^{\star}\delta(A)\mathbin{\equiv}\lnot\iota(A)$.

Theorem 6.1

For all formulas $A$ and $B$ of CL:666Clearly, the formulas of CL, $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$ and $\mathrm{K3}^{\mathbin{\supset},{\mathsf{F}}}$ are the same.

[TABLE]

Proof

Theorems 3.10 and 4.2 in [9] constitute a similar result for the first-order extensions of the $\{\lnot,\land,\lor\}$-fragments of $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$ and $\mathrm{K3}^{\mathbin{\supset},{\mathsf{F}}}$ in a setting with multiple-conclusion logical consequence relations. The proofs of these theorems do not depend on the absence of $\mathbin{\supset}$ and ${\mathsf{F}}$ and can be adapted with minor changes to the propositional case and single-conclusion logical consequence relations. ∎

Theorem 6.1 can be generalized to the case with multiple premises. However, in that case, the symmetry that shows up in the theorem gets lost in the single-conclusion versions of $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$ and $\mathrm{K3}^{\mathbin{\supset},{\mathsf{F}}}$ presented in this paper.

7 Properties of $\mathrm{K3}^{\mathbin{\supset},{\mathsf{F}}}$ Comparable to Properties of $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$

In this section, properties of $\mathrm{K3}^{\mathbin{\supset},{\mathsf{F}}}$ are presented that are comparable to properties of $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$ that have been proposed as desirable properties of a reasonable paraconsistent propositional logic and a property of $\mathrm{K3}^{\mathbin{\supset},{\mathsf{F}}}$ is proved that is comparable to the property of $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$ concerning the logical equivalence relation that distinguishes $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$ from other reasonable three-valued paraconsistent propositional logics.

The following properties of $\mathrm{K3}^{\mathbin{\supset},{\mathsf{F}}}$ are similar to properties of $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$ mentioned in Section 3:

• (a*′*)

containment in classical logic: ${\mathrel{\vDash}^{\star}}\subseteq{\mathrel{\vDash_{\mathrm{CL}}}}$;

• (b*′*)

proper basic connectives: for all sets $\Gamma$ of formulas of $\mathrm{K3}^{\mathbin{\supset},{\mathsf{F}}}$ and all formulas $A$, $B$, and $C$ of $\mathrm{K3}^{\mathbin{\supset},{\mathsf{F}}}$:

• (b${}^{\prime}_{1}$)

\Gamma,A\mathrel{\vDash}^{\star}B$${}\land{}$$C iff $\Gamma\mathrel{\vDash}^{\star}A\mathbin{\supset}B$,

• (b${}^{\prime}_{2}$)

$\Gamma\mathrel{\vDash}^{\star}A\land B$,$C$ iff $\Gamma\mathrel{\vDash}^{\star}A$ and $\Gamma\mathrel{\vDash}^{\star}B$,

• (b${}^{\prime}_{3}$)

$\Gamma,A\lor B\mathrel{\vDash}^{\star}C$ iff $\Gamma,A\mathrel{\vDash}^{\star}C$ and $\Gamma,B\mathrel{\vDash}^{\star}C$;

• (c*′*)

weakly maximal paracompleteness relative to classical logic: for all formulas $A$ of $\mathrm{K3}^{\mathbin{\supset},{\mathsf{F}}}$ with $\mathrel{\not{\!\vDash}}^{\star}A$ and $\mathrel{\vDash_{\mathrm{CL}}}A$, for the minimal consequence relation $\mathrel{\vDash^{\prime}}$ such that ${\mathrel{\vDash}^{\star}}\subseteq{\mathrel{\vDash^{\prime}}}$ and $\mathrel{\vDash^{\prime}}A$, for all formulas $B$ of $\mathrm{K3}^{\mathbin{\supset},{\mathsf{F}}}$, $\mathrel{\vDash^{\prime}}B$ iff $\mathrel{\vDash_{\mathrm{CL}}}B$;

• (e*′*)

internalized notion of definedness: $A$ is defined iff ${}\mathrel{\vDash}^{\star}\lnot(A\mathbin{\supset}{\mathsf{F}})\lor\lnot(\lnot A\mathbin{\supset}{\mathsf{F}})$;

• (f*′*)

internalized notion of logical equivalence: $A\Leftrightarrow B$ iff ${}\mathrel{\vDash}^{\star}(A\mathbin{\equiv}B)\land(\lnot A\mathbin{\equiv}\lnot B)$.

It is easy to see that $\mathrm{K3}^{\mathbin{\supset},{\mathsf{F}}}$ has properties (a*′), (b′), (e′), and (f′). Property (c′*) is stated in Section 5 of [8] (where $\mathrm{K3}^{\mathbin{\supset},{\mathsf{F}}}$ is called CLaNs). It remains an open question whether $\mathrm{K3}^{\mathbin{\supset},{\mathsf{F}}}$ has the following property:

• (d*′*)

strongly maximal absolute paracompleteness: for all propositional logics $\mathcal{L}$ with the same logical constants and connectives as $\mathrm{K3}^{\mathbin{\supset},{\mathsf{F}}}$ and a consequence relation $\mathrel{\vDash^{\prime}}$ such that ${\mathrel{\vDash}^{\star}}\subset{\mathrel{\vDash^{\prime}}}$, $\mathcal{L}$ is not paracomplete.

By property (e*′*), $\mathrm{K3}^{\mathbin{\supset},{\mathsf{F}}}$ is a logic of formal undeterminedness in the sense made precise in [14].

The following theorem concerns the number of three-valued paracomplete propositional logics with properties (a*′) and (b′*).

Theorem 7.1

There are exactly 1024 three-valued paracomplete propositional logics with properties (a′) and (b′).777It seems that [22] refers to an unpublished document about these 1024 paracomplete propositional logics.

Proof

Consider the set of 1024 three-valued paracomplete propositional logics that are induced by a matrix of which the set of truth values is $\{{\mathsf{t}},{\mathsf{f}},{\mathsf{\star}}\}$, the set of designated values is $\{{\mathsf{t}}\}$, and the functions $\mathbin{\tilde{\land}}$, $\mathbin{\tilde{\lor}}$, $\mathbin{\tilde{\supset}}$, and $\mathbin{\tilde{\lnot}}$ on the set of truth values that correspond to the connectives $\land$, $\lor$, $\mathbin{\supset}$, and $\lnot$, respectively, are such that, for each $b\in\{{\mathsf{t}},{\mathsf{f}},{\mathsf{\star}}\}$:

[TABLE]

For an induced logic, $\nu(A\diamond B)=\tilde{\diamond}(\nu(A),\nu(B))$ for each $\diamond\in\{\land,\lor,\mathbin{\supset}\}$ and $\nu(\lnot A)=\mathbin{\tilde{\lnot}}(\nu(A))$. From this it follows easily that the above conditions on the functions $\mathbin{\tilde{\land}}$, $\mathbin{\tilde{\lor}}$, $\mathbin{\tilde{\supset}}$, and $\mathbin{\tilde{\lnot}}$ are equivalent to the condition that, for each valuation $\nu$:

[TABLE]

For an induced logic, $\Gamma\mathrel{\vDash}^{\star}A$ iff for every valuation $\nu$, either $\nu(A^{\prime})\neq{\mathsf{t}}$ for some $A^{\prime}\in\Gamma$ or $\nu(A)={\mathsf{t}}$. From this it follows easily that the above condition on valuations implies properties (a*′) and (b′*). Moreover, it follows immediately from the above-mentioned properties of an induced logic, that $\mathbin{\tilde{\lnot}}({\mathsf{\star}})\in\{{\mathsf{f}},{\mathsf{\star}}\}$ iff the induced logic is paracomplete.

In other words, by the above conditions on the functions $\mathbin{\tilde{\land}}$, $\mathbin{\tilde{\lor}}$, $\mathbin{\tilde{\supset}}$, and $\mathbin{\tilde{\lnot}}$, the 1024 induced logics are three-valued paracomplete logics that have properties (a*′) and (b′). It is still to be shown that there are no other three-valued paracomplete logics that has properties (a′) and (b′*).

The only weakening of the above condition on valuations that still guarantees property (a*′*) is the one that is obtained by replacing

[TABLE]

This weakening is equivalent to the weakening of the above conditions on the functions $\mathbin{\tilde{\land}}$, $\mathbin{\tilde{\lor}}$, $\mathbin{\tilde{\supset}}$, and $\mathbin{\tilde{\lnot}}$ that is obtained by replacing

[TABLE]

However, if $\mathbin{\tilde{\lnot}}({\mathsf{\star}})={\mathsf{t}}$, then the induced logic is not paracomplete. ∎

The following is a clarifying reformulation of the conditions on the functions $\mathbin{\tilde{\land}}$, $\mathbin{\tilde{\lor}}$, $\mathbin{\tilde{\supset}}$, and $\mathbin{\tilde{\lnot}}$ of the matrices from the proof of Theorem 7.1:

• •

for each $\tilde{\diamond}\in\{\mathbin{\tilde{\land}},\mathbin{\tilde{\lor}},\mathbin{\tilde{\supset}},\mathbin{\tilde{\lnot}}\}$, the restriction of $\tilde{\diamond}$ to $\{{\mathsf{t}},{\mathsf{f}}\}$ is $\tilde{\diamond}$ from the matrix for classical propositional logic;

• •

for each $\tilde{\diamond}\in\{\mathbin{\tilde{\land}},\mathbin{\tilde{\lor}},\mathbin{\tilde{\supset}}\}$, for each $b\in\{{\mathsf{t}},{\mathsf{f}}\}$:

[TABLE]

• •

$\mathbin{\tilde{\lnot}}({\mathsf{\star}})\neq{\mathsf{t}}$.

This reformulation shows clearly that ${\mathsf{\star}}$ is just an alternative for ${\mathsf{f}}$ in the cases of $\mathbin{\tilde{\land}}$, $\mathbin{\tilde{\lor}}$, and $\mathbin{\tilde{\supset}}$, but not in the case of $\mathbin{\tilde{\lnot}}$.

The next theorem concerns the logical equivalence relation of $\mathrm{K3}^{\mathbin{\supset},{\mathsf{F}}}$.

Theorem 7.2

The logical equivalence relation of $\mathrm{K3}^{\mathbin{\supset},{\mathsf{F}}}$ satisfies laws (1)–(9) from Table 2 and the laws (10′) ${\mathsf{T}}\mathbin{\supset}A\Leftrightarrow A$ and (11′) $(A\land\lnot A)\mathbin{\supset}B\Leftrightarrow{\mathsf{T}}$.

Proof

The proof is easy by constructing, for each of the laws concerned, truth tables for both sides. For laws (1)–(9), this proof coincides with the proof of Theorem 4.1. ∎

The 11 laws of logical equivalence from Theorem 7.2 are sufficient to distinguish $\mathrm{K3}^{\mathbin{\supset},{\mathsf{F}}}$ completely from the other 1023 three-valued paracomplete propositional logics with properties (a*′) and (b′*).

Theorem 7.3

There is exactly one three-valued paracomplete propositional logic with properties (a′) and (b′) of which the logical equivalence relation satisfies laws (1)–(9) from Table 2 and the laws (10′) ${\mathsf{T}}\mathbin{\supset}A\Leftrightarrow A$ and (11′) $(A\land\lnot A)\mathbin{\supset}B\Leftrightarrow{\mathsf{T}}$.

Proof

The proof is similar to the proof of Theorem 4.2. The matrices involved are now the 1024 matrices from the proof of Theorem 7.1. In this case, there are 32 alternatives for $\mathbin{\tilde{\land}}$, 8 alternatives for $\mathbin{\tilde{\lor}}$, 2 alternatives for $\mathbin{\tilde{\supset}}$, and 2 alternatives for $\mathbin{\tilde{\lnot}}$. Below, it will be shown that, for each of these functions, laws from the ones mentioned in the theorem exclude all but one alternative.

Law (1) excludes $\mathbin{\tilde{\land}}({\mathsf{\star}},{\mathsf{f}})={\mathsf{\star}}$, law (3) excludes $\mathbin{\tilde{\land}}({\mathsf{\star}},{\mathsf{t}})={\mathsf{f}}$, law (5) excludes $\mathbin{\tilde{\land}}({\mathsf{\star}},{\mathsf{\star}})={\mathsf{f}}$, and law (7) excludes $\mathbin{\tilde{\land}}({\mathsf{f}},{\mathsf{\star}})={\mathsf{\star}}$ and $\mathbin{\tilde{\land}}({\mathsf{t}},{\mathsf{\star}})={\mathsf{f}}$. Hence, there is only one of the 32 alternatives for $\mathbin{\tilde{\land}}$ left. Law (4) excludes $\mathbin{\tilde{\lor}}({\mathsf{\star}},{\mathsf{f}})={\mathsf{f}}$, law (6) excludes $\mathbin{\tilde{\lor}}({\mathsf{\star}},{\mathsf{\star}})={\mathsf{f}}$, and law (8) excludes $\mathbin{\tilde{\lor}}({\mathsf{f}},{\mathsf{\star}})={\mathsf{f}}$. Hence, there is only one of the 8 alternatives for $\mathbin{\tilde{\lor}}$ left. Law (9) excludes $\mathbin{\tilde{\lnot}}({\mathsf{\star}})={\mathsf{f}}$. Hence, there is only one of the 2 alternatives for $\mathbin{\tilde{\lnot}}$ left. Law (10*′*) excludes $\mathbin{\tilde{\supset}}({\mathsf{t}},{\mathsf{\star}})={\mathsf{f}}$. Hence, there is only one of the 2 alternatives for $\mathbin{\tilde{\supset}}$ left. ∎

Theorem 7.4

The logical equivalence relation of $\mathrm{K3}^{\mathbin{\supset},{\mathsf{F}}}$ satisfies laws (12)–(24) from Table 3.

Proof

Because $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$ and $\mathrm{K3}^{\mathbin{\supset},{\mathsf{F}}}$ have the same truth tables for conjunction, disjunction and negation, the logical equivalence relation of $\mathrm{K3}^{\mathbin{\supset},{\mathsf{F}}}$ also satisfies laws (12)–(21) from Table 3. Proving that the logical equivalence relation of $\mathrm{K3}^{\mathbin{\supset},{\mathsf{F}}}$ also satisfies laws (22)–(24) from Table 3 is straightforward by constructing, for each of the laws concerned, truth tables for both sides. ∎

Like $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$, $\mathrm{K3}^{\mathbin{\supset},{\mathsf{F}}}$ is Blok-Pigozzi algebraizable.

Theorem 7.5

$\mathrm{K3}^{\mathbin{\supset},{\mathsf{F}}}$* is finitely Blok-Pigozzi algebraizable with the equivalence formulas $\{p\mathbin{\supset}q,q\mathbin{\supset}p,\lnot p\mathbin{\supset}\lnot q,\lnot q\mathbin{\supset}\lnot p\}$ and the single defining equation $p=p$ ($p$ and $q$ are propositional variables).*

Proof

The proof follows the same line as the proof of Theorem 5.2. ∎

The algebraization concerned is the quasi-variety generated by the expansion of the 3-element bounded normal i-lattice obtained by adding the unique binary operation $\mathbin{\supset}$ that satisfies ${\mathsf{T}}\mathbin{\supset}p=p$ and $(p\land\lnot p)\mathbin{\supset}q={\mathsf{T}}$.

8 Concluding Remarks

In this paper, properties concerning the logical equivalence relation of a logic are used to distinguish the logic $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$ from the other logics that belong to the 8192 three-valued paraconsistent propositional logics that have properties (a)–(f) from Section 3. These 8192 logics are regarded as potentially interesting because properties (a)–(f) are generally considered to be desirable properties of a reasonable paraconsistent propositional logic.

Properties (a)–(f) concern the logical consequence relation of a logic. Unlike in classical propositional logic, it is not the case that $A\Leftrightarrow B$ iff $A\mathrel{\vDash}B$ and $B\mathrel{\vDash}A$ in a three-valued paraconsistent propositional logic. As a consequence, the classical laws of logical equivalence that follow from property (b) in classical propositional logic, viz. laws (1)–(8) and (12)–(17) from Section 4, do not follow from property (b) in a three-valued paraconsistent propositional logic. Therefore, if closeness to classical propositional logic is considered important, it should be a desirable property of a reasonable paraconsistent propositional logic to have a logical equivalence relation that satisfies laws (1)–(8) and (12)–(17). This would reduce the potentially interesting three-valued paraconsistent propositional logics from 8192 to 32.

In [10], satisfaction of laws (1)–(8), (11), (14)–(17), and (22)–(24) is considered essential for a paraconsistent propositional logic on which a process algebra that allows for dealing with contradictory states is built. It follows easily from Theorem 4.1 and the proof of Theorem 4.2 that $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$ is one of only four three-valued paraconsistent propositional logics with properties (a) and (b) of which the logical equivalence relation satisfies laws (1)–(8), (11), (14)–(17), and (22)–(24).

It is also shown in this paper that, for most presented properties of $\mathrm{LP}^{\mathbin{\supset},{\mathsf{F}}}$, its paracomplete analogue $\mathrm{K3}^{\mathbin{\supset},{\mathsf{F}}}$ has a comparable property.

Acknowledgements

We thank three anonymous referees for carefully reading preliminary versions of this paper, for pointing out several flaws in it, and for suggesting improvements of the presentation.