A Paraconsistent Logic Obtained from an Algebra-Valued Model of Set Theory

Abstract

This paper presents a three-valued paraconsistent logic obtained from some algebra-valued model of set theory. Soundness and completeness theorems are established. The logic has been compared with other three-valued paraconsistent logics.

We are thankful to Prof. Benedikt Löwe for his support in the set theoretic investigations indicated in this paper. We also acknowledge the anonymous referee for making valuable comments. The first author’s research is funded by CSIR Ph.D. fellowship, Govt. of India, grant number: 09/028(0754)/2009 -EMR-1.

1 Introduction and Overview

The idea of Boolean-valued models $\mathbf {V}^{(\mathbb {B})}$ where $\mathbf {V}$ is the standard class model of classical set theory and $\mathbb {B}$ is any arbitrary but fixed complete Boolean algebra was introduced in 1960s (cf. [2]). The motivation behind this construction was to understand in a different way Cohen’s method of forcing [5] that is used to prove the consistency and independence results. Afterward, this kind of construction has come into practice as an autonomous mathematical technique from the angle of generalization of $\mathbf {V}^{(\mathbb {B})}$ and for some other reasons. As for example, we get Heyting-valued model of Intuitionistic set theory [7] where the complete Boolean algebra is replaced by a complete Heyting algebra, Orthomodular-valued model of Quantum set theory [12] where the same is replaced by a complete orthomodular lattice. Generally speaking, an $\mathbb {A}$-valued model $\mathbf {V}^{(\mathbb {A})}$ are models of all (or some) of the $\mathrm {ZF}$-axioms where $\mathbb {A}$ is the algebraic model for the underlying logic on which $\mathrm {ZF}$-axioms are situated. For instance, Boolean algebras are algebraic models of classical logic, Heyting algebras are algebraic models of intuitionistic logic, and orthomodular lattices are algebraic models for quantum logic. Accordingly, $\mathbf {V}^{(\mathbb {A})}$ is called a model for classical set theory, intuitionistic set theory, and quantum set theory when $\mathbb {A}$ is a Boolean algebra, a Heyting algebra and an orthomodular lattice, respectively.

This paper may be considered as a part of a larger project of constructing a paraconsistent set theory. As a step an algebra $\mathbb {A}$ is defined so that $\mathbf {V}^{(\mathbb {A})}$ becomes a model of some version of $\mathrm {ZF}$-axioms (cf. Sect. 7.2.1) [9]. This algebra $\mathbb {A}$ is sufficiently general to give rise to some non-classical logics other than paraconsistent logics. In this paper, we have chosen a three-valued matrix $\mathrm {PS}_3$ as an instance of the above-mentioned algebra $\mathbb {A}$. $\mathrm {PS}_3$ is shown to be a semantics of a paraconsistent logic. We would like to mention some of the results obtained in [9] to justify the selection of the particular algebra $\mathrm {PS}_3$ here. In fact, in this paper we shall discuss the reason for the choice of the particular algebra $\mathrm {PS}_3$ and investigate the logical properties that it represents. As another part of the mentioned bigger project, Tarafder investigated some properties of ordinals in the model $\mathbf {V}^{(\mathrm {PS}_3)}$ of some paraconsistent set theory [13].

It should be focused that claiming an algebra to be the model of some logic means that the logic should be sound and complete with respect to the semantics given in the algebra. Thus in the algebra some elements need to be designated, that is, some 0-ary operations have to be present. In the three cases mentioned above the designated element is only the top element of the bounded lattice. There can be more than one designated elements as will be in our case. An algebra with designated elements is usually called a matrix in logic–literature.

This paper has been designed as follows. In the next section (viz. Sect. 7.2) the requirements to the algebra shall be specified and a three-element matrix will be identified for the purpose. Section 7.3 will deal with the paraconsistent logic (in Hilbert style axiomatic presentation) which is sound and complete with respect to the matrix. In Sect. 7.4 some comparisons of the present logic with other paraconsistent logics will be made. Section 7.5 contains the concluding remarks. All the proofs are given as an appendix.

2 The Algebra for the Proposed Algebra-Valued Models

2.1 Algebraic Properties Required

Let us consider an algebra $\mathbb {A} = (A,\wedge ,\vee ,\Rightarrow ,^*)$ where $(A,\wedge ,\vee )$ is a complete distributive lattice such that the following conditions are satisfied:    

P1::

$x\wedge y\le z$ implies $x\le y\Rightarrow z$.

P2::

$y\le z$ implies $x\Rightarrow y\le x\Rightarrow z$.

P3::

$y\le z$ implies $z\Rightarrow x\le y\Rightarrow x$.

P4::

$(x\wedge y)\Rightarrow z=x\Rightarrow (y\Rightarrow z)$.

  Let us construct $\mathbf {V}^{(\mathbb {A})}$ in the same way as the Boolean-valued model construction of classical set theory. Then extend the language of set theory by adding a constant corresponding to every element of $\mathbf {V}^{(\mathbb {A})}$. Following the standard way (cf. [2]), every formula of the extended language of set theory is associated with a value of A by the mapping $[\![. ]\!]$ as follows:

for any u, v in $\mathbf {V}^{(\mathbb {A})}$,

$$\begin{aligned}{}[\![u \in v ]\!]= \bigvee _{x \in dom(v)} (v(x) \wedge [\![x = u ]\!]) \end{aligned}$$

$$\begin{aligned}{}[\![u = v ]\!]= \bigwedge _{x \in dom(u)} (u(x) \Rightarrow [\![x \in v ]\!]) \wedge \bigwedge _{y \in dom(v)} (v(y) \Rightarrow [\![y \in u ]\!]). \end{aligned}$$

Now for any well-formed formulas $\sigma$ and $\tau$ we define

$$\begin{aligned}{}[\![\sigma \wedge \tau ]\!]&= [\![\sigma ]\!]\wedge [\![\tau ]\!]\\ [\![\sigma \vee \tau ]\!]&= [\![\sigma ]\!]\vee [\![\tau ]\!]\\ [\![\sigma \rightarrow \tau ]\!]&= [\![\sigma ]\!]\Rightarrow [\![\tau ]\!]\\ [\![\lnot \sigma ]\!]&= [\![\sigma ]\!]^* \end{aligned}$$

for any formula $\varphi (x)$ with one free variable x,

$$\begin{aligned}{}[\![\forall x \varphi (x) ]\!]&= \bigwedge _{u \in \mathbf {V}^{(\mathbb {A})}} [\![\varphi (u) ]\!]\\ [\![\exists x \varphi (x) ]\!]&= \bigvee _{u \in \mathbf {V}^{(\mathbb {A})}} [\![\varphi (u) ]\!]\end{aligned}$$

A formula $\varphi$ will be called valid in $\mathbf {V}^{(\mathbb {A})}$ iff $[\![\varphi ]\!]\in D$, where D is the designated set of $\mathbb {A}$. It is well known for a Boolean-valued model or Heyting-valued model that for any formula $\varphi (x)$ with one free variable and any constant u of the extended language,

$$\begin{aligned}{}[\![\forall x (x \in u) \rightarrow \varphi (x) ]\!]= \bigwedge _{x \in dom(u)}(u(x) \Rightarrow [\![\varphi (x)]\!]).\quad \quad \quad \qquad \quad ({\mathrm {BQ}_\varphi }) \end{aligned}$$

