2 Variants for N3 and N4

In this section, we introduce the formalizations for the variants of N3 and N4 with an alternative falsity condition for implication, which we shall call DN3 and DN4. Here we shall argue in the following language $\mathcal {L}$ :

$$ \begin{align*} A ::= p\ |\ \bot\ |\ A\land A\ |\ A\lor A\ |\ A\to A\ |\ \mathord{\sim} A. \end{align*} $$

We shall use $\neg A$ and $A\leftrightarrow B$ as abbreviations for $A\to \bot $ and $(A\to B)\land (B\to A)$ , respectively. The set of formulas in $\mathcal {L}$ will be denoted by Fm, and $\equiv $ will be used for graphical equality.

2.1 Proof theory

We start with introducing the axiomatization of N3 in $\mathcal {L}$ .

Definition 2.1 (N3).

(EFQ) $$ \begin{align} \bot\to A \end{align} $$

(K) $$ \begin{align} A\to (B\to A) \end{align} $$

(S) $$ \begin{align} (A{\to}(B{\to}C)){\to}((A{\to}B){\to}(A{\to}C)) \end{align} $$

(CI) $$ \begin{align} A\to (B\to (A\land B)) \end{align} $$

(CE) $$ \begin{align} (A_{1}\land A_{2})\to A_{i} \end{align} $$

(DI) $$ \begin{align} A_{i}\to (A_{1}\lor A_{2}) \end{align} $$

(DE) $$ \begin{align} (A{\to}C){\to}((B{\to}C){\to}(A{\lor}B{\to}C)) \end{align} $$

(BF) $$ \begin{align} \mathord{\sim} \bot \end{align} $$

(CF) $$ \begin{align} \mathord{\sim}(A\land B)\leftrightarrow(\mathord{\sim} A\lor\mathord{\sim} B) \end{align} $$

(DF) $$ \begin{align} \mathord{\sim}(A\lor B)\leftrightarrow(\mathord{\sim} A\land\mathord{\sim} B) \end{align} $$

(IF) $$ \begin{align} \mathord{\sim}(A\to B)\leftrightarrow(A\land\mathord{\sim} B) \end{align} $$

(FF) $$ \begin{align} \mathord{\sim}\mathord{\sim} A\leftrightarrow A \end{align} $$

(SN) $$ \begin{align} \mathord{\sim} A\to\neg A \end{align} $$

(MP)

where $i\in \{1,2\}$ .

We shall write $\Gamma \vdash A$ if there is a finite sequence of formulas $B_{1},\ldots ,B_{n}\equiv A$ such that each $B_{i}$ is either an element of $\Gamma $ , an instance of one of the axioms, or obtained by (MP) from $B_{j}$ and $B_{k}$ where $j,k< i$ . We shall sometimes denote the proof system explicitly, e.g., $\textbf {N3}\vdash A$ . Similar remarks will apply to the other systems we shall introduce.

The system N4 Footnote ² is now defined by removing (SN) from the above axiomatization. If we further restrict the formulas of the form $\mathord {\sim } A$ to $\mathord {\sim } \bot $ Footnote ³ , and remove the axioms (BF), (CF), (DF), (IF) and (FF), then we obtain the intuitionistic propositional calculus IPC.

Now, as explained in the introduction, our intent is to replace (IF) in N3 and N4 with the following equivalence:

(IF2) $$ \begin{align} \mathord{\sim}(A\to B)\leftrightarrow(\neg\neg A\land\mathord{\sim} B) . \end{align} $$

Henceforth we shall designate the resulting systems by DN3 and DN4.

Before moving on, we have something to observe in DN3. In the system, the relationship between $\neg (A\to B)$ and $\mathord {\sim }(A\to B)$ can be made explicit by the following equivalence.

Proposition 2.2. $\textbf {DN3}\vdash \mathord {\sim }(A\to B)\leftrightarrow (\neg (A\to B)\land \mathord {\sim } B)$ .

Proof. In IPC, we can show

$$ \begin{align*} \textbf{IPC}\vdash(\neg\neg A\land\neg B)\leftrightarrow(\neg(A\to B)\land\neg B), \end{align*} $$

which consequently holds in DN3 as well. Thus by (SN),

$$ \begin{align*} \textbf{DN3}\vdash(\neg\neg A\land\mathord{\sim} B)\to \neg(A\to B),\ (\neg(A\to B)\land\mathord{\sim} B)\to \neg\neg A. \end{align*} $$

Hence it follows that $\textbf {DN3}\vdash (\neg \neg A\land \mathord {\sim } B)\leftrightarrow (\neg (A\to B)\land \mathord {\sim } B)$ . Now use (IF2) to obtain the desired equivalence.□

We may indeed take

(IF3) $$ \begin{align} \mathord{\sim}(A\to B)\leftrightarrow(\neg(A\to B)\land\mathord{\sim} B) \end{align} $$

to be the falsity condition for implication, as the resulting system is identical to DN3. However, if (SN) is absent, then the resulting system (let us name it DN4’) will turn out to be non-identical to DN4, as we shall see later.

2.2 Semantics

We next look at the semantical side of the systems. The systems DN3, DN4 and DN4’ can be characterized with Kripke semantics which are slight variants of the semantics for N3 and N4 in [Reference Gurevich10, Reference Kamide and Wansing13, Reference Thomason29]. The following completeness proof is also based on their methodology, and is similar to those of N3 and N4.

Definition 2.3 (Kripke semantics for DN3).

A Kripke frame $\mathcal {F}$ of DN3 is an inhabited pre-ordered set $(W,\leq )$ . A Kripke model $\mathcal {M}$ of DN3 is a pair $(\mathcal {F},\mathcal {V})$ where $\mathcal {V}=\{\mathcal {V}^{+},\mathcal {V}^{-}\}$ . Each $\mathcal {V}^{*}$ ( $*\in \{+,-\}$ ) is a mapping assigning a subset $\mathcal {V}^{*}(p)$ to each propositional variable p. Here each $\mathcal {V}^{*}(p)$ is required to be upward closed, i.e.,

$$ \begin{align*} w\in\mathcal{V}^{*}(p)\text{ and }w'\geq w\text{ implies }w'\in\mathcal{V}^{*}(p). \end{align*} $$

We further assume $\mathcal {V}^{+}(p)\cap \mathcal {V}^{-}(p)=\emptyset $ . Then the forcings $\Vdash ^{+}$ and $\Vdash ^{-}$ of formulas are uniquely extended from $\mathcal {V}^{+}$ and $\mathcal {V}^{-}$ by the following clauses.