But $\mathrm {BQ}_\varphi$ does not hold generally in $\mathbf {V}^{(\mathbb {A})}$. A formula $\varphi$ will be called a negation-free formula (NFF) if no subformula of it contains the unary connective $\lnot$. In [9] it is proved that if $\mathrm {BQ}_\varphi$ holds in $\mathbf {V}^{(\mathbb {A})}$ for each negation-free formula $\varphi$ then the $\mathrm {ZF}$-axioms Extensionality, Pairing, Infinity, Union, and Powerset are valid in $\mathbf {V}^{(\mathbb {A})}$. Moreover, under the same conditions NFF-Separation and NFF-Replacement are also valid in $\mathbf {V}^{(\mathbb {A})}$ where NFF-Separation and NFF-Replacement means, respectively, the Separation and Replacement axiom schemas only for negation-free formulas.

It should be clear that although a negation operator is present in the algebra it did not play any role so far. Now, in order to incorporate the paraconsistency factor, negation comes into the picture. It is known that the key feature of paraconsistency lies in the non-approval of the law of explosion ($\{ \varphi , \lnot \varphi \} \vdash \psi$ for all well-formed formulas $\varphi , \psi$) which is present in the classical as well as intuitionistic logics. So paraconsistency is characterized by the fact that there are well-formed formulas $\varphi$ and $\psi$ such that

$$\begin{aligned} \{\varphi , \lnot \varphi \} \nvdash \psi .\qquad \qquad \quad \qquad \quad (\mathrm{{Par}}) \end{aligned}$$

The reflection of (Par) in the algebra should be as follows: while both $\varphi$ and $\lnot \varphi$ receive some designated values, $\psi$ does not. The algebra $(A,\wedge ,\vee ,\Rightarrow )$ is to be enhanced with a $^*$ so as to fulfill the above condition. Can we find such a matrix? The two-element lattice cannot be a good choice since for satisfying properties $\mathbf {P1}$, $\mathbf {P2}$, $\mathbf {P3}$, and $\mathbf {P4}$ the truth table of $\Rightarrow$ has either to be the same as the two-valued Boolean implication table or it becomes degenerated. So we look into a three-element lattice.

2.2 The Three-Valued Matrix $\mathrm {PS}_3$

In this section, we introduce a three-valued matrix having the following truth tables:

and as the designated set.

$\mathrm {PS_3}$ is a complete distributive lattice relative to $\wedge , \vee$. It is easy to check that $\mathrm {PS_3}$ satisfies $\mathbf {P1}$, $\mathbf {P2}$, $\mathbf {P3}$, and $\mathbf {P4}$. By asserting values from to $\varphi$ and 0 to $\psi$ one can check that (Par) is satisfied. Moreover, in [9] it is proved that $\mathrm {BQ}_\varphi$ holds in $\mathbf {V}^{(\mathrm {PS}_3)}$ for every negation-free formula $\varphi$.

This matrix is included in the collection of $2^{13}$ three-valued matrices of the Logic of Formal Inconsistencies (cf. [4]) after exclusion of the inconsistency operator “$\bullet$”. For our purpose we do not need the operator for inconsistency which acts for internalizing inconsistency within the object language. Now it is important to explain why we have chosen $\mathrm {PS}_3$. First of all has to be a complete distributive lattice for which $\wedge$ and $\vee$ have to be the operators minimum and maximum, respectively. Second, for satisfying properties $\mathbf {P1}$, $\mathbf {P2}$, $\mathbf {P3}$, and $\mathbf {P4}$ the only possibilities for the implication are given below:

The implications $\Rightarrow _1$ and $\Rightarrow _2$ cannot produce a reasonable logic as these two are degenerated. The implication $\Rightarrow _3$ produces converse of $\mathbf {P1}$ also which we do not require. Besides, $\Rightarrow _3$ together with the above-mentioned operators $\wedge$ and $\vee$ produce the three-valued Heyting algebra. As a consequence we are interested in $\Rightarrow _4$ which is the implication of $\mathrm {PS}_3$. Before fixing the truth table of $^*$ it should be noticed, since in the chosen truth table for $\Rightarrow$, for getting Modus Ponens as a valid rule in our system the designated set has to be fixed as . For the truth table of $^*$ we can go for any of the following tables which can produce a paraconsistent logic provided the designated set is fixed as .

We are interested in taking $1^* = 0$ and $0^* = 1$ so that it does not violate the third criterion of Jaśkowski for being a paraconsistent logic (cf. Sect. 7.4). So we could choose any one of ${^*}_1$ and ${^*}_2$. Since we want to have the rule of double negation, as in many of the other well-known paraconsistent logics (shown in Sect. 7.4) the only choice for $^*$ is ${^*}_1$. However, it may be mentioned that in [11] a three-valued paraconsistent logic G’$_3$ having connectives $\wedge$, $\vee$, $\Rightarrow$ and $^*$ has been intensively investigated in which $\wedge$ and $\vee$ are same as $\mathrm {PS}_3$ but $\Rightarrow$ and $^*$ are taken as $\Rightarrow _3$ and ${^*}_2$, respectively. It is to be noted that $\mathrm {PS}_3$ is a fixed, particular algebra of type (2, 2, 2, 1, 0, 0) or a matrix that satisfies the conditions $\mathbf {P1}$, $\mathbf {P2}$, $\mathbf {P3}$, $\mathbf {P4}$, and (Par). $\mathbf {V}^{(\mathrm {PS}_3)}$ will have all the desired properties provided it can be made an algebraic model of some paraconsistent logic.

3 The Logic $\mathbb {L}\mathrm {PS}_3$

In this section we introduce an axiom system for the propositional logic $\mathbb {L}\mathrm {PS}_3$ having the matrix $\mathrm {PS}_3$ as the three-valued semantics. The alphabet of $\mathbb {L}\mathrm {PS}_3$ consists of propositional letters $p_1, p_2, \ldots$; logical connectives $\lnot , \; \wedge , \; \vee , \; \rightarrow$. The well-formed formulas are constructed in the usual way.

3.1 The Axiom System for $\mathbb {L}\mathrm {PS}_3$

The following formulas are taken as the axioms for $\mathbb {L}\mathrm {PS}_3$:

           $(\mathrm {Ax}1) \qquad \varphi \rightarrow (\psi \rightarrow \varphi )$

           $(\mathrm {Ax}2) \qquad (\varphi \rightarrow (\psi \rightarrow \gamma )) \rightarrow ((\varphi \rightarrow \psi ) \rightarrow (\varphi \rightarrow \gamma ))$

           $(\mathrm {Ax}3) \qquad \varphi \wedge \psi \rightarrow \varphi$

           $(\mathrm {Ax}4) \qquad \varphi \wedge \psi \rightarrow \psi$

           $(\mathrm {Ax}5) \qquad \varphi \rightarrow \varphi \vee \psi$

           $(\mathrm {Ax}6) \qquad (\varphi \rightarrow \gamma ) \wedge (\psi \rightarrow \gamma ) \rightarrow (\varphi \vee \psi \rightarrow \gamma )$

           $(\mathrm {Ax}7) \qquad (\varphi \rightarrow \psi ) \wedge (\varphi \rightarrow \gamma ) \rightarrow (\varphi \rightarrow \psi \wedge \gamma )$

           $(\mathrm {Ax}8) \qquad \varphi \leftrightarrow \lnot \lnot \varphi$

           $(\mathrm {Ax}9) \qquad \lnot (\varphi \wedge \psi ) \leftrightarrow (\lnot \varphi \vee \lnot \psi )$

         $(\mathrm {Ax}10) \qquad (\varphi \wedge \lnot \varphi ) \rightarrow (\lnot (\psi \rightarrow \varphi ) \rightarrow \gamma )$

         $(\mathrm {Ax}11) \qquad (\varphi \rightarrow \psi ) \rightarrow (\lnot (\varphi \rightarrow \gamma ) \rightarrow \psi )$

         $(\mathrm {Ax}12) \qquad (\lnot \varphi \rightarrow \psi ) \rightarrow (\lnot (\gamma \rightarrow \varphi ) \rightarrow \psi )$

         $(\mathrm {Ax}13) \qquad \bot \rightarrow \varphi$

         $(\mathrm {Ax}14) \qquad (\varphi \wedge (\psi \rightarrow \bot )) \rightarrow \lnot (\varphi \rightarrow \psi )$

         $(\mathrm {Ax}15) \qquad (\varphi \wedge (\lnot \varphi \rightarrow \bot )) \vee (\varphi \wedge \lnot \varphi ) \vee (\lnot \varphi \wedge (\varphi \rightarrow \bot ))$

where $\varphi , \psi , \gamma$ are any well-formed formulas and $\bot$ is the abbreviation for $\lnot (\theta \rightarrow \theta )$ for any arbitrary formula $\theta$.

The rules for $\mathbb {L}\mathrm {PS}_3$ are the following:

• 1. $\frac{\varphi , \; \psi }{\varphi \wedge \psi }$

• 2. $\frac{\varphi , \; \varphi \rightarrow \psi }{\psi }$

Let $\vdash$ and $\models$ be the syntactic and semantic consequence relations, respectively, defined in the usual way with respect to the above-mentioned axiom system and the matrix $\mathrm {PS}_3$. It will be proved that the above propositional axiom system is sound and (weak)complete with respect to $\mathrm {PS}_3$.

3.2 Soundness

Theorem 7.3.1

For any formula $\varphi$ and a set of formulas $\Gamma$, if $\Gamma \vdash \varphi$ then $\Gamma \models \varphi$.

Proof

It is immediate that under any valuation the values of the axioms are either 1 or and all the rules preserve designatedness of well-formed formulas. So the theorem follows. $\square$

3.3 Completeness

For the proof of completeness we need a few lemmas.

Lemma 7.3.2

For any formula $\varphi , \quad \vdash \; \varphi \rightarrow \varphi$ holds.

Lemma 7.3.3

(Deduction Theorem) If $\Gamma \cup \{\varphi \} \; \vdash \; \psi$ then $\Gamma \; \vdash \; \varphi \rightarrow \psi$.

Proof

The proof is in the usual procedure by induction on the length of derivation of $\psi$ from $\Gamma \cup \{\varphi \}$. $\square$

Using the Deduction theorem one can prove the following lemma.

Lemma 7.3.4

For any formulas $\varphi , \psi$ and $\gamma$ the following formulas are theorems.

• (i) $(\varphi \rightarrow \psi ) \rightarrow ((\varphi \wedge \gamma ) \rightarrow \psi )$

• (ii) $(\varphi \rightarrow \psi ) \rightarrow ((\psi \rightarrow \gamma ) \rightarrow (\varphi \rightarrow \gamma ))$

• (iii) $(\varphi \rightarrow \psi ) \wedge (\psi \rightarrow \gamma ) \rightarrow (\varphi \rightarrow \gamma )$

Lemma 7.3.5 is the most important step to prove the completeness theorem.

Lemma 7.3.5

For any formula $\varphi$ and a given valuation v with respect to $\mathrm {PS}_3$ let $\varphi '$ be defined by

$$ \varphi ' = \left\{ \begin{array}{rll} \varphi \wedge (\lnot \varphi \rightarrow \bot ) &{}\quad {if} &{}\quad v(\varphi ) = 1; \\ \varphi \wedge \lnot \varphi &{}\quad {if} &{}\quad v(\varphi ) = {1}/{2}; \\ \lnot \varphi \wedge (\varphi \rightarrow \bot ) &{}\quad {if} &{}\quad v(\varphi ) = 0. \end{array}\right. $$