$$ \begin{align*} w\Vdash^{*} p & \Leftrightarrow w\in\mathcal{V}^{*}(p).\\ w\Vdash^{+} \bot & \text{ for} \text{ no } w\in W. \\ w\Vdash^{-} \bot & \text{ for} \text{ all } w\in W.\\ w\Vdash^{+} A\land B & \Leftrightarrow w\Vdash^{+} A\text{ and }w\Vdash^{+} B.\\ w\Vdash^{-} A\land B & \Leftrightarrow w\Vdash^{-} A\text{ or }w\Vdash^{-} B.\\ w\Vdash^{+} A\lor B & \Leftrightarrow w\Vdash^{+} A\text{ or }w\Vdash^{+} B.\\ w\Vdash^{-} A\lor B & \Leftrightarrow w\Vdash^{-} A\text{ and }w\Vdash^{-} B.\\ w\Vdash^{+} A\to B & \Leftrightarrow \forall{w'\geq w}(w'\Vdash^{+} A\text{ implies }w'\Vdash^{+} B).\\ w\Vdash^{-} A\to B & \Leftrightarrow \forall{w'\geq w}\exists{w''\geq w'}(w''\Vdash^{+} A)\text{ and }w\Vdash^{-} B.\\ w\Vdash^{+} \mathord{\sim} A & \Leftrightarrow w\Vdash^{-} A.\\ w\Vdash^{-} \mathord{\sim} A & \Leftrightarrow w\Vdash^{+} A. \end{align*} $$

Occasionally we denote the model explicitly, as $\mathcal {M},w\Vdash ^{*} A$ . We shall write $\mathcal {M}\vDash A$ if $\mathcal {M},w\Vdash ^{+} A$ for all w. We shall write $\Gamma \vDash A$ if for all $\mathcal {M}$ :

$$ \begin{align*} \forall B\in\Gamma(\mathcal{M}\vDash B)\text{ implies }\mathcal{M}\vDash A. \end{align*} $$

In particular, when $\Gamma =\emptyset $ we write $\vDash A$ . When necessary, we shall denote the system explicitly, e.g., $\textbf {DN3}\vDash A$ .

We note that $w\Vdash ^{-} A\to B$ iff $w\Vdash ^{+} \neg \neg A\text { and }w\Vdash ^{-} B$ with the above condition. This is because, as in intuitionistic logic, we have:

$$ \begin{align*} w\Vdash^{+} \neg\neg A \Leftrightarrow \forall{w'\geq w}\exists{w''\geq w'}(w''\Vdash^{+} A). \end{align*} $$

In particular, if $w\Vdash ^{+}\neg \neg A$ then $w'\nVdash ^{+}\neg A$ for any $w'\geq w$ , which forces the existence of $w''\geq w$ such that $w''\Vdash ^{+}A$ . This forcing condition formalizes the informal interpretation of the falsity condition for implication discussed in the introduction.

The semantics for N3 can be obtained by making the next change to the clauses.

$$ \begin{align*} w\Vdash^{-} A\to B \Leftrightarrow(w\Vdash^{+} A\text{ and }w\Vdash^{-} B). \end{align*} $$

The semantics for N4 and DN4 are then obtained by removing the condition $\mathcal {V}^{+}(p)\cap \mathcal {V}^{-}(p)=\emptyset $ from the respective semantics. In addition, the semantics of DN4’ is obtained by altering the falsity condition of implication to:

$$ \begin{align*} w\Vdash^{-} A\to B \Leftrightarrow \forall{w'\geq w}\exists{w''\geq w'}(w''\Vdash^{+} A\text{ and }w''\nVdash^{+}B)\text{ and }w\Vdash^{-} B. \end{align*} $$

That is to say, $w\Vdash ^{+}\neg (A\to B)$ and $w\Vdash ^{-} B$ . Finally, the semantics for IPC can be obtained if we restrict the language and our attention to $\Vdash ^{+}$ alone, with the additional condition that $w\Vdash ^{+}\mathord {\sim }\bot $ always holds. In what follows, we shall omit the superscript $+$ from $\mathcal {V}^{+}$ and $\Vdash ^{+}$ when we talk about IPC.

Theorem 2.4 (Completeness of IPC).

$\Gamma \vdash A$ in IPC if and only if $\Gamma \vDash A$ in the Kripke semantics for IPC.

Proof. See [Reference Troelstra and van Dalen30].□

It is routine to establish for the semantics of DN3, DN4 and DN4’ that the forcing of a formula is closed upward, i.e.:

Proposition 2.5. For $*\in \{+,-\}$ , if $w\Vdash ^{*}A$ and $w'\geq w$ then $w'\Vdash ^{*} A$ .

Proof. By induction on the complexity of A.□

Moreover, we readily observe that the condition $\mathcal {V}^{+}(p)\cap \mathcal {V}^{-}(p)=\emptyset $ in the semantics of DN3 is extended to all formulas.

Proposition 2.6. In the semantics for DN3, for no $w$ it holds that $w\Vdash ^{+} A$ and $w\Vdash ^{-} A$ .

Proof. Again by induction on the complexity of A.□

We shall establish the completeness of DN3 with respect to the Kripke semantics via the completeness of IPC. For this purpose, we need some preparations. To begin with, we assign to each formula A its negation normal form $r(A)$ .

Definition 2.7 (Negation normal form).

We define a mapping $r:\textbf {Fm}\to \textbf {Fm}$ inductively by the following clauses.

$$ \begin{align*} r(p) & = p,\\ r(\bot) & = \bot,\\ r(A\circ B) & = r(A)\circ r(B),\\ r(\mathord{\sim} p) & = \mathord{\sim} p,\\ r(\mathord{\sim}\bot) & = \mathord{\sim} \bot, \end{align*} $$

$$ \begin{align*} r(\mathord{\sim}(A\land B)) & = r(\mathord{\sim} A)\lor r(\mathord{\sim} B),\\ r(\mathord{\sim}(A\lor B)) & = r(\mathord{\sim} A)\land r(\mathord{\sim} B),\\ r(\mathord{\sim}(A\to B)) & = \neg\neg r(A)\land r(\mathord{\sim} B),\\ r(\mathord{\sim}\mathord{\sim} A) & = r(A), \end{align*} $$

where $\circ \in \{\land ,\lor ,\to \}$ . We shall call a formula of the form $r(A)$ a reduced formula.

In the above, if we use the clause

$$ \begin{align*} r(\mathord{\sim}(A\to B)) = r(A)\land r(\mathord{\sim} B), \end{align*} $$

then we obtain the negation normal form for N3 and N4. Let us call a propositional variable or $\bot $ a prime formula. We note that $r(A)$ has all occurrences of $\mathord {\sim }$ in front of prime formulas. Moreover, we observe the next lemmas.

Lemma 2.8. $\textbf {DN3}\vdash A\leftrightarrow r(A)$ .

Proof. By induction on the complexity of A.□

Lemma 2.9. If $\textbf {DN3}\vdash A$ , then $\textbf {DN3}\vdash r(A)$ ; moreover, one may assume all the formulas in the proof are reduced. (That is, it has a reduced proof.)

Proof. By induction on the depth of derivation. That is to say, we have to show that for each axiom A, its negation normal form $r(A)$ is derivable with all the formulas in the proof reduced. Then

is an instance of (MP) and so the statement follows.

For the case for (SN), we have to argue by induction on the complexity of the formula A. When $A\equiv B\to C$ , we have to show $r(\mathord {\sim } (B\to C)\to \neg (B\to C))$ is derivable. This is syntactically equivalent to

$$ \begin{align*} (\neg\neg r(B)\land r(\mathord{\sim} C))\to\neg(r(B)\to r(C)). \end{align*} $$

By I.H., there is a reduced proof of $r(\mathord {\sim } C)\to \neg r(C)$ . Also

$$ \begin{align*} \neg r(C)\to (\neg\neg r(B)\to \neg(r(B)\to r(C))) \end{align*} $$

is an instance of an intuitionistically derivable formula; so the proof can be assumed to be reduced. Then it is easy to construct a reduced proof of $(\neg \neg r(B)\land r(\mathord {\sim } C))\to \neg (r(B)\to r(C))$ .□

Let $A[\mathord {\sim } p_{1},\ldots , \mathord {\sim } p_{n}]$ be a reduced formula, with the occurrences of subformulas of the form $\mathord {\sim } p$ marked by $\mathord {\sim } p_{1},\ldots , \mathord {\sim } p_{n}$ . We shall assume that for each $p_{i}$ there is a new propositional variable $q_{i}$ in the language of IPC. Then we define a formula

$$ \begin{align*} E:=\bigwedge_{1\leq i\leq n}(q_{i}\to\neg p_{i}). \end{align*} $$

This allows us to assert the next proposition, which is analogous to the case for N3 originally treated by Vorob’ev [Reference Vorob’ev31].Footnote ⁴

Proposition 2.10. Let $A[\mathord {\sim } p_{1},\ldots , \mathord {\sim } p_{n}]$ be a reduced formula. Then the following are equivalent.

1. (i) $\textbf {DN3}\vdash A[\mathord {\sim } p_{1},\ldots , \mathord {\sim } p_{n}]$ .

2. (ii) $\textbf {IPC}\vdash E\to A[\mathord {\sim } p_{1},\ldots , \mathord {\sim } p_{n}/q_{1},\ldots , q_{n}]$ .

Proof. From (i) to (ii), first note that we can w.l.o.g. assume all the formulas of the form $\mathord {\sim } p$ occurring in the derivation occurs in $A[\mathord {\sim } p_{1},\ldots , \mathord {\sim } p_{n}]$ ; for otherwise we can consider the derivation of an equivalent formula

$$ \begin{align*} A[\mathord{\sim} p_{1},\ldots, \mathord{\sim} p_{n}]\land(\mathord{\sim} p\to\mathord{\sim} p), \end{align*} $$

whose reduced proof requires no more occurrences of formulas of the mentioned form. With this proviso it is sufficient to observe that a reduced proof in DN3 can be replicated in IPC with the aid of E. In particular, for the axiom $\mathord {\sim } B\to \neg B$ , because the proof is reduced, B has to be prime. If $B\equiv \bot $ , then $\mathord {\sim }\bot \to \neg \bot $ is a theorem of IPC (recall $\mathord {\sim }\bot $ is in the language of $\textbf {IPC}$ ); if $B\equiv p_{i}$ for some $1\leq i\leq n$ (as we may assume by the comment above), then

$$ \begin{align*} \textbf{IPC}\vdash (q_{i}\to\neg p_{i})\to((\mathord{\sim} p_{i}\to\neg p_{i})[\mathord{\sim} p_{i}/q_{i}]), \end{align*} $$

and so E is sufficient for the replication.

From (ii) to (i), if

$$ \begin{align*} \textbf{IPC}\vdash E\to A[q_{1},\ldots, q_{n}], \end{align*} $$

then DN3 can replicate the proof except for the unavailable propositional variables $q_{1},\ldots , q_{n}$ . Therefore we replace the occurrences of $q_{1},\ldots , q_{n}$ by $\mathord {\sim } p_{1},\ldots , \mathord {\sim } p_{n}$ from the proof in IPC, which allows us to obtain the proof witnessing

$$ \begin{align*} \textbf{DN3}\vdash (E\to A)[q_{1},\ldots, q_{n}/\mathord{\sim} p_{1},\ldots, \mathord{\sim} p_{n}]. \end{align*} $$

That is, $\textbf {DN3}\vdash A[\mathord {\sim } p_{1},\ldots , \mathord {\sim } p_{n}]$ .□

Now we are ready to establish the soundness and completeness of DN3 with the Kripke semantics. Firstly, it is straightforward to check the soundness direction.

Theorem 2.11 (Soundness of DN3).

If $\textbf {DN3}\vdash A$ then $\textbf {DN3}\vDash A$ .

Proof. By induction on the depth of derivation. In particular, the case for (SN) follows from Proposition 2.6.□

For the completeness, we shall use the next lemma.

Lemma 2.12.

1. (i) $w\Vdash ^{+}A$ if and only if $w\Vdash ^{+} r(A)$ .

2. (ii) $w\Vdash ^{-}A$ if and only if $w\Vdash ^{+} r(\mathord {\sim } A)$ .

Proof. By simultaneous induction on the complexity of A. For instance, in (ii), if $A\equiv B\to C$ , $w\Vdash ^{-} B\to C$ iff $w\Vdash ^{+}\neg \neg B$ and $w\Vdash ^{-}C$ . By I.H. this is equivalent to $w\Vdash ^{+}\neg \neg r(B)$ and $w\Vdash ^{+} r(\mathord {\sim } C)$ , which is by definition equivalent to $w\Vdash ^{+} r(\mathord {\sim }(B\to C))$ .□

Theorem 2.13 (Completeness of DN3).

If $\textbf {DN3}\vDash A$ then $\textbf {DN3}\vdash A$ .

Proof. We prove the contrapositive. Suppose $\textbf {DN3}\nvdash A$ . Then by Lemma 2.8,

$$ \begin{align*} \textbf{DN3}\nvdash r(A)[\mathord{\sim} p_{1},\ldots,\mathord{\sim} p_{n}]. \end{align*} $$

Then by Proposition 2.10 and the deduction theorem for IPC,

$$ \begin{align*} E\nvdash r(A)[\mathord{\sim} p_{1},\ldots,\mathord{\sim} p_{n}/q_{1},\ldots,q_{n}] \end{align*} $$

in IPC. Hence by the completeness of IPC,

$$ \begin{align*} E\nvDash r(A)[\mathord{\sim} p_{1},\ldots,\mathord{\sim} p_{n}/q_{1},\ldots,q_{n}] \end{align*} $$

in the Kripke semantics for IPC. That is, there is a model $(\mathcal {F},\mathcal {V})$ of IPC and a world w such that

$$ \begin{align*} (\mathcal{F},\mathcal{V})\vDash E, \end{align*} $$

but

$$ \begin{align*} (\mathcal{F},\mathcal{V}),w\nVdash r(A)[\mathord{\sim} p_{1},\ldots,\mathord{\sim} p_{n}/q_{1},\ldots,q_{n}]. \circledast. \end{align*} $$

Then we construct a corresponding model of DN3 $(\mathcal {F}_{2},\mathcal {V}_{2})$ such that

• • $\mathcal {F}_{2}=\mathcal {F}$ ;

• • $u\in \mathcal {V}^{+}_{2}(p_{i})\text { iff }u\in \mathcal {V}(p_{i})$ ;

• • $u\in \mathcal {V}^{-}_{2}(p_{i})\text { iff }u\in \mathcal {V}(q_{i})$ .

Note here if $u\in \mathcal {V}^{+}_{2}(p_{i})\cap \mathcal {V}^{-}_{2}(p_{i})$ then $(\mathcal {F},\mathcal {V}),u\Vdash p_{i}\land q_{i}$ , so $(\mathcal {F},\mathcal {V}),u\Vdash \bot $ , a contradiction. Hence $\mathcal {V}^{+}_{2}(p_{i})\cap \mathcal {V}^{-}_{2}(p_{i})=\emptyset $ , and consequently $(\mathcal {F}_{2},\mathcal {V}_{2})$ is well-defined.

Now it suffices to observe (by an easy induction on the complexity of the formula) that for any subformula $B$ of $r(A)$ ,

$$ \begin{align*} (\mathcal{F},\mathcal{V}),w\Vdash B[\mathord{\sim} p_{1},\ldots,\mathord{\sim} p_{n}/q_{1},\ldots, q_{n}]\text{ iff }(\mathcal{F}_{2},\mathcal{V}_{2}),w\Vdash^{+} B, \end{align*} $$

because then $\circledast $ implies $(\mathcal {F}_{2},\mathcal {V}_{2}),w\nVdash ^{+} r(A)$ and so $(\mathcal {F}_{2},\mathcal {V}_{2}),w\nVdash ^{+} A$ by Lemma 2.12.□

The soundness and completeness for DN4 and DN4’ are provable in a similar manner. For DN4’, the notion of negation normal form is altered to

$$ \begin{align*} r(\mathord{\sim}(A\to B))=\neg r(A\to B)\land r(\mathord{\sim} B). \end{align*} $$

In addition, for both DN4 and DN4’, E is not assumed in establishing the equivalence in the analogue of Proposition 2.10. Thence we establish the relationship between the two systems.

Proposition 2.14. DN4 and DN4’ are incomparable.

Proof. We claim

$$ \begin{align*} \textbf{DN4}\nvdash\mathord{\sim}(p\to q)\to(\neg(p\to q)\land\mathord{\sim} q) \end{align*} $$

and

$$ \begin{align*} \textbf{DN4'}\nvdash(\neg\neg p\land\mathord{\sim} q)\to\mathord{\sim}(p\to q). \end{align*} $$

For this purpose, take the next model $(\mathcal {F},\mathcal {V})$ of IPC refuting $\neg \neg p\to \neg (p\to q)$ .

• • $W=\{w\}$ ;

• • $\mathcal {V}(p)=\mathcal {V}(q)=W$ .

Then construct a model $(\mathcal {F}_{2},\mathcal {V}_{2})$ of DN4’ by letting

• • $\mathcal {F}_{2}=\mathcal {F}$ ;

• • $\mathcal {V}^{+}_{2}=\mathcal {V}$ and $\mathcal {V}^{-}_{2}(q)=W$ .

Then $(\mathcal {F}_{2},\mathcal {V}_{2}),w\Vdash ^{+}\neg \neg p\land \mathord {\sim } q$ , but $(\mathcal {F}_{2},\mathcal {V}_{2}),w\nVdash ^{+}\neg (p\to q)\land \mathord {\sim } q$ . Hence

$$ \begin{align*} (\mathcal{F}_{2},\mathcal{V}_{2})\nvDash \mathord{\sim}(p\to q)\to(\neg(p\to q)\land\mathord{\sim} q). \end{align*} $$

So by soundness

$$ \begin{align*} \textbf{DN4}\nvdash\mathord{\sim}(p\to q)\to(\neg(p\to q)\land\mathord{\sim} q). \end{align*} $$

Similarly we can show

$$ \begin{align*} \textbf{DN4'}\nvdash(\neg\neg p\land\mathord{\sim} q)\to\mathord{\sim}(p\to q). \end{align*} $$

□

The above in particular implies that while

$$ \begin{align*} \textbf{DN4'}\vdash\mathord{\sim}(A\to B)\to\neg (A\to B), \end{align*} $$

(SN) in full generality is not derivable in DN4’, because then it would be identical to DN3, which contains DN4.

From this point on, we shall occasionally write DN4(’) to mean both DN4 and DN4’, to state propositions that hold for both of the systems. Before moving on, we observe the constructible falsity property for the systems as a special case for disjunction property, which can be proved by a semantical argument as in IPC.

Theorem 2.15 (Disjunction property).

1. (i) $\textbf {DN3}\vdash A\lor B$ then $\textbf {DN3}\vdash A$ or $\textbf {DN3}\vdash B$ .

2. (ii) $\textbf {DN4(')}\vdash A\lor B$ then $\textbf {DN4(')}\vdash A$ or $\textbf {DN4(')}\vdash B$ .

Proof. We prove by contradiction. Since IPC is complete with respect to rooted frames (i.e., frames with the least element), DN3 and DN4(’) are complete with respect to rooted frames as well. Now suppose $\textbf {DN3}\vdash A_{1}\lor A_{2}$ , but $\textbf {DN3}\nvdash A_{1}$ and $\textbf {DN3}\nvdash A_{2}$ . Then by completeness, there are models $(\mathcal {F}_{i},\mathcal {V}_{i})$ and the worlds $r_{i}$ , where $i\in \{1,2\}$ and $(\mathcal {F}_{i},\mathcal {V}_{i}),r_{i}\nVdash ^{+} A_{i}$ . We may assume $r_{i}$ to be the least element of the set $W_{i}$ of the respective model. Then define a new model $(\mathcal {F}_{3},\mathcal {V}_{3})$ by taking $W_{3}=W_{1}\cup W_{2}\cup \{r_{3}\}$ , where $r_{3}$ is a new least element of $W_{3}$ . Set

$$ \begin{align*} r_{3}\in\mathcal{V}^{*}_{3}(p)\text{ iff }W_{1}=\mathcal{V}^{*}_{1}(p)\text{ and }W_{2}=\mathcal{V}^{*}_{2}(p). \end{align*} $$

If $w\neq r_{3}$ and $w\in W_{i}$ , set

$$ \begin{align*} w\in\mathcal{V}^{*}_{3}(p)\text{ iff }w\in\mathcal{V}^{*}_{i}(p). \end{align*} $$

It is easy to check $\mathcal {V}^{*}_{3}(p)$ is upward closed, and $\mathcal {V}^{+}_{3}(p)\cap \mathcal {V}^{-}_{3}(p)=\emptyset $ . Now since $\textbf {DN3}\vdash A_{1}\lor \ A_{2}$ , by soundness

$$ \begin{align*} (\mathcal{F}_{3},\mathcal{V}_{3}),r_{3}\Vdash^{+} A_{1}\text{ or }(\mathcal{F}_{3},\mathcal{V}_{3}),r_{3}\Vdash^{+} A_{2}. \end{align*} $$

On the other hand, $(\mathcal {F}_{3},\mathcal {V}_{3}),r_{i}\nVdash ^{+} A_{i}$ from our choice of $\mathcal {V}^{+}_{3}$ , a contradiction. The case for DN4(’) is similar.□

Corollary 2.16 (Constructible falsity).

1. (i) $\textbf {DN3}\vdash \mathord {\sim }(A\land \ B)$ then $\textbf {DN3}\vdash \mathord {\sim } A$ or $\textbf {DN3}\vdash \mathord {\sim } B$ .

2. (ii) $\textbf {DN4(')}\vdash \mathord {\sim }(A\land \ B)$ then $\textbf {DN4(')}\vdash \mathord {\sim } A$ or $\textbf {DN4(')}\vdash \mathord {\sim } B$ .

Proof. Immediate from the previous theorem and (CF).□

3 Properties of DN3 and DN4(’)

In this section, we look at the properties of DN3 and DN4(’) in order to demonstrate the advantages of the logics compared with N3 and N4.

We begin with observing how the alternation in the falsity condition for implication allows the strong negation to retain more similarity with intuitionistic negation. More precisely, we shall see that the equivalence of strong and intuitionistic negation can be shown for a wider class of formulas, once we assume the equivalence for the atomic formulas.Footnote ⁵ For this purpose, we consider a limited language $\mathcal {L^{*}}$ , which does not contain $\land $ and $\mathord {\sim }$ that allow inferences not allowed for intuitionistic negation.

$$ \begin{align*} A ::= p\ |\ \bot\ |\ A\lor A\ |\ A\to A. \end{align*} $$

Then we shall see $\neg A$ and $\mathord {\sim } A$ become equivalent if we assume the equivalence between $\neg p$ and $\mathord {\sim } p$ for each p from a certain subset of the set of all propositional variables occurring in A.

Definition 3.17. Let A be a formula in $\mathcal {L}^{*}$ . We inductively define a class $\Gamma _{A}$ by the following clauses:

$$ \begin{align*} \Gamma_{p} & \equiv \{p\}, \quad \Gamma_{A\lor B} \equiv \Gamma_{A}\cup\Gamma_{B},\\ \Gamma_{\bot} & \equiv \emptyset,\quad \Gamma_{A\to B} \equiv \Gamma_{B}. \end{align*} $$

Now let

$$ \begin{align*} \mathcal{I}_{A}:=\{\neg p\to\mathord{\sim} p:p\in \Gamma_{A}\}\text{ and } \mathcal{E}_{A}:=\{\neg p\leftrightarrow\mathord{\sim} p:p\in \Gamma_{A}\}. \end{align*} $$

Then we observe that $\neg A$ and $\mathord {\sim } A$ become equivalent under a suitable class of assumptions and a restriction on language.

Proof. Here we prove for DN3; the case for DN4(’) is analogous. We show by induction on the complexity of A.

When $A\equiv p$ , then $\mathcal {I}_{p}=\{\neg p\to \mathord {\sim } p\}$ . Thus the statements hold, as $\neg p\to \mathord {\sim } p\vdash \neg p\to \mathord {\sim } p$ .

When $A\equiv \bot $ , then $\vdash \neg \bot \to \mathord {\sim }\bot $ , hence $\mathcal {I}_{\bot }=\emptyset $ suffices.

When $A\equiv B\lor C$ , then $\mathcal {I}_{A}=\mathcal {I}_{B}\cup \mathcal {I}_{C}$ . By I.H.

$$ \begin{align*} \mathcal{I}_{B}\vdash\neg B\to\mathord{\sim} B\text{ and }\mathcal{I}_{C}\vdash\neg C\to\mathord{\sim} C. \end{align*} $$

Since $\neg (B\lor C)\leftrightarrow (\neg B\land \neg C)$ holds in IPC, it follows that

$$ \begin{align*} \mathcal{I}_{A}\vdash\neg (B\lor C)\to\mathord{\sim} (B\lor C). \end{align*} $$

When $A\equiv B\to C$ , then $\mathcal {I}_{A}=\mathcal {I}_{C}$ . Then by I.H.

$$ \begin{align*} \mathcal{I}_{C}\vdash(\neg\neg B\land\neg C)\to(\neg\neg B\land\mathord{\sim} C). \end{align*} $$

Hence in view of the fact that $\textbf {IPC}\vdash \neg (B\to C)\leftrightarrow (\neg \neg B\land \neg C)$ , it follows that

$$ \begin{align*} \mathcal{I}_{A}\vdash\neg(B\to C)\to\mathord{\sim}(B\to C).\\[-36pt] \end{align*} $$

□

On the other hand, clearly $\neg p\leftrightarrow \mathord {\sim } p\nvdash \neg \neg p\to \mathord {\sim }\neg p$ in N3 and N4, since $\mathord {\sim }\neg p$ is equivalent to p in N3 and N4. Hence the difference between the cases for N3 and N4 is the inclusion of implication, which is significant as a fragment.

We next give an example of formulas provable in DN3 and DN4(’) but not in N3 nor N4.

It is apparent that $\mathord {\sim }\neg (A\lor \neg A)$ is not provable in N3 nor N4, because it is equivalent to $A\lor \neg A$ . On the other hand, it is straightforward to check that $\mathord {\sim }\neg p\to p$ is provable in N3 and N4 but not in DN3 nor DN4(’). Hence N3 and DN3 are incomparable, and similarly for N4 and DN4(’).

Nonetheless, we can still establish a certain relationship between the systems, with the exception of DN4’. For this we first require establishing a Glivenko-like lemma.

Proof. We argue by induction on the depth of deduction. In each case, it suffices to show the derivability of

$$ \begin{align*} \neg\neg(\mathord{\sim}(A\to B)\leftrightarrow(A\land\mathord{\sim} B)) \end{align*} $$

in the target system. Since $\textbf {IPC}\vdash \neg \neg (A\leftrightarrow B)\leftrightarrow (\neg \neg A\leftrightarrow \neg \neg B)$ , we aim to show

$$ \begin{align*} \neg\neg\mathord{\sim}(A\to B)\to\neg\neg(A\land\mathord{\sim} B) \end{align*} $$

and

$$ \begin{align*} \neg\neg(A\land\mathord{\sim} B)\to\neg\neg\mathord{\sim}(A\to B). \end{align*} $$

Indeed, the latter is an immediate consequence of

$$ \begin{align*} (A\land\mathord{\sim} B)\to\mathord{\sim}(A\to B). \end{align*} $$

As for the former, note $\neg \neg \mathord {\sim }(A\to B)\leftrightarrow \neg \neg (\neg \neg A\land \mathord {\sim } B)$ holds in both DN3 and DN4. Then as $\textbf {IPC}\vdash \neg \neg (A\land B)\leftrightarrow (\neg \neg A\land \neg \neg B)$ ,

$$ \begin{align*} \neg\neg\mathord{\sim}(A\to B)\to(\neg\neg A\land\neg\neg\mathord{\sim} B), \end{align*} $$

and using the above equivalence again, we obtain $\neg \neg \mathord {\sim }(A\to B)\to \neg \neg (A\land \mathord {\sim } B)$ as desired.□

Now we can infer the next theorem, showing that any formulas in the language of IPC (i.e., not containing $\mathord {\sim }$ except for $\mathord {\sim }\bot $ ) refutable in N3 and N4 are also refutable in $\textbf {DN3}$ and $\textbf {DN4}$ . Given the preceding observation that $\mathord {\sim }\neg (A\lor \neg A)$ is refutable only in the latter pair, we can conclude that they refute strictly more propositions that are in the language of IPC than N3 and N4.

Proof. Here we look at the case for N3. The case for N4 is analogous. We prove by induction on the complexity of A.

When $A\equiv p$ , then $\mathord {\sim } p$ is not a theorem of N3, so the statement vacuously holds. Similarly when $A\equiv \mathord {\sim }\bot $ .

When $A\equiv \bot $ , then $\textbf {DN3}\vdash \mathord {\sim }\bot $ .

When $A\equiv B\land C$ , then if $\textbf {N3}\vdash \mathord {\sim } (B\land C)$ , either

$$ \begin{align*} \textbf{N3}\vdash \mathord{\sim} B\text{ or }\textbf{N3}\vdash \mathord{\sim} C, \end{align*} $$

by the constructive falsity property of N3. Thus by I.H.

$$ \begin{align*} \textbf{DN3}\vdash \mathord{\sim} B\text{ or }\textbf{DN3}\vdash \mathord{\sim} C, \end{align*} $$

and so $\textbf {DN3}\vdash \mathord {\sim } (B\land C)$ in each case.

When $A\equiv B\lor C$ , then if $\textbf {N3}\vdash \mathord {\sim } (B\lor C)$ ,

$$ \begin{align*} \textbf{N3}\vdash \mathord{\sim} B\text{ and }\textbf{N3}\vdash \mathord{\sim} C, \end{align*} $$

and so by I.H.

$$ \begin{align*} \textbf{DN3}\vdash \mathord{\sim} B\text{ and }\textbf{DN3}\vdash \mathord{\sim} C. \end{align*} $$

Hence $\textbf {DN3}\vdash \mathord {\sim } (B\lor C)$ .

When $A\equiv B\to C$ , then if $\textbf {N3}\vdash \mathord {\sim } (B\to C)$ ,

$$ \begin{align*} \textbf{N3}\vdash B\text{ and }\textbf{N3}\vdash \mathord{\sim} C. \end{align*} $$

Then by I.H. and Lemma 3.20

$$ \begin{align*} \textbf{DN3}\vdash \neg\neg B\text{ and }\textbf{DN3}\vdash \mathord{\sim} C, \end{align*} $$

and so $\textbf {DN3}\vdash \mathord {\sim } (B\to C)$ .□

Note here that the above theorem cannot be extended to the full language, because when $A\equiv \mathord {\sim } B$ , we would need $\textbf {N3}\vdash B$ implying $\textbf {DN3}\vdash B$ .

Before moving on to another topic, let us look back at Lemma 3.20. Unlike Glivenko’s theorem, in each case we cannot show the converse direction, for $\neg \neg (A\lor \neg A)$ is intuitionistically derivable but not $A\lor \neg A$ . However, we may still observe a correspondence for propositions of the form $\neg A$ . In order to state the next result, we shall use $\Vdash _{\textbf {N4}}$ and $\Vdash _{\textbf {DN4}}$ for the forcings of the respective semantics, and $r_{1}$ and $r_{2}$ for the negation normal forms in N4 and DN4, respectively. Also note that a model of N3 or N4 can be seen as a model of DN3 and DN4 but with a different forcing condition.

Lemma 3.22. Let $\mathcal {M}=(\mathcal {F},\mathcal {V})$ be a model of N4. Then for any A and any world w in the model,

$$ \begin{align*} \mathcal{M},w\Vdash^{+}_{\textbf{N4}}\neg r_{1}(A)\text{ if and only if }\mathcal{M},w\Vdash^{+}_{\textbf{DN4}}\neg r_{2}(A). \end{align*} $$

Proof. We prove by induction on the complexity of A.

If $A\equiv p$ , then $r_{1}(A)= r_{2}(A)= p$ . We have $\mathcal {M},w\Vdash ^{+}_{\textbf {N4}}\neg p$ if and only if $\forall w'\geq w(w'\notin \mathcal {V}^{+}(p))$ if and only if $\mathcal {M},w\Vdash ^{+}_{\textbf {DN4}}\neg p$ .

If $A\equiv \bot $ , then $r_{1}(A)= r_{2}(A)= \bot $ , and $\mathcal {M},w\Vdash ^{+}_{\textbf {N4}}\neg \bot $ and $\mathcal {M},w\Vdash ^{+}_{\textbf {DN4}}\neg \bot $ hold for all w.

If $A\equiv B\land C$ , then $r_{i}(A)= r_{i}(B)\land r_{i}(C)$ for $i\in \{1,2\}$ . By I.H.,

$$ \begin{align*} \mathcal{M},w\Vdash^{+}_{\textbf{N4}}\neg r_{1}(B) & \text{ if and only if } \mathcal{M},w\Vdash^{+}_{\textbf{DN4}}\neg r_{2}(B),\\ \mathcal{M},w\Vdash^{+}_{\textbf{N4}}\neg r_{1}(C) & \text{ if and only if } \mathcal{M},w\Vdash^{+}_{\textbf{DN4}}\neg r_{2}(C). \end{align*} $$

We need to show

$$ \begin{align*} \mathcal{M},w\Vdash^{+}_{\textbf{N4}}\neg (r_{1}(B)\land r_{1}(C))\text{ if and only if }\mathcal{M},w\Vdash^{+}_{\textbf{DN4}}\neg (r_{2}(B)\land r_{2}(C)). \end{align*} $$

For the left-to-right direction, assume $\mathcal {M},w\Vdash ^{+}_{\textbf {N4}}\neg (r_{1}(B)\land r_{1}(C))$ . Suppose that $\mathcal {M},w'\Vdash ^{+}_{\textbf {DN4}} r_{2}(B)\land r_{2}(C)$ for $w'\geq w$ . Then if $\mathcal {M},w''\Vdash ^{+}_{\textbf {N4}}\neg r_{1}(B)$ for $w''\geq w'$ , by I.H. $\mathcal {M},w''\Vdash ^{+}_{\textbf {DN4}}\neg r_{2}(B)$ , a contradiction. Hence $\mathcal {M},w'\Vdash ^{+}_{\textbf {N4}}\neg \neg r_{1}(B)$ . Similarly $\mathcal {M},w'\Vdash ^{+}_{\textbf {N4}}\neg \neg r_{1}(C)$ . Consequently $\mathcal {M},w'\Vdash ^{+}_{\textbf {N4}}\neg \neg (r_{1}(B)\land r_{1}(C))$ , another contradiction. Therefore $\mathcal {M},w\Vdash ^{+}_{\textbf {DN4}}\neg (r_{2}(B)\land r_{2}(C))$ . The converse direction is analogous.

If $A\equiv B\lor C$ , then $r_{i}(A)= r_{i}(B)\lor r_{i}(C)$ for $i\in \{1,2\}$ . We have the same I.H. as the previous case. We need to show

$$ \begin{align*} \mathcal{M},w\Vdash^{+}_{\textbf{N4}}\neg (r_{1}(B)\lor r_{1}(C))\text{ if and only if }\mathcal{M},w\Vdash^{+}_{\textbf{DN4}}\neg (r_{2}(B)\lor r_{2}(C)). \end{align*} $$

For the left-to-right direction, assume $\mathcal {M},w\Vdash ^{+}_{\textbf {N4}}\neg (r_{1}(B)\lor r_{1}(C))$ . Then $\mathcal {M},w\Vdash ^{+}_{\textbf {N4}}\neg r_{1}(B)$ and $\mathcal {M},w\Vdash ^{+}_{\textbf {N4}}\neg r_{1}(C)$ . Hence by I.H. $\mathcal {M},w\Vdash ^{+}_{\textbf {DN4}}\neg r_{2}(B)$ and $\mathcal {M},w\Vdash ^{+}_{\textbf {DN4}}\neg r_{2}(C)$ . Therefore $\mathcal {M},w\Vdash ^{+}_{\textbf {DN4}}\neg (r_{2}(B)\lor r_{2}(C))$ . The converse direction is analogous.

If $A\equiv B\to C$ , then $r_{i}(A)= r_{i}(B)\to r_{i}(C)$ for $i\in \{1,2\}$ . We have the same I.H. as the previous case. We need to show

$$ \begin{align*} \mathcal{M},w\Vdash^{+}_{\textbf{N4}}\neg (r_{1}(B)\to r_{1}(C))\text{ if and only if }\mathcal{M},w\Vdash^{+}_{\textbf{DN4}}\neg (r_{2}(B)\to r_{2}(C)). \end{align*} $$

For the left-to-right direction, assume $\mathcal {M},w\Vdash ^{+}_{\textbf {N4}}\neg (r_{1}(B)\to r_{1}(C))$ . Suppose $\mathcal {M},w'\Vdash ^{+}_{\textbf {DN4}} r_{2}(B)\to r_{2}(C)$ for $w'\geq w$ . Then if $\mathcal {M},w''\Vdash ^{+}_{\textbf {N4}}\neg r_{1}(C)$ for $w''\geq w'$ , by I.H. $\mathcal {M},w''\Vdash ^{+}_{\textbf {DN4}}\neg r_{2}(C)$ . Hence by our supposition $\mathcal {M},w''\Vdash ^{+}_{\textbf {DN4}}\neg r_{2}(B)$ . By I.H. again, $\mathcal {M},w''\Vdash ^{+}_{\textbf {N4}}\neg r_{1}(B)$ . Thus $\mathcal {M},w'\Vdash ^{+}_{\textbf {N4}}\neg r_{1}(C)\to \neg r_{1}(B)$ . So $\mathcal {M},w'\Vdash ^{+}_{\textbf {N4}}\neg \neg (r_{1}(B)\to r_{1}(C))$ , which contradicts with our assumption. Therefore $\mathcal {M},w\Vdash ^{+}_{\textbf {DN4}} \neg (r_{2}(B)\to r_{2}(C))$ . The converse direction is analogous.

If $A\equiv \mathord {\sim } B$ , we argue by induction on the complexity of B.

If $B\equiv p$ , then $r_{i}(A)= \mathord {\sim } p$ for $i\in \{1,2\}$ . We have $\mathcal {M},w\Vdash ^{+}_{\textbf {N4}}\neg \mathord {\sim } p$ if and only if $\forall w'\geq w(w'\notin \mathcal {V}^{-}(p))$ if and only if $\mathcal {M},w\Vdash ^{+}_{\textbf {DN4}}\neg \mathord {\sim } p$ .

If $B\equiv \bot $ , then $r_{1}(A)= r_{2}(A)= \mathord {\sim }\bot $ , and $\mathcal {M},w\Vdash ^{+}_{\textbf {N4}}\neg \mathord {\sim } \bot $ and $\mathcal {M},w\Vdash ^{+}_{\textbf {DN4}}\neg \mathord {\sim } \bot $ never hold for any w.

If $B\equiv C\land D$ , then $r_{i}(A)= r_{i}(\mathord {\sim } C)\lor r_{i}(\mathord {\sim } D)$ for $i\in \{1,2\}$ . By I.H.

$$ \begin{align*} \mathcal{M},w\Vdash^{+}_{\textbf{N4}}\neg r_{1}(\mathord{\sim} C) & \text{ if and only if } \mathcal{M},w\Vdash^{+}_{\textbf{DN4}}\neg r_{2}(\mathord{\sim} C),\\ \mathcal{M},w\Vdash^{+}_{\textbf{N4}}\neg r_{1}(\mathord{\sim} D) & \text{ if and only if } \mathcal{M},w\Vdash^{+}_{\textbf{DN4}}\neg r_{2}(\mathord{\sim} D). \end{align*} $$

We need to show

$$ \begin{align*} \mathcal{M},w\Vdash^{+}_{\textbf{N4}}\neg (r_{1}(\mathord{\sim} C)\lor r_{1}(\mathord{\sim} D))\text{ if and only if }\mathcal{M},w\Vdash^{+}_{\textbf{DN4}}\neg (r_{2}(\mathord{\sim} C)\lor r_{2}(\mathord{\sim} D)). \end{align*} $$

The case is thus similar to the case $A\equiv B\lor C$ .

If $B\equiv C\lor D$ , then $r_{i}(A)= r_{i}(\mathord {\sim } C)\land r_{i}(\mathord {\sim } D)$ for $i\in \{1,2\}$ . We have the same I.H. as the previous case. We need to show

$$ \begin{align*} \mathcal{M},w\Vdash^{+}_{\textbf{N4}}\neg (r_{1}(\mathord{\sim} C)\land r_{1}(\mathord{\sim} D))\text{ if and only if }\mathcal{M},w\Vdash^{+}_{\textbf{DN4}}\neg (r_{2}(\mathord{\sim} C)\land r_{2}(\mathord{\sim} D)). \end{align*} $$

The case is thus similar to the case $A\equiv B\land C$ .

If $B\equiv C\to D$ , then $r_{1}(A)= r_{1}(C)\land r_{1}(\mathord {\sim } D)$ and $r_{2}(A)= \neg \neg r_{2}(C)\land r_{2}(\mathord {\sim } D)$ . By I.H.,

$$ \begin{align*} \mathcal{M},w\Vdash^{+}_{\textbf{N4}}\neg r_{1}(C) & \text{ if and only if } \mathcal{M},w\Vdash^{+}_{\textbf{DN4}}\neg r_{2}(C),\\ \mathcal{M},w\Vdash^{+}_{\textbf{N4}}\neg r_{1}(\mathord{\sim} D) & \text{ if and only if } \mathcal{M},w\Vdash^{+}_{\textbf{DN4}}\neg r_{2}(\mathord{\sim} D). \end{align*} $$

We need to show

$$ \begin{align*} \mathcal{M},w\Vdash^{+}_{\textbf{N4}}\neg (r_{1}(C)\land r_{1}(\mathord{\sim} D))\text{ if and only if }\mathcal{M},w\Vdash^{+}_{\textbf{DN4}}\neg (\neg\neg r_{2}(C)\land r_{2}(\mathord{\sim} D)). \end{align*} $$

We first note that (because both formulas equal $r_{2}(\mathord {\sim } D)\to \neg r_{2}(\mathord {\sim } C)$ )

$$ \begin{align*} \mathcal{M},w\Vdash^{+}_{\textbf{DN4}}\neg (\neg\neg r_{2}(C)\land r_{2}(\mathord{\sim} D))\text{ if and only if }\mathcal{M},w\Vdash^{+}_{\textbf{DN4}}\neg ( r_{2}(C)\land r_{2}(\mathord{\sim} D)). \end{align*} $$

Hence it suffices to show

$$ \begin{align*} \mathcal{M},w\Vdash^{+}_{\textbf{N4}}\neg (r_{1}(C)\land r_{1}(\mathord{\sim} D))\text{ if and only if }\mathcal{M},w\Vdash^{+}_{\textbf{DN4}}\neg ( r_{2}(C)\land r_{2}(\mathord{\sim} D)). \end{align*} $$

Thus the case is similar to the case $A\equiv B\land C$ .

If $B\equiv \mathord {\sim } C$ , then $r_{i}(A)= r_{i}(C)$ for $i\in \{1,2\}$ . We need to show

$$ \begin{align*} \mathcal{M},w\Vdash^{+}_{\textbf{N4}}\neg r_{1}(C)\text{ if and only if }\mathcal{M},w\Vdash^{+}_{\textbf{DN4}}\neg r_{2}(C), \end{align*} $$

which already holds by I.H.□

In particular, the statement holds between N3 and DN3, since a model of N3 is a model of N4. Then we can demonstrate the next theorem.

Moving on to the next topic, a notable feature of N3 and N4 is that they do not allow the contraposition of an implication.Footnote ⁶ For DN3 and DN4(’), they are still not provable. However it is provable in partial forms.

Proof. For (i), by a theorem of IPC,

$$ \begin{align*} \textbf{DN3}\vdash (\neg A\to B)\to(\neg B\to\neg\neg A). \end{align*} $$

Then by (SN) and Proposition 3.19 we obtain the stated formula. For (ii), similarly we have

$$ \begin{align*} \textbf{DN4(')}\vdash (\neg A\to \neg B)\to(\neg \neg B\to\neg\neg A). \end{align*} $$

Then use Proposition 3.19 for both $\neg \neg B$ and $\neg \neg A$ .□

In comparison, N3 and N4 do not prove $(\neg A\to \neg B)\to (B\to A)$ , so we can see that the same restrictions do not work. On the other hand, we can derive $(A\to B)\to (\mathord {\sim } B\to \mathord {\sim }\neg \neg A)$ and $(A\to B)\to (\mathord {\sim }\neg \neg B\to \mathord {\sim }\neg \neg A)$ in N3 and N4, respectively. However it is easy to check that each of the formulas is also derivable respectively in DN3 and DN4. Hence DN3 and DN4(’) seem to fare better in this regard.

4 Law of excluded middle for strong negation in DN4(’)

As is well-known, the addition of the law of excluded middle over intuitionistic logic defines classical logic. Similarly, the addition of the law of excluded middle for strong negation, i.e.,

$$ \begin{align*} A\lor\mathord{\sim} A \end{align*} $$

to N3 will result in classical logic, as the strong negation becomes identical to the classical negation. The situation does not change when we move from N3 to DN3; from $A\lor \mathord {\sim } A$ and $\mathord {\sim } A\to \neg A$ , all the same we can derive both $A\lor \neg A$ and $\mathord {\sim } A\leftrightarrow \neg A$ .

More interesting are the cases for the systems DN4 and DN4’. What kind of systems are obtained when we add $A\lor \mathord {\sim } A$ to these logics? For N4, the resulting system will be the system CLuNs of Batens & De Clercq [Reference Batens and De Clercq2], as mentioned in [Reference Omori, Wansing, Olivietti, Verbrugge, Negri and Sandu24]. CLuNs may be seen as a three-valued logic, with the truth-tables (Table 1) given in terms of values $\{\mathbf {T},\mathbf {I},\mathbf {F}\}$ . The value of $\bot $ is set to be $\mathbf {F}$ and the designated values for this semantics are taken to be $\mathbf {T}$ and $\mathbf {I}$ .

Table 1

Truth tables for CLuNs

That the above truth table works as a semantics for CLuNs means that $A\lor \neg A$ is derivable in it, i.e., the fragment without $\mathord {\sim }$ is classical. Indeed, it is easily seen that $(A\to \neg A)\lor \mathord {\sim }(A\to \neg A)$ derives the excluded middle with respect to the intuitionistic negation. Here it is important that $\mathord {\sim }(A\to \neg A)$ is equivalent to A.

Going back to DN4, the same formula $\mathord {\sim }(A\to \neg A)$ is equivalent only to $\neg \neg A$ , and as a result $(A\to \neg A)\lor \mathord {\sim }(A\to \neg A)$ derives only the weak law of excluded middle $\neg A\lor \neg \neg A$ . This suggests the following axiomatization of the system $\textbf {DN4}+(A\lor \mathord {\sim } A)$ , which we shall call $\textbf {DN4}_{+}$ .

Definition 4.25 ( $\textbf {DN4}_{+}$ ).

The system $\textbf {DN4}_{+}$ is defined by the following addition of axioms to DN4.

(WLEM) $$ \begin{align} \neg A\lor\neg\neg A \end{align} $$

(SLEM) $$ \begin{align} A\lor\mathord{\sim} A \end{align} $$

We first note that as a proof system, $\textbf {DN4}_{+}$ has a redundancy: it follows from our discussion above that (WLEM) is provable from (SLEM). Our decision to include (WLEM) in the list of axioms is motivated solely by the convenience it offers in proving the completeness.

The semantics for $\textbf {DN4}_{+}$ is obtained from that of $\textbf {DN4}$ by slight modifications.

It is well-known (cf. [Reference Chagrov and Zakharyaschev4, Reference Gabbay9]) that the system defined by the addition of (WLEM) to intuitionistic logic (to be denoted IPC $+$ (WLEM)Footnote ⁷ ) is sound and complete with the class of Kripke frames satisfying the above frame conditions. We shall utilize this fact in order to prove the completeness for $\textbf {DN4}_{+}$ .

We begin with observing the soundness of $\textbf {DN4}_{+}$ .

Proof. We argue by induction on the depth of deduction. It suffices to show that $w\Vdash ^{+} A\lor \mathord {\sim } A$ for all w and A. We show this by induction on the complexity of A.

When $A\equiv p$ , then since $\mathcal {V}^{+}(p)\cup \mathcal {V}^{-}(p)=W$ , either

$$ \begin{align*} w\Vdash^{+}p\text{ or }w\Vdash^{-}p \end{align*} $$

for each w. Hence $w\Vdash ^{+}p\lor \mathord {\sim } p$ for all w.

When $A\equiv \bot $ , since $w\Vdash ^{-}\bot $ , it follows that $w\Vdash ^{+}\bot \lor \mathord {\sim }\bot $ for all w.

When $A\equiv A_{1}\land A_{2}$ , by I.H.

$$ \begin{align*} w\Vdash^{+}A_{1}\lor\mathord{\sim} A_{1}\text{ and }w\Vdash^{+} A_{2}\lor \mathord{\sim} A_{2}. \end{align*} $$

If $w\Vdash ^{+}A_{1}$ and $w\Vdash ^{+}A_{2}$ , then $w\Vdash ^{+}A_{1}\land A_{2}$ . Otherwise, $w\Vdash ^{-}A_{1}$ or $w\Vdash ^{-}A_{2}$ , so $w\Vdash ^{-}A_{1}\land A_{2}$ . Hence $w\Vdash ^{+}\mathord {\sim }(A_{1}\land A_{2})$ . Therefore either way, $w\Vdash ^{+}(A_{1}\land A_{2})\lor \mathord {\sim }(A_{1}\land A_{2})$ .

When $A\equiv A_{1}\lor A_{2}$ , we have the same I.H. as above. If $w\Vdash ^{+}A_{1}$ or $w\Vdash ^{+}A_{2}$ , then $w\Vdash ^{+}A_{1}\lor A_{2}$ . Otherwise, $w\Vdash ^{-}A_{1}$ and $w\Vdash ^{-}A_{2}$ . So $w\Vdash ^{-}A_{1}\lor A_{2}$ . Thus $w\Vdash ^{+}\mathord {\sim } (A_{1}\lor A_{2})$ . Therefore $w\Vdash ^{+}(A_{1}\lor A_{2})\lor \mathord {\sim }(A_{1}\lor A_{2})$ .

When $A\equiv A_{1}\to A_{2}$ , we wish to show

$$ \begin{align*} w\Vdash^{+}(A_{1}\to A_{2})\lor \mathord{\sim}(A_{1}\to A_{2}). \end{align*} $$

Assume otherwise. Then

$$ \begin{align*} w\nVdash^{+}(A_{1}\to A_{2})\text{ and }w\nVdash^{+}\mathord{\sim}(A_{1}\to A_{2}). \end{align*} $$

From the former, there is $w'\geq w$ such that

$$ \begin{align*} w'\Vdash^{+}A_{1}\text{ and }w'\nVdash^{+}A_{2}. \end{align*} $$

It follows then that $w\nVdash ^{+}A_{2}$ . From the latter, either

$$ \begin{align*} w\nVdash^{+}\neg\neg A_{1}\text{ or }w\nVdash^{-} A_{2}. \end{align*} $$

Now, by I.H. $w\Vdash ^{+}A_{2}\lor \mathord {\sim } A_{2}$ ; but as $w\nVdash ^{+}A_{2}$ , we need to infer that $w\Vdash ^{+} \mathord {\sim } A_{2}$ . Thus $w\Vdash ^{-} A_{2}$ , and so it cannot be the case that $w\nVdash ^{-} A_{2}$ . Therefore $w\nVdash ^{+}\neg \neg A_{1}$ . Hence there is $w''\geq w$ such that for all $w'''\geq w''$ , it holds that $w'''\nVdash ^{+}A_{1}$ . Then by the frame property, there is $u\geq w',w''$ such that $u\Vdash ^{+}A_{1}$ and $u\nVdash ^{+}A_{1}$ , a contradiction. Therefore $w\Vdash ^{+}(A_{1}\to A_{2})\lor \mathord {\sim }(A_{1}\to A_{2})$ .

When $A\equiv \mathord {\sim } A_{1}$ , by I.H. we have $w\Vdash ^{+}A_{1}\lor \mathord {\sim } A_{1}$ . Hence $w\Vdash ^{+}\mathord {\sim } A_{1}\lor \mathord {\sim }\mathord {\sim } A_{1}$ .□

Next we move on to prove the completeness. The argument is similar to that of DN3. First, we look at the analogue of Lemma 2.9.

Proof. We argue by induction on the depth of derivation. It suffices to check the case for the axiom (SLEM). This we show by induction on the complexity of A.

When $A\equiv p$ , then $r(p\lor \mathord {\sim } p)$ is $p\lor \mathord {\sim } p$ , which is an instance of (SLEM). Similarly when $A\equiv \bot $ .

When $A\equiv A_{1}\land A_{2}$ , then $r(A\lor \mathord {\sim } A)$ is

$$ \begin{align*} (r(A_{1})\land r(A_{2}))\lor(r(\mathord{\sim} A_{1})\lor r(\mathord{\sim} A_{2})). \end{align*} $$

By I.H., there are reduced proofs of

$$ \begin{align*} r(A_{1})\lor r(\mathord{\sim} A_{1})\text{ and }r(A_{2})\lor r(\mathord{\sim} A_{2}), \end{align*} $$

and so we can also obtain a reduced proof of $r(A\lor \mathord {\sim } A)$ .

When $A\equiv A_{1}\lor A_{2}$ , the argument is similar to the previous case.

When $A\equiv A_{1}\to A_{2}$ , $r(A\lor \mathord {\sim } A)$ is

$$ \begin{align*} (r(A_{1})\to r(A_{2}))\lor (\neg\neg r(A_{1})\land r(\mathord{\sim} A_{2})). \end{align*} $$

By I.H. there is a reduced proof of $r(A_{2})\lor r(\mathord {\sim } A_{2})$ . In addition, $\neg r(A_{1})\lor \neg \neg r(A_{1})$ is an instance of (WLEM). Thus there is a reduced proof of $r(A\lor \mathord {\sim } A)$ .

When $A\equiv \mathord {\sim } A_{1}$ , then $r(A\lor \mathord {\sim } A)$ is $r(\mathord {\sim } A_{1})\lor r(A_{1})$ , which has a reduced proof by I.H.□

We shall next show the analogue of Proposition 2.10. For this purpose, given a reduced formula $A[\mathord {\sim } p_{1},\ldots ,\mathord {\sim } p_{n}]$ , we define a formula

$$ \begin{align*} F:= \bigwedge_{1\leq i\leq n}(p_{i}\lor q_{i}). \end{align*} $$

Now we are ready to conclude the completeness proof.

Comparing $\textbf {DN4}_{+}$ to $\textbf {CLuNs}$ , it may be taken as advantageous that (SLEM) does not necessitate the full law of excluded middle in the former. For instance, one may wish to introduce a decidable notion of negation while keeping the constructive setting as much as possible.Footnote ⁸

We next look at the case for DN4’. For this purpose we define a new system $\textbf {DN4'}_{+}$ .

Definition 4.32 ( $\textbf {DN4'}_{+}$ ).

The system $\textbf {DN4'}_{+}$ is defined by the addition of (SLEM) and the next axiom to DN4’.

(LEM) $$ \begin{align} A\lor\neg A \end{align} $$

This time, as was the case for N4, we require (LEM) to be derivable in the system, thus committing to a less constructive principle than $\textbf {DN4}_{+}$ . It does not mean, however, that $\textbf {DN4'}_{+}$ becomes identical to CLuNs, as we shall see below.

The Kripke semantics for $\textbf {DN4'}_{+}$ is quite similar to the semantics for classical logic.

Then we start with the soundness of the semantics with respect to $\textbf {DN4'}_{+}$ .

Proof. We show by induction on the depth of derivation. We concentrate on the case for (SLEM), with $A\equiv A_{1}\to A_{2}$ . In this case, by I.H.

$$ \begin{align*} w\Vdash^{+} A_{1}\lor\mathord{\sim} A_{1}\text{ and }w\Vdash^{+} A_{2}\lor\mathord{\sim} A_{2}. \end{align*} $$

Now if $w\nVdash ^{+} A_{1}\to A_{2}$ and $w\nVdash ^{+} \mathord {\sim }(A_{1}\to A_{2})$ , then $w\Vdash ^{+} A_{1}$ and $w\nVdash ^{+} A_{2}$ from the former. Also, $w\nVdash ^{-} A_{1}\to A_{2}$ from the latter; so $w\nVdash ^{+} \neg (A_{1}\to A_{2})$ or $w\nVdash ^{-} A_{2}$ . But the former means $w\Vdash ^{+} A_{1}\to A_{2}$ , a contradiction. On the other hand, the latter means $w\nVdash ^{+} A_{2}\lor \mathord {\sim } A_{2}$ , another contradiction. Therefore $w\Vdash ^{+}(A_{1}\to A_{2})\lor \mathord {\sim }(A_{1}\to A_{2})$ .□

Next we shall treat the completeness direction. The outline is identical to that of $\textbf {DN4}_{+}$ .

Proof. Again, it suffices to check the case for (SLEM), and we concentrate on the case $A\equiv A_{1}\to A_{2}$ . Then

$$ \begin{align*} r((A_{1}\to A_{2})\lor\mathord{\sim}(A_{1}\to A_{2}))=(r(A_{1})\to r(A_{2}))\lor (\neg(r(A_{1})\to r(A_{2}))\land r(\mathord{\sim} A_{2})). \end{align*} $$

By I.H., there is a reduced proof of $r(A_{2})\lor r(\mathord {\sim } A_{2})$ , and thus of $(r(A_{1})\to r(A_{2}))\lor r(\mathord {\sim } A_{2})$ . Moreover, $(r(A_{1})\to r(A_{2}))\lor \neg (r(A_{1})\to r(A_{2}))$ is an instance of (LEM). Hence there is a reduced proof of

$$ \begin{align*} (r(A_{1})\to r(A_{2}))\lor(\neg(r(A_{1})\to r(A_{2}))\land r(\mathord{\sim} A_{2})).\\[-33pt] \end{align*} $$

□

Let CPC to be the formalization of classical logic, defined as IPC $+$ (LEM).

Having established the completeness, we shall see how the semantics for $\textbf {DN4'}_{+}$ compares to that of CLuNs in terms of truth tables.

We shall define an assignment $\mathcal {A}$ to be a mapping from the set of prime formulas to the set of truth values $\{\textbf {T},\textbf {I},\textbf {F}\}$ . We in particular set $\mathcal {A}(\bot ):=\textbf {F}$ .

The truth value for a general formula is determined by the truth tables for each of the connectives. The truth tables for conjunction, disjunction and strong negation are identical to those of CLuNs. Table 2 gives the table of implication for $\textbf {DN4'}_{+}$ .

Table 2

Truth table of implication for DN4’ ₊

The only changes from the truth table of implication for CLuNs are when the antecedent of an implication has the value T or I, and the succedent the value $\mathbf {I}$ . As a consequence, an implication always has the value T or F Footnote ⁹ .

We define the validity with respect to the truth tables, to be denoted with $\vDash _{3}$ , by the next clause.

$$ \begin{align*} \vDash_{3} A\text{ iff for all assignment }\mathcal{A}, \mathcal{A}(A)\in\{T,I\}. \end{align*} $$

We shall now establish the correspondence of the truth tables with the Kripke semantics.

Lemma 4.38. Let $\mathcal {M}$ be a model of $\textbf {DN4'}_{+}$ . Define an assignment $\mathcal {A}_{\mathcal {M}}$ by:

$$ \begin{align*} \mathcal{A}_{\mathcal{M}} := \begin{cases} \textbf{T} & \text{ if } \mathcal{M},w\Vdash^{+} p\text{ and }\mathcal{M},w\nVdash^{-} p,\\ \textbf{I} & \text{ if } \mathcal{M},w\Vdash^{+} p\text{ and }\mathcal{M},w\Vdash^{-} p,\\ \textbf{F} & \text{ if } \mathcal{M},w\nVdash^{+} p\text{ and }\mathcal{M},w\Vdash^{-} p. \end{cases} \end{align*} $$

Then the following statements hold.

1. (i) $\mathcal {A}_{\mathcal {M}}(A)=\textbf {T}$ iff $\mathcal {M},w\Vdash ^{+} A$ and $\mathcal {M},w\nVdash ^{-} A$ .

2. (ii) $\mathcal {A}_{\mathcal {M}}(A)=\textbf {I}$ iff $\mathcal {M},w\Vdash ^{+} A$ and $\mathcal {M},w\Vdash ^{-} A$ .

3. (iii) $\mathcal {A}_{\mathcal {M}}(A)=\textbf {F}$ iff $\mathcal {M},w\nVdash ^{+} A$ and $\mathcal {M},w\Vdash ^{-} A$ .

For the converse direction, we have the following lemma.

Lemma 4.39. Let $\mathcal {A}$ be an assignment. Define a $\textbf {DN4'}_{+}$ model $\mathcal {M}_{\mathcal {A}}$ by:

$$ \begin{align*} w\in\mathcal{V}^{+}(p) & \text{ if } \mathcal{A}(p)=\textbf{T}\text{ or }\textbf{I},\\ w\in\mathcal{V}^{-}(p) & \text{ if } \mathcal{A}(p)=\textbf{F}\text{ or }\textbf{I}. \end{align*} $$

Then the following statements hold.

1. (i) $\mathcal {M}_{\mathcal {A}},w\Vdash ^{+} A$ if and only if $\mathcal {A}(A)=\textbf {T}\text { or }\textbf {I}$ .

2. (ii) $\mathcal {M}_{\mathcal {A}},w\Vdash ^{-} A$ if and only if $\mathcal {A}(A)=\textbf {F}\text { or }\textbf {I}$ .

Proof. By induction on the complexity of A. We look at the case when $A\equiv A_{1}\to A_{2}$ .

For (i) and (ii), we observe the following equivalences.

$$ \begin{align*} \text{ (i) }\mathcal{M}_{\mathcal{A}},w\Vdash^{+} A_{1}\to A_{2} &\Leftrightarrow \mathcal{M}_{\mathcal{A}},w\nVdash^{+} A_{1}\text{ or }\mathcal{M}_{\mathcal{A}},w\Vdash^{+}A_{2}.\\& \Leftrightarrow \mathcal{A}(A_{1})=\textbf{F}\text{ or }\mathcal{A}(A_{2})\neq \textbf{F}.\\& \Leftrightarrow \mathcal{A}(A_{1}\to A_{2})=\textbf{T}\text{ (or}\ \textbf{I}).\end{align*} $$

In the last equivalence, note it is impossible that $\mathcal {A}(A_{1}\to A_{2})=\textbf {I}$ .

$$ \begin{align*} \text{ (ii) }\mathcal{M}_{\mathcal{A}},w\Vdash^{-} A_{1}\to A_{2} & \Leftrightarrow \mathcal{M}_{\mathcal{A}},w\Vdash^{+} \neg(A_{1}\to A_{2})\text{ and } \mathcal{M}_{\mathcal{A}},w\Vdash^{-}A_{2}.\\ & \Leftrightarrow (\mathcal{A}(A_{1})=\textbf{T}\text{ or } \textbf{I})\text{ and }\mathcal{A}(A_{2})=\textbf{F}.\\ & \Leftrightarrow \mathcal{A}(A_{1}\to A_{2})=\textbf{F}\text{ (or}\ \textbf{I}). \end{align*} $$

□

Therefore we can establish the desired correspondence.

Having obtained the completeness of $\textbf {DN4'}_{+}$ with the three-valued truth-tables, a natural question now would be to ask what may be the sense of the tables. In this respect, it is helpful to note that the same tables are used in [Reference Coniglio and Silvestrini5] as a semantics for the logic LPT, which is defined by (K), (S), (CI), (CE), (DI), (DE), (FF), (SLEM) and the following axioms, with the rule (MP).

• • $A\lor (A\to B)$ ,

• • $\circ A\to (A\to (\mathord {\sim } A\to B))$ ,

• • $\mathord {\sim }\circ A\to (A\land \mathord {\sim } A)$ ,

• • $\circ (A\to B)$ ,

• • $\circ A\land \circ B\to \circ (A\land B)$ ,

• • $(A\land \mathord {\sim } A\land B)\to \mathord {\sim }(A\land B)\land \mathord {\sim }(B\land A)$ ,

where $\circ :=\neg (A\land \mathord {\sim } A)$ is what is known as the consistency operator.

LPT is designed to capture the notion of quasi-truth, which was originally introduced in [Reference Mikenberg, da Costa and Chuaqui17]. Its setting differs from ours only in that they take $\bot $ and $\lor $ as defined by the clauses $\bot :=\mathord {\sim }(A\to A)$ and $A\lor B:=\mathord {\sim }(\mathord {\sim } A\land \mathord {\sim } B)$ . We shall see the precise correspondence of the two systems.

Then we appeal to the well-known replacement rule for strong negation (cf. for instance [Reference Odintsov22, proposition 8.1.3]). Let $*$ be a fixed propositional variable taking a position in a formula C. (That is, $*$ occurs once in C.)

The above lemmas imply that occurrences of $\bot $ and disjunctions in a formula can be replaced with equivalent formulas without the connectives. Then it is straightforward to observe the following.

5 Connexivizing the variants

Having looked at the behavior of strong negation in DN3 and DN4(’), one natural development would be to consider how a similar change would affect the sibling notion of connexive negation in the system C of Wansing [Reference Wansing, Schmidt, Pratt-Hartmann, Reynolds and Wansing32]. C may be obtainedFootnote ¹⁰ from N4 by changing the falsity condition of implication to

$$ \begin{align*} \mathord{\sim}(A\to B)\leftrightarrow(A\to\mathord{\sim} B). \end{align*} $$

That is to say, by replacing $\land $ with $\to $ in the condition. Then the contra-classical principles called Aristotle’s theses and Boethius’ theses below become valid.

(AT) $$ \begin{align} \mathord{\sim}(\mathord{\sim} A\to A) \end{align} $$

(AT') $$ \begin{align} \mathord{\sim}(A\to\mathord{\sim} A) \end{align} $$

(BT) $$ \begin{align} (A\to B)\to\mathord{\sim} (A\to\mathord{\sim} B) \end{align} $$

(BT') $$ \begin{align} (A\to\mathord{\sim} B)\to\mathord{\sim}(A\to B) \end{align} $$

When we consider similar alternations in the falsity condition for implication, we have a choice between starting from DN4-type or DN4’-type falsity condition. Selecting the latter would mean employing the axiom

$$ \begin{align*} \mathord{\sim}(A\to B)\leftrightarrow(\neg(A\to B)\to\mathord{\sim} B). \end{align*} $$

This however does not seem satisfactory, because this would imply the derivability of

$$ \begin{align*} (A\to B)\to\mathord{\sim} (A\to B), \end{align*} $$

that is to say all implication implies its falsity, which is odd and rather strong. DN4-type condition, on the other hand, gives rise to the next axiom

$$ \begin{align*} \mathord{\sim}(A\to B)\leftrightarrow(\neg\neg A\to\mathord{\sim} B). \end{align*} $$

Then one may ask whether Aristotle’s and Boethius’ theses hold as in C. Now in our setting, these are equivalent to:

• • $\neg \neg \mathord {\sim } A\to \mathord {\sim } A$ ,

• • $\neg \neg A\to A$ ,

• • $(A\to B)\to (\neg \neg A\to B)$ ,

• • $(A\to \mathord {\sim } B)\to (\neg \neg A\to \mathord {\sim } B)$ .

Therefore we observe that the validity of the connexive theses in this formulation is tied with the validity of non-constructive principles such as double negation elimination. This is a rather interesting phenomenon in that it ties contra-classical characteristics for negation with classical characteristics, thus offering a different view of connexivity from that of C.

If we restrict A to be of the form $\neg A$ , then (AT)–(BT') indeed hold, but this rests on the fact that $\mathord {\sim }(A\to \bot )$ is a theorem for any A. This is an odd feature, and one may wish not to have $\bot $ in the language for this reason, as the original formulation did not. A possible remedy then is to change the language to a modal language $\mathcal {L}_{\Box }$

$$ \begin{align*} A ::= p\ |\ \Box A\ |\ A\land A\ |\ A\lor A\ |\ A\to A\ |\ \mathord{\sim} A, \end{align*} $$

with the modal axioms for double negation in [Reference Božič and Došen3, Reference Thomason28]:

(M1) $$ \begin{align} \Box(A\to B)\to(\Box A\to\Box B) \end{align} $$

(M2) $$ \begin{align} A\to\Box A \end{align} $$

(M3) $$ \begin{align} \Box(((A\to B)\to A)\to A) \end{align} $$

(M4) $$ \begin{align} \Box(\Box A\to A) \end{align} $$

We can set the falsity conditions for implication and modal formulas to be

• • $\mathord {\sim }(A\to B)\leftrightarrow (\Box A\to \mathord {\sim } B)$ ,

• • $\mathord {\sim }\Box A\leftrightarrow \Box \mathord {\sim } A$ .

Then for formulas of the form $\Box A$ , (AT)–(BT') become equivalent to the following:

• • $\Box \mathord {\sim } \Box A\to \mathord {\sim } \Box A$ ,

• • $\Box \Box A\to \Box A$ ,

• • $(\Box A\to \Box B)\to (\Box \Box A\to \Box B)$ ,

• • $(\Box A\to \mathord {\sim } \Box B)\to (\Box \Box A\to \mathord {\sim } \Box B)$ ,

which all hold. (Note $\Box \Box A\leftrightarrow \Box A$ because $\neg \neg \neg \neg A\leftrightarrow \neg \neg A$ .) Therefore even when we adopt the DN4-type condition, one can retain connexivity with respect to the formulas of form $\Box A$ , i.e.,

• • $\mathord {\sim } (\mathord {\sim } \Box A\to \Box A)$ ,

• • $\mathord {\sim }(\Box A\to \mathord {\sim }\Box A)$ ,

• • $(\Box A\to \Box B)\to \mathord {\sim }(\Box A\to \mathord {\sim }\Box B)$ ,

• • $(\Box A\to \mathord {\sim } \Box B)\to \mathord {\sim }(\Box A\to \Box B)$ .

In the above, one may also take $\neg $ to be primitive and alter the falsity condition for $\neg A$ to

$$ \begin{align*} \mathord{\sim}\neg A\leftrightarrow\neg\mathord{\sim} A \end{align*} $$

in order to obtain a similar result.Footnote ¹¹ Here one might argue that such a move is unwarranted, because the falsity condition for $\neg A$ should not be different from that of $A\to \bot $ , for semantically their truth conditions are equivalent. We may, however, associate a different truth condition for intuitionistic negation. For example, Došen [Reference Došen8] observes that the intuitionistic negation may be seen as a modal operator with a modal accessibility relation R (with certain conditions imposed), s.t.

$$ \begin{align*} w\Vdash \neg A \Longleftrightarrow \forall{w'}(wRw'\Rightarrow w'\nVdash A). \end{align*} $$

From such a point of view, it does not appear as justified that the above falsity condition for primitive negation should be identical to that of $A\to \bot $ . Similarly, for $\Box $ the truth condition in [Reference Božič and Došen3] is given by $\forall w'(wRw'\Rightarrow w'\Vdash A)$ , which when looked independently does not seem to support that the corresponding falsity condition should be that of $(A\to \bot )\to \bot $ .

6 Concluding remarks

In this paper, we looked at the strong negation of Nelson–Markov, and identified the problem that the falsity condition for implication does not reflect the intuitionistic equivalence between $\neg (A\to B)$ and $\neg \neg A\land \neg B$ . For this reason we set up the systems DN3 and DN4(’) by replacing A in the falsity condition with $\neg \neg A$ . We established the soundness and completeness of the systems with respect to Kripke semantics, and then made comparisons with N3 and N4.

From the results we obtained, it is possible to summarize the advantages of DN3 and DN4(’) over N3 and N4 as follows.

• • DN3 and DN4 refute strictly more propositions in the language of intuitionistic logic.

• • More general forms of contraposition are available in DN3 and DN4(’).

• • Unlike N4, adding $A\lor \mathord {\sim } A$ to DN4 does not force $A\lor \neg A$ to be valid.

For these reasons, we wish to claim that our systems are improvements over N3 and N4, at least if one believes that strong negation should resemble intuitionistic negation as much as possible (while retaining the constructive falsity property).

In addition to the above, our observations included that the provability of propositions of the form $\neg A$ in N3 (N4) corresponds with that of DN3 (DN4); how DN4’ may be seen as a generalization of a logic of quasi-truth; and how the resulting systems fare with connexivity when a change is made corresponding to that of DN4 to C.

For the future works, an obvious direction would be to consider the predicate extension of DN3 and DN4(’). It is expected that not all of the observations we made in this paper are replicable in the predicate logic, at least because we appealed to a Glivenko-like proposition. Therefore it is interesting to study how much of our results can be elevated to the predicate level. It is also worthwhile to explore whether the change in the falsity condition for implication creates a difference that is unique to the predicate language.

Another fruitful direction would be to relate DN4’ with the notion of quasi-truth. We started from the notion of strong negation and reached $\textbf {DN4'}_{+}$ . It is then a natural question to ask whether one can start from the theory of quasi-truth and shed light on DN4’ from that perspective. In particular, it should be of considerable interest if one could give an interpretation of the difference between DN4 and DN4’ through such a route.

Finally, it is intriguing to ask how the same change in the falsity condition would affect the logic of contraposable strong negation explored in [Reference Nelson and Heyting21], which is recently studied in depth in [Reference Nascimento, Rivieccio, Marcos, Spinks, Moss, de Queiroz and Martinez18, Reference Nascimento, Rivieccio, Marcos and Spinks19].