If $p_{i_1}, p_{i_2}, \ldots , p_{i_k}$ are the propositional letters in $\varphi$ then $\{p_{i_1}', p_{i_2}', \ldots , p_{i_k}'\} \vdash \varphi '$.

Proof

The proof is obtained by Kalmer’s method by induction on the complexity of $\varphi$. For the detail proof we refer Appendix A. $\square$

Now we are in the position to prove the weak completeness theorem.

Theorem 7.3.6

(Completeness) For any formula $\varphi$, if $\models \varphi$ then $\vdash \varphi$.

Proof

Let $\varphi$ be a formula such that $\models \varphi$. Moreover, let $p_{i_1}, p_{i_2}, \ldots , p_{i_n}$ be n propositional letters in $\varphi$. By the Lemma 7.3.5, for any arbitrarily fixed valuation we have $\{p_{i_1}', p_{i_2}', \ldots , p_{i_n}'\} \vdash \varphi '$. Since, $\models \varphi$, by the definition, $\varphi '$ is either $\varphi \wedge (\lnot \varphi \rightarrow \bot )$ or $\varphi \wedge \lnot \varphi$. So in any case $\{p_{i_1}', p_{i_2}', \ldots , p_{i_n}'\} \; \vdash \; \varphi$ can be derived by Axiom 3 and using M.P. Hence, deduction theorem gives

$$\begin{aligned} \{p_{i_1}', p_{i_2}', \ldots , p_{i_{n-1}}'\} \; \vdash \; p_{i_n}' \rightarrow \varphi . \end{aligned}$$

Now, since the valuation was arbitrary, we get

$$\begin{aligned} \{p_{i_1}', p_{i_2}', \ldots , p_{i_{n-1}}'\} \;&\vdash \; [p_{i_n} \wedge (\lnot p_{i_n} \rightarrow \bot )] \rightarrow \varphi , \\ \{p_{i_1}', p_{i_2}', \ldots , p_{i_{n-1}}'\} \;&\vdash \; (p_{i_n} \wedge \lnot p_{i_n}) \rightarrow \varphi \\ \quad \text {and} \quad \{p_{i_1}', p_{i_2}', \ldots , p_{i_{n-1}}'\} \;&\vdash \; [\lnot p_{i_n} \wedge (p_{i_n} \rightarrow \bot )] \rightarrow \varphi . \end{aligned}$$

Hence, the following derivation can be established:

$\{p_{i_1}', p_{i_2}', \ldots , p_{i_{n-1}}'\} \; \vdash$

       1. $[(p_{i_n} \wedge (\lnot p_{i_n} \rightarrow \bot )) \rightarrow \varphi ] \wedge [(p_{i_n} \wedge \lnot p_{i_n}) \rightarrow \varphi ] \wedge$

                                            $[(\lnot p_{i_n} \wedge (p_{i_n} \rightarrow \bot )) \rightarrow \varphi ]$ Rule 1

       2. $[(p_{i_n} \wedge (\lnot p_{i_n} \rightarrow \bot )) \vee (p_{i_n} \wedge \lnot p_{i_n}) \vee$

                                            $(\lnot p_{i_n} \wedge (p_{i_n} \rightarrow \bot ))] \rightarrow \varphi$ Ax6

       3. $(p_{i_n} \wedge (\lnot p_{i_n} \rightarrow \bot )) \vee (p_{i_n} \wedge \lnot p_{i_n}) \vee (\lnot p_{i_n} \wedge (p_{i_n} \rightarrow \bot ))$ Ax15

       4. $\varphi$ M.P. 2, 3

Repeating this process for each of the remaining $p_{i_j}' \; \{j = n-1, n-2, \ldots , 1\}$ we get $\vdash \varphi$.

Hence, the (weak) completeness theorem is proved. $\square$

It is worthwhile to mention that another axiomatization of the matrix $\mathrm {PS}_3$ together with an extra operator $\bullet$ can be found in [6]. But as described earlier we do not need the logical operator $\bullet$ for our purpose. It can be proved that the $\bullet$-less axioms cannot form a complete axiom system for $\mathrm {PS}_3$. For the $\bullet$-free fragment of this logic our axioms give a $\bullet$-free set of axioms.

4 $\mathbb {L}\mathrm {PS}_3$ and Other Three-Valued Paraconsistent Logics

In this section, some important properties of $\mathbb {L}\mathrm {PS}_3$ will be discussed and comparisons between $\mathbb {L}\mathrm {PS}_3$ and some other well-known three-valued paraconsistent logics will be pointed out with respect to some logical properties.

4.1 Maximality Relative to Classical Propositional Logic

Maximality is an important issue in the study of paraconsistent logics (cf. [1, 4]).

Definition 7.4.1

A logic $\mathbf {L_1} = \langle \mathscr {L}, \vdash _1 \rangle$ is said to be maximal relative to a logic $\mathbf {L_2} = \langle \mathscr {L}, \vdash _2 \rangle$ iff

• (i) $\vdash _1 \varphi$ implies $\vdash _2 \varphi$ for any $\varphi$, and

• (ii) if $\nvdash _1 \varphi$, $\vdash _2 \varphi$ and $\vdash _1$ is enhanced to $\vdash _1'$ by adding $\varphi$ to the theorem set of $\mathbf {L_1}$ then $\langle \mathscr {L}, \vdash _1' \rangle = \langle \mathscr {L}, \vdash _2 \rangle$.

Definition 7.4.1 is more demanding than what is there in [3]. The change is in the condition $\mathrm {(ii)}$ of the Definition 7.4.1. In [3] the condition (ii) was taken as if $\nvdash _1 \varphi$, $\vdash _2 \varphi$ and $\vdash _1$ is enhanced to $\vdash _1'$ by adding $\varphi$ to the theorem set of $\mathbf {L_1}$ then the set of theorems in $\langle \mathscr {L}, \vdash _1' \rangle$ is same as the set of theorems in $\langle \mathscr {L}, \vdash _2 \rangle$.

The following theorem shows the relationship between $\mathbb {L}\mathrm {PS}_3$ and the classical propositional logic.

Theorem 7.4.2

$\mathbb {L}\mathrm {PS}_3$ is maximal relative to the classical propositional logic $\mathrm {(CPL)}$.

Proof

The proof is given in Appendix B.

4.2 Comparison with Other Logics

The three-valued paraconsistent logics chosen for comparisons are G. Priest’s Logic of Paradox ($\mathrm {LP}$), Logic of Formal Inconsistency 1 ($\mathrm {LFI1}$) and Logic of Formal Inconsistency 2 ($\mathrm {LFI2}$) by W.A. Carnielli, J. Marcos, and S. de Amo, I.M.L. D’Ottaviano’s logic ($\mathrm {J_3}$), The Logic $\mathrm {RM_3}$ by the Entailment school, A. M. Sette’s three-valued paraconsistent logic $\mathrm {P^1}$ and C. Mortensen’s paraconsistent logic $\mathrm {C_{0,2}}$. Moreover, we will also make a comparison table with respect to S. Jaśkowski’s and N. Da Costa’s criteria for paraconsistent logics.

In $\mathrm {1948}$ S. Jaśkowski proposed three conditions for a paraconsistent propositional logic, and the simplified versions of which are as follows (cf. [8, 10]):    

Jas1 :

the logic does not satisfy the implicational law of overfilling:

$$\begin{aligned} \varphi \rightarrow (\lnot \varphi \rightarrow \psi ); \end{aligned}$$

Jas2 :

the logic should be rich enough to enable practical inferences: it satisfies modus ponens and the following formulas:

Jas3 :

it should have an intuitive justification: restriction to $\{0,1\}$ gives the classical valuation.  

  Driven by some different motivations in 1963 Newton da Costa wanted to characterize paraconsistency by proposing a whole hierarchy of paraconsistent propositional calculi, known as $\mathrm {C_n}$, for $0 < n < \omega$. The following four conditions are the basic requirements for this calculi (cf. [10]):    

NdaC1 :

the law of non-contradiction, $\lnot (\varphi \wedge \lnot \varphi )$, should not be a valid schema;

NdaC2 :

from the set of formulae, $\{\varphi , \lnot \varphi \}$, not all formulas should be derived in general;

NdaC3 :

extensions to the predicate calculi (with or without equality) of these propositional calculi are simple;

NdaC4 :

without violating NdaC1, the calculi should contain the most part of the schemata and rules of the classical propositional calculus.  

  We will first produce a comparison table below where the following abbreviations are used:

• $\mathrm {DN}$ for $\vdash \lnot \lnot \varphi \leftrightarrow \varphi$.

• $\mathrm {DM1}$ for $\vdash \lnot (\varphi \wedge \psi ) \leftrightarrow (\lnot \varphi \vee \lnot \psi )$.

• $\mathrm {DM2}$ for $\vdash \lnot (\varphi \vee \psi ) \leftrightarrow (\lnot \varphi \wedge \lnot \psi )$.

• $\mathrm {LEM}$ for $\vdash \varphi \vee \lnot \varphi$.

• $\mathrm {C}$ for $\vdash (\lnot \varphi \rightarrow \lnot \psi ) \rightarrow (\psi \rightarrow \varphi )$.

• $\mathrm {C1}$ for $\vdash (\lnot \varphi \rightarrow \psi ) \rightarrow (\lnot \psi \rightarrow \varphi )$.

• $\mathrm {C2}$ for $\vdash (\varphi \rightarrow \lnot \psi ) \rightarrow (\psi \rightarrow \lnot \varphi )$.

• $\mathrm {C3}$ for $\vdash (\varphi \rightarrow \psi ) \rightarrow (\lnot \psi \rightarrow \lnot \varphi )$.

• $\mathrm {HS}$ for $\vdash (\varphi \rightarrow \psi ) \wedge (\psi \rightarrow \gamma ) \rightarrow (\varphi \rightarrow \gamma )$.

• $\mathrm {MP}$ for the rule Modus Ponens.

• $\mathrm {DT}$ for the Deduction Theorem.

($\checkmark$)-mark indicates that the property holds and (x)-mark indicates that the property does not hold in the corresponding logical system.

	$\mathrm {DN}$	$\mathrm {DM1}$	$\mathrm {DM2}$	$\mathrm {LEM}$	$\mathrm {C}$	$\mathrm {C1}$	$\mathrm {C2}$	$\mathrm {C3}$	$\mathrm {HS}$	$\mathrm {MP}$	$\mathrm {DT}$
$\mathbb {L}\mathrm {PS}_3$	$\checkmark$	$\checkmark$	$\checkmark$	$\checkmark$	x	x	x	x	$\checkmark$	$\checkmark$	$\checkmark$
$\mathrm {LP}$	$\checkmark$	$\checkmark$	$\checkmark$	$\checkmark$	$\checkmark$	$\checkmark$	$\checkmark$	$\checkmark$	x	x	$\checkmark$
$\mathrm {LFI1}$	$\checkmark$	$\checkmark$	$\checkmark$	$\checkmark$	x	x	x	x	$\checkmark$	$\checkmark$	$\checkmark$
$\mathrm {LFI2}$	$\checkmark$	x	x	$\checkmark$	x	x	x	x	$\checkmark$	$\checkmark$	$\checkmark$
$\mathrm {J_3}$	$\checkmark$	$\checkmark$	$\checkmark$	$\checkmark$	x	x	x	x	$\checkmark$	$\checkmark$	$\checkmark$
$\mathrm {RM_3}$	$\checkmark$	$\checkmark$	$\checkmark$	$\checkmark$	$\checkmark$	$\checkmark$	$\checkmark$	$\checkmark$	$\checkmark$	$\checkmark$	x
$\mathrm {P^1}$	x	x	x	$\checkmark$	x	x	x	x	$\checkmark$	$\checkmark$	$\checkmark$
$\mathrm {C_{0,2}}$	$\checkmark$	x	x	$\checkmark$	x	x	x	x	$\checkmark$	$\checkmark$	$\checkmark$

We also present the following comparison table with respect to $\mathrm {Jas1}$, $\mathrm {Jas2}$, $\mathrm {Jas3}$, $\mathrm {NdaC1}$, and $\mathrm {NdaC2}$.

	$\mathrm {Jas1}$	$\mathrm {Jas2}$	$\mathrm {Jas3}$	$\mathrm {NdaC1}$	$\mathrm {NdaC2}$
$\mathbb {L}\mathrm {PS}_3$	$\checkmark$	$\checkmark$	$\checkmark$	x	$\checkmark$
$\mathrm {LP}$	x	x	$\checkmark$	x	$\checkmark$
$\mathrm {LFI1}$	$\checkmark$	$\checkmark$	$\checkmark$	x	$\checkmark$
$\mathrm {LFI2}$	$\checkmark$	$\checkmark$	$\checkmark$	x	$\checkmark$
$\mathrm {J_3}$	$\checkmark$	$\checkmark$	$\checkmark$	x	$\checkmark$
$\mathrm {RM_3}$	$\checkmark$	$\checkmark$	$\checkmark$	x	$\checkmark$
$\mathrm {P^1}$	$\checkmark$	$\checkmark$	$\checkmark$	$\checkmark$	$\checkmark$
$\mathrm {C_{0,2}}$	$\checkmark$	$\checkmark$	$\checkmark$	$\checkmark$	$\checkmark$

Note. All the observations for $\mathrm {LP}$ and $\mathrm {C_{0,2}}$ are semantical.

4.3 Some Other Differences

This section shows some more differences between some of the aforesaid three-valued logics and $\mathbb {L}\mathrm {PS}_3$ which are not included in the comparison table.

Comparison with $\mathrm {LFI1}$ and $\mathrm {LFI2}$: From the tables we see that the entries for $\mathbb {L}\mathrm {PS}_3$ and $\mathrm {LFI1}$ are the same. In fact, though the structure for $\mathrm {LFI1}$ contains an extra unary operator $\bullet$ named as inconsistency, this structure and $\mathrm {PS}_3$ are interdefinable. But as described earlier we do not need the logical operator $\bullet$ for our purpose. Second, with respect to the $\Rightarrow$ defined in $\mathrm {PS}_3$, conditions $\mathbf {P1}$, $\mathbf {P2}$, $\mathbf {P3}$, and $\mathbf {P4}$ are satisfied but not with respect to the implication operator of the matrix for $\mathrm {LFI1}$.

Some differences are marked in the table with $\mathrm {LFI2}$. Another major difference lies in the fact that the matrix for $\mathrm {LFI2}$ does not form a lattice.

Comparison between $\mathbb {L}\mathrm {PS}_3$ and $\mathrm {RM_3}$: The comparison table shows that there are formulas which are theorems of $\mathrm {RM_3}$ but not of $\mathbb {L}\mathrm {PS}_3$, whereas the comparison tables do not explain anything about the converse. But a simple observation shows that the formula $\varphi \rightarrow (\psi \rightarrow \varphi )$ which is one of the axioms of $\mathbb {L}\mathrm {PS}_3$ is not a theorem of $\mathrm {RM_3}$.

$\mathbb {L}\mathrm {PS}_3$ and $\mathrm {RM_3}$ agree on the important fact that neither $(\varphi \rightarrow \psi ) \leftrightarrow (\lnot \varphi \vee \psi )$ nor $(\varphi \rightarrow \psi ) \leftrightarrow \lnot (\varphi \wedge \lnot \psi )$ is a theorem.

Comparison between $\mathbb {L}\mathrm {PS}_3$ and $\mathrm {P^1}$: Like the three-valued semantics of $\mathrm {LFI2}$ the three-valued semantics of $\mathrm {P^1}$ also does not form a lattice which makes a difference with $\mathrm {PS}_3$. The following interesting similarities and dissimilarities of these two logics may also be noted.

• $(\varphi \rightarrow \psi ) \rightarrow (\lnot \varphi \vee \psi )$ is a theorem in both.

• The reverse, $(\lnot \varphi \vee \psi ) \rightarrow (\varphi \rightarrow \psi )$ is not a theorem in any of them.

• $(\varphi \rightarrow \psi ) \rightarrow \lnot (\varphi \wedge \lnot \psi )$ is a theorem of $\mathbb {L}\mathrm {PS}_3$ but not a theorem in $\mathrm {P^1}$.

• But the reverse, $\lnot (\varphi \wedge \lnot \psi ) \rightarrow (\varphi \rightarrow \psi )$ is a theorem of $\mathrm {P^1}$ but not a theorem of $\mathbb {L}\mathrm {PS}_3$.

5 Conclusion

In the literature one can get several paraconsistent logics having algebraic semantics. Some of them are mentioned in this paper. These logics and their algebraic semantics were developed from various motivations. Our motivation is to construct models of some paraconsistent set theories.

With respect to the algebraic properties discussed in Sect. 7.2 which are needed for making an algebra-valued model of a paraconsistent set theory, the following comparison with other paraconsistent logics is made. The algebras of the three-valued semantics for $\mathrm {LFI2}$, $\mathrm {P^1}$ and $\mathrm {C_{0,2}}$ are not lattices and for the others we make the following comparison table.

	$\mathbf {P1}$	$\mathbf {P2}$	$\mathbf {P3}$	$\mathbf {P4}$
$\mathbb {L}\mathrm {PS}_3$	$\checkmark$	$\checkmark$	$\checkmark$	$\checkmark$
$\mathrm {LP}$	x	$\checkmark$	$\checkmark$	$\checkmark$
$\mathrm {LFI1}$	x	$\checkmark$	$\checkmark$	$\checkmark$
$\mathrm {J_3}$	x	$\checkmark$	$\checkmark$	$\checkmark$
$\mathrm {RM_3}$	x	$\checkmark$	$\checkmark$	x

Note. The comparisons are made with respect to the corresponding three-valued semantics of the respective logics

Thus $\mathrm {PS}_3$ differs from the other three-valued matrices mentioned here in forming an algebraic structure suitable to construct some model of set theory within $\mathbf {V}$ with an underlying paraconsistent logic. It is yet unknown whether other logics are suitable for this purpose. The full development of the corresponding predicate logic by extending $\mathbb {L}\mathrm {PS}_3$ is still pending.

Appendices

Appendix A

Proof of the Lemma 7.3.5:

As it was indicated that the proof will be by induction on the complexity of $\varphi$. Let, $\Gamma = \{p_{i_1}', p_{i_2}', \ldots , p_{i_k}'\}$.

Basis step: It is obvious when the complexity is 0.

Induction hypothesis: Assume the lemma holds well for formulas with complexity less than n.

Induction step: Let the complexity of $\varphi$ be n.

Case 1: Let $\varphi = \lnot \psi$.

Clearly, the complexity of $\psi$ is less than n and the propositional letters in $\psi$ are exactly same as the propositional letters in $\varphi$.

Subcase 1.1: If $v(\psi ) = 1$ then $v(\varphi ) = 0$. Hence, by our construction, $\psi ' = \psi \wedge (\lnot \psi \rightarrow \bot )$ and $\varphi ' = \lnot \varphi \wedge (\varphi \rightarrow \bot )$. Here we get

$\Gamma \; \vdash$

1. $\psi '$       induction hypothesis

            2. $\psi$       Ax3 and M.P.

            3. $\lnot \psi \rightarrow \bot$       Ax4 and M.P.

            4. $\psi \rightarrow \lnot \lnot \psi$       Ax8

            5. $\lnot \lnot \psi$       M.P. 2, 4

            6. $\lnot \varphi \wedge (\varphi \rightarrow \bot )$       Rule 1 on 3 and 5

Hence, in Subcase 1.1, $\Gamma \; \vdash \; \varphi '$.

Subcase 1.2: If then . So by the construction, $\psi ' = \psi \wedge \lnot \psi$ and $\varphi ' = \varphi \wedge \lnot \varphi$. So we have

       $\Gamma \; \vdash$

            1. $\psi '$       induction hypothesis

            2. $\psi$       Ax3 and M.P.

            3. $\lnot \psi$       Ax4 and M.P.

            4. $\psi \rightarrow \lnot \lnot \psi$       Ax8

            5. $\lnot \lnot \psi$       M.P. 2, 4

            6. $\varphi \wedge \lnot \varphi$       Rule 1 on 3 and 5

Hence, $\Gamma \; \vdash \; \varphi '$ holds here.

Subcase 1.3: If $v(\psi ) = 0$ then $v(\varphi ) = 1$. Hence,

                        $\psi ' = \lnot \psi \wedge (\psi \rightarrow \bot )$ and $\varphi ' = \varphi \wedge (\lnot \varphi \rightarrow \bot )$.

The following derivation can be made

       $\Gamma \; \vdash$

            1. $\psi '$       induction hypothesis

            2. $\lnot \psi$       Ax3 and M.P.

            3. $\psi \rightarrow \bot$       Ax4 and M.P.

            4. $(\lnot \lnot \psi \rightarrow \psi ) \rightarrow [(\psi \rightarrow \bot ) \rightarrow (\lnot \lnot \psi \rightarrow \bot )]$       Theorem 7.3.4(ii)

            5. $\lnot \lnot \psi \rightarrow \psi$       Ax8

            6. $(\psi \rightarrow \bot ) \rightarrow (\lnot \lnot \psi \rightarrow \bot )$       M.P. 4, 5

            7. $\lnot \lnot \psi \rightarrow \bot$       M.P. 3, 6

            8. $\varphi '$       Rule 1 on 2, 7

Hence, in Case 1 we always get $\Gamma \; \vdash \; \varphi '$.

Case 2: Let $\varphi = \psi \wedge \gamma$.

Obviously, both the complexities of $\psi$ and $\gamma$ are less than n and the sets of propositional letters in $\varphi$ and $\psi$ are proper subsets of $\{p_{i_1}', p_{i_2}', \ldots , p_{i_k}'\}$, the set of propositional letters in $\varphi$. Hence, clearly by the induction hypothesis and monotonicity property we get

$$\begin{aligned} \Gamma \; \vdash \; \psi ' \quad \text {and} \quad \Gamma \; \vdash \; \gamma '. \end{aligned}$$

Subcase 2.1: If any one of $v(\psi )$ and $v(\gamma )$ is 0 then it can be proved $\Gamma \; \vdash \; \varphi '$. Without loss of generality, let $v(\psi ) = 0$, then $v(\varphi ) = 0$. Hence, we get the following:

$$\begin{aligned} \psi ' = \lnot \psi \wedge (\psi \rightarrow \bot ) \quad \text {and} \quad \varphi ' = \lnot \varphi \wedge (\varphi \rightarrow \bot ). \end{aligned}$$

Since $\Gamma \; \vdash \; \psi '$,

       $\Gamma \; \vdash$

            1. $\lnot \psi$       Ax3 and M.P.

            2. $\psi \rightarrow \bot$       Ax4 and M.P.

            3. $\lnot \psi \rightarrow (\lnot \psi \vee \lnot \gamma )$       Ax5

            4. $\lnot \psi \vee \lnot \gamma$       M.P. 1, 3

            5. $(\lnot \psi \vee \lnot \gamma ) \rightarrow \lnot (\psi \wedge \gamma )$       Ax9

            6. $\lnot (\psi \wedge \gamma )$    M.P. 4, 5

            7. $(\psi \rightarrow \bot ) \rightarrow (\psi \wedge \gamma \rightarrow \bot )$       Theorem 7.3.4(i)

            8. $\psi \wedge \gamma \rightarrow \bot$       M.P. 2, 7

            9. $\varphi '$       Rule 1 on 6, 8

Subcase 2.2: If and then also. So by the definition,

$$\begin{aligned} \psi ' = \psi \wedge \lnot \psi , \quad \gamma ' = \gamma \wedge \lnot \gamma \quad \text {and} \quad \varphi ' = \varphi \wedge \lnot \varphi . \end{aligned}$$

Now for proving $\Gamma \; \vdash \; \varphi '$, i.e., $\Gamma \; \vdash \; (\psi \wedge \gamma ) \wedge \lnot (\psi \wedge \gamma )$ we go through the following derivation, using $\Gamma \; \vdash \; \psi '$ and $\Gamma \; \vdash \; \gamma '$.

$\Gamma \; \vdash$

1. $\psi$       Ax3 and M.P.

2. $\lnot \psi$       Ax4 and M.P.

3. $\gamma$       Ax3 and M.P.

4. $\psi \wedge \gamma$       Rule 1 on 1, 3

5. $\lnot \psi \rightarrow (\lnot \psi \vee \lnot \gamma )$       Ax5

6. $(\lnot \psi \vee \lnot \gamma )$       M.P. 2, 5

7. $(\lnot \psi \vee \lnot \gamma ) \rightarrow \lnot (\psi \wedge \gamma )$       Ax9

8. $\lnot (\psi \wedge \gamma )$       M.P. 6, 7

9. $\varphi '$       Rule 1 on 4, 8

Subcase 2.3: If and $v(\gamma ) = 1$ then also. Hence,

$$\begin{aligned} \psi ' = \psi \wedge \lnot \psi , \quad \gamma ' = \gamma \wedge (\lnot \gamma \rightarrow \bot ) \quad \text {and} \quad \varphi ' = \varphi \wedge \lnot \varphi . \end{aligned}$$

Since $\Gamma \; \vdash \; \psi '$ and $\Gamma \; \vdash \; \gamma '$, using Axiom 1, 2 and rule M.P. we get

$$\begin{aligned} \Gamma \; \vdash \; \psi , \quad \Gamma \; \vdash \; \lnot \psi \quad \text {and} \quad \Gamma \; \vdash \; \gamma . \end{aligned}$$

Now following the same derivation as above we can prove $\Gamma \; \vdash \; \psi '$.

Subcase 2.4: If $v(\psi ) = 1$ and $v(\gamma ) = 1$ then $v(\varphi ) = 1$. Therefore, by our construction,

$$\begin{aligned} \psi ' = \psi \wedge (\lnot \psi \rightarrow \bot ), \quad \gamma ' = \gamma \wedge (\lnot \gamma \rightarrow \bot ) \quad \text {and} \quad \varphi ' = \varphi \wedge (\lnot \varphi \rightarrow \bot ). \end{aligned}$$

So we have to prove $\Gamma \; \vdash \; \varphi '$, i.e., $\Gamma \; \vdash \; (\psi \wedge \gamma ) \wedge [\lnot (\psi \wedge \gamma ) \rightarrow \bot ]$. The derivation is as follows:

$\Gamma \; \vdash$

1. $\psi$       Ax3 and M.P.

2. $\gamma$       Ax3 and M.P.

3. $\lnot \psi \rightarrow \bot$       Ax4 and M.P.

4. $\lnot \gamma \rightarrow \bot$       Ax4 and M.P.

5. $\psi \wedge \gamma$       Rule 1 on 1 and 2

6. $(\lnot \psi \rightarrow \bot ) \wedge (\lnot \gamma \rightarrow \bot )$       Rule 1 on 3 and 4

7. $(\lnot \psi \rightarrow \bot ) \wedge (\lnot \gamma \rightarrow \bot ) \rightarrow (\lnot \psi \vee \lnot \gamma \rightarrow \bot )$       Ax6

8. $\lnot \psi \vee \lnot \gamma \rightarrow \bot$       M.P. 6, 7

9. $\lnot (\psi \wedge \gamma ) \rightarrow (\lnot \psi \vee \lnot \gamma )$       Ax9

10. $[\lnot (\psi \wedge \gamma ) \rightarrow (\lnot \psi \vee \lnot \gamma )] \rightarrow$

$[((\lnot \psi \vee \lnot \gamma ) \rightarrow \bot ) \rightarrow (\lnot (\psi \wedge \gamma ) \rightarrow \bot )]$       Theorem 7.3.4(ii)

11. $\lnot (\psi \wedge \gamma ) \rightarrow \bot$ M.P. repeatedly on 10, 9, 8

12. $\varphi '$       Rule 1 on 5, 11

Subcase 2.5: If $v(\psi ) = 1$ and then by the same derivation in Subcase 2.3 it can be proved $\Gamma \; \vdash \; \varphi '$.

Hence, in Case 2 we can always prove $\Gamma \; \vdash \; \varphi '$.

Case 3: Let $\varphi = \psi \vee \gamma$.

Since $\varphi \vee \psi$ can be abbreviated as $\lnot (\lnot \varphi \wedge \lnot \psi )$ therefore using Case 1 and Case 2, $\Gamma \; \vdash \; \varphi '$ can be proved in this case also.

Case 4: Let $\varphi = \psi \rightarrow \gamma$.

Obviously, both the complexities of $\psi$ and $\gamma$ are less than n and the sets of propositional letters in $\varphi$ and $\psi$ are subsets of $\{p_{i_1}', p_{i_2}', \ldots , p_{i_k}'\}$, the set of propositional letters in $\varphi$. Hence, clearly by the induction hypothesis and monotonicity property we get

$$\begin{aligned} \Gamma \; \vdash \; \psi ' \quad \text {and} \quad \Gamma \; \vdash \; \gamma '. \end{aligned}$$

Subcase 4.1: If $v(\gamma ) = 1$ then no matter what $v(\psi )$ is, $v(\varphi ) = 1$ always. So we get $\gamma ' = \gamma \wedge (\lnot \gamma \rightarrow \bot )$ and $\varphi ' = \varphi \wedge (\lnot \varphi \rightarrow \bot ) = (\psi \rightarrow \gamma ) \wedge [\lnot (\psi \rightarrow \gamma ) \rightarrow \bot ].$

Now for proving $\Gamma \; \vdash \; \varphi '$ we go through the following derivation:

$\Gamma \; \vdash$

1. $\gamma$       Ax3 and M.P.

2. $\lnot \gamma \rightarrow \bot$       Ax4 and M.P.

3. $\gamma \rightarrow (\psi \rightarrow \gamma )$       Ax1

4. $\psi \rightarrow \gamma$       M.P. 1, 3

5. $(\lnot \gamma \rightarrow \bot ) \rightarrow [\lnot (\psi \rightarrow \gamma ) \rightarrow \bot ]$       Ax12

6. $\lnot (\psi \rightarrow \gamma ) \rightarrow \bot$       M.P. 2, 5

7. $\varphi '$       Rule 1 on 4, 6

Subcase 4.2: If then always $v(\varphi ) = 1$. Hence, by the definition,

$$\begin{aligned} \gamma ' = \gamma \wedge \lnot \gamma \quad \text {and} \quad \varphi ' = \varphi \wedge (\lnot \varphi \rightarrow \bot ) = (\psi \rightarrow \gamma ) \wedge [\lnot (\psi \rightarrow \gamma ) \rightarrow \bot ]. \end{aligned}$$

Hence, we get the following:

$\Gamma \; \vdash$

1. $\gamma \wedge \lnot \gamma$       induction hypothesis

2. $\gamma$       Ax3 and M.P.

3. $\gamma \rightarrow (\psi \rightarrow \gamma )$       Ax1

4. $\psi \rightarrow \gamma$       M.P. 1, 2

5. $(\gamma \wedge \lnot \gamma ) \rightarrow [\lnot (\psi \rightarrow \gamma ) \rightarrow \bot ]$       Ax10

6. $\lnot (\psi \rightarrow \gamma ) \rightarrow \bot$       M.P. 1, 5

7. $\varphi '$       Rule 1 on 3, 6

Subcase 4.3: If and $v(\psi ) = 0$ then $v(\varphi ) = 1$. So by the construction, $\gamma ' = \lnot \gamma \wedge (\gamma \rightarrow \bot )$, $\psi ' = \lnot \psi \wedge (\psi \rightarrow \bot )$ and

$$\begin{aligned} \varphi '&= \varphi \wedge (\lnot \varphi \rightarrow \bot ) \\&= (\psi \rightarrow \gamma ) \wedge [\lnot (\psi \rightarrow \gamma ) \rightarrow \bot ]. \end{aligned}$$

Now the following derivation shows that $\Gamma \; \vdash \; \varphi '$ holds in this subcase also.

$\Gamma \; \vdash$

1. $\psi \rightarrow \bot$       Ax4 and M.P.

2. $\bot \rightarrow \gamma$       Ax13

3. $(\psi \rightarrow \bot ) \rightarrow [(\bot \rightarrow \gamma ) \rightarrow (\psi \rightarrow \gamma )]$       Theorem 7.3.4(ii)

4. $(\bot \rightarrow \gamma ) \rightarrow (\psi \rightarrow \gamma )$       M.P. 1, 3

5. $\psi \rightarrow \gamma$       M.P. 2, 4

6. $(\psi \rightarrow \bot ) \rightarrow [\lnot (\psi \rightarrow \gamma ) \rightarrow \bot ]$       Ax11

7. $\lnot (\psi \rightarrow \gamma ) \rightarrow \bot$       M.P. 1, 6

8. $\varphi '$       Rule 1 on 5, 7

Subcase 4.4: If $v(\gamma ) = 0$ and $v(\psi ) = 1$ then $v(\varphi ) = 0$. Therefore, $\gamma ' = \lnot \gamma \wedge (\gamma \rightarrow \bot )$, $\psi ' = \psi \wedge (\lnot \psi \rightarrow \bot )$ and

$$\begin{aligned} \varphi '&= \lnot \varphi \wedge (\varphi \rightarrow \bot ) \\&= \lnot (\psi \rightarrow \gamma ) \wedge [(\psi \rightarrow \gamma ) \rightarrow \bot ]. \end{aligned}$$

Deduction theorem will be used here for proving $\Gamma \; \vdash \; \varphi '$. Since we know $\Gamma \; \vdash \; \psi '$ and $\Gamma \; \vdash \; \gamma '$

$\Gamma \cup \{\psi \rightarrow \gamma \} \; \vdash$

1. $\psi '$       monotonicity

2. $\psi$       Ax3 and M.P. with 1

3. $\gamma '$       monotonicity

4. $\gamma \rightarrow \bot$       Ax4 and M.P. with 3

5. $\psi \rightarrow \gamma$       assumption

6. $\gamma$       M.P. 2, 5

7. $\bot$       M.P. 4, 6

Now applying Deduction theorem we get $\Gamma \; \vdash \; (\psi \rightarrow \gamma ) \rightarrow \bot$.

Again for proving $\Gamma \; \vdash \; \lnot (\psi \rightarrow \gamma )$ we do the following derivation:

$\Gamma \; \vdash$

1. $\psi '$       induction hypothesis

2. $\psi$       Ax3 and M.P. with 1

3. $\gamma '$       induction hypothesis

4. $\gamma \rightarrow \bot$       Ax4 and M.P. with 3

5. $\psi \wedge (\gamma \rightarrow \bot )$       Rule 1 on 2 and 4

6. $\psi \wedge (\gamma \rightarrow \bot ) \rightarrow \lnot (\psi \rightarrow \gamma )$       Axiom 14

7. $\lnot (\psi \rightarrow \gamma )$       M.P. 3, 4

Hence, again by Rule 1 it is derived $\Gamma \; \vdash \; \lnot (\psi \rightarrow \gamma ) \wedge [(\psi \rightarrow \gamma ) \rightarrow \bot ]$ i.e., $\Gamma \; \vdash \; \varphi '$.

Subcase 4.5: If $v(\gamma ) = 0$ and then $v(\varphi ) = 0$. Therefore by definition, $\gamma ' = \lnot \gamma \wedge (\gamma \rightarrow \bot )$, $\psi ' = \psi \wedge \lnot \psi$ and

$\varphi ' = \lnot \varphi \wedge (\varphi \rightarrow \bot ) = \lnot (\psi \rightarrow \gamma ) \wedge [(\psi \rightarrow \gamma ) \rightarrow \bot ]$. Since $\Gamma \; \vdash \; \psi '$ and $\Gamma \; \vdash \; \gamma '$, by Axiom 1, 2 and using M.P. we get

$$\Gamma \; \vdash \; \psi \text { and } \Gamma \; \vdash \; \gamma \rightarrow \bot .$$

Therefore, in this subcase $\Gamma \; \vdash \; \varphi '$ can be proved by following the same steps used in Subcase 4.4.

Hence, combining all the cases the Lemma 7.3.5 is proved. $\square$

Appendix B

Proof of the theorem 7.4.2:

Lemma. First, we show that by adding any theorem of $\mathrm {CPL}$ (Classical Propositional Logic) which is not a theorem of $\mathbb {L}\mathrm {PS}_3$, as an axiom schema in $\mathbb {L}\mathrm {PS}_3$, all the theorems of $\mathrm {CPL}$ can be proved.

Let $\varphi (p_{i_1}, p_{i_2}, \ldots , p_{i_n})$ be a theorem of $\mathrm {CPL}$ but not a theorem of $\mathbb {L}\mathrm {PS}_3$, where $p_{i_1}, p_{i_2}, \ldots , p_{i_n}$ are the propositional variables. Hence, for any valuation v from the set of all formulas of $\mathbb {L}\mathrm {PS}_3$ to $\mathrm {PS}_3$ for which

$$v(\varphi (p_{i_1}, p_{i_2}, \ldots , p_{i_n})) = 0$$

there must exist some $p_{i_l}$, $1 \le l \le n$ such that . Now using this fact without loss of generality we may assume that for any given valuation v we have $v(\varphi (p_{i_1}, p_{i_2}, \ldots , p_{i_n})) = 0$ iff for all $l \in \{1, \ldots , n\}$. It is guaranteed by the following fact: Suppose a formula $\psi (p_{r_1}, p_{r_2}, \ldots p_{r_{t+1}})$ is such that for all $l \in \{ 1, \ldots , t\}$ but . We then replace the propositional variable $p_{r_{t+1}}$

• by $\lnot (p_{r_1} \rightarrow p_{r_1})$ if $v(p_{r_{t+1}}) = 0$

• by $(p_{r_1} \rightarrow p_{r_1})$ if $v(P_{r_{t+1}}) = 1$

in the formula $\psi (p_{r_1}, p_{r_2}, \ldots p_{r_{t+1}})$ and therefore after replacing, the formula will get the value 0 iff all its propositional variables take the value . In this way we always get such a formula $\varphi (p_{i_1}, p_{i_2}, \ldots , p_{i_n})$.

Let us now assume $\sigma (p_{k_1}, p_{k_2}, \ldots , p_{k_m})$ be another arbitrarily chosen theorem of $\mathrm {CPL}$ which is not a theorem of $\mathbb {L}\mathrm {PS}_3$, where $p_{k_1}, p_{k_2}, \ldots , p_{k_m}$ are the propositional variables. It will be proved that $\sigma (p_{k_1}, p_{k_2}, \ldots , p_{k_m})$ can be derived from the axiom system of $\mathbb {L}\mathrm {PS}_3$ if it is extended by the new axiom schema $\varphi (p_{i_1}, p_{i_2}, \ldots , p_{i_n})$. Let $\varphi (p_{k_j})$ be the formula replacing each propositional variable of $\varphi (p_{i_1}, p_{i_2}, \ldots , p_{i_n})$ by $p_{k_j}$, for all $j \in \{1, \ldots , m\}$.

Claim: $\varphi (p_{k_1}) \wedge \varphi (p_{k_2}) \wedge \cdots \wedge \varphi (p_{k_m}) \rightarrow \sigma (p_{k_1}, p_{k_2}, \ldots , p_{k_m})$ is a theorem of $\mathbb {L}\mathrm {PS}_3$.

Proof of the claim. Let v be any valuation. Two cases could happen: either $v(\sigma (p_{k_1}, p_{k_2}, \ldots , p_{k_m})) = 0$ or $v(\sigma (p_{k_1}, p_{k_2}, \ldots , p_{k_m})) \ne 0$.

If $v(\sigma (p_{k_1}, p_{k_2}, \ldots , p_{k_m})) = 0$ and since $\sigma (p_{k_1}, p_{k_2}, \ldots , p_{k_m})$ is a theorem of $\mathrm {CPL}$ there must exist $p_{k_j}$ such that for some $j \in \{1, \ldots , m\}$. Hence, $v(\varphi (p_{k_j})) = 0$ and therefore

$$v(\varphi (p_{k_1}) \wedge \varphi (p_{k_2}) \wedge \cdots \wedge \varphi (p_{k_m}) \rightarrow \sigma (p_{k_1}, p_{k_2}, \ldots , p_{k_m})) = 1.$$

Again if $v(\sigma (p_{k_1}, p_{k_2}, \ldots , p_{k_m})) \ne 0$ then by the truth tables of $\mathrm {PS}_3$

$$v(\varphi (p_{k_1}) \wedge \varphi (p_{k_2}) \wedge \cdots \wedge \varphi (p_{k_m}) \rightarrow \sigma (p_{k_1}, p_{k_2}, \ldots , p_{k_m})) = 1.$$

Hence, for any valuation the formula

$$\begin{aligned} \varphi (p_{k_1}) \wedge \varphi (p_{k_2}) \wedge \cdots \wedge \varphi (p_{k_m}) \rightarrow \sigma (p_{k_1}, p_{k_2}, \ldots , p_{k_m}) \end{aligned}$$

always get the value 1. So by the completeness theorem of $\mathbb {L}\mathrm {PS}_3$ the claim is proved.

Now let us extend the axiom system of $\mathbb {L}\mathrm {PS}_3$ by including $\varphi (p_{i_1}, \ldots , p_{i_n})$ as an axiom schema. Let this system be denoted by $\mathbb {L}'\mathrm {PS}_3$. Then by the Rule 1, $\varphi (p_{k_1}) \wedge \varphi (p_{k_2}) \wedge \cdots \wedge \varphi (p_{k_m})$ is a theorem of $\mathbb {L}'\mathrm {PS}_3$. Now using M.P. we have $\sigma (p_{k_1}, p_{k_2}, \ldots , p_{k_m})$ as a theorem of the new system. Hence, the lemma is proved.

From this lemma it follows that for the enhanced system $\mathbb {L}'\mathrm {PS}_3$,

$$\begin{aligned} \Gamma \vdash _{\mathbb {L}'\mathrm {PS}_3} \varphi \text { iff } \Gamma \vdash _{\mathrm {CPL}} \varphi . \end{aligned}$$

$\square$