In contrast to weak negation, and in analogy to the use of a strong “or” and “exists” in constructive logic,
Nelson [1]}, and independently Markov [2]}, introduced the strong negation
\(\sim \hspace{-4.2679pt} A\)  of \(A\) .
Following Kleene's recursive realisability, Nelson developed constructive arithmetic with strong negation and showed that
it has the same expressive power as Heyting arithmetic. Within Nelson's realisability,
the equivalences \(\mathbin {\sim } (A \wedge B) \Leftrightarrow \ \mathbin {\sim }A\)  \(\vee \mathbin {\sim } B\)  and \(\mathbin {\sim }\forall _x A(x) \Leftrightarrow \exists _x \mathbin {\sim } A(x)\)  are realisable. In axiomatic presentations of constructive logic with
strong negation \((\mathrm {CLSN})\)  (see [3]}, [4]}) these equivalences are axiom schemes. In most formalisations of \(\mathrm {CLSN}\) ,
but not in all (see system N4 in [5]}), strong negation \(\mathbin {\sim } A\)  implies weak negation
\(\lnot A\) . Markov [2]} expressed weak negation
through strong negation and implication as follows:
\(\lnot A := A \rightarrow \mathbin {\sim } A.\) 
Rasiowa [3]} went even further, introducing a strong implication
\(A \Rightarrow B\) , defined through the standard “weak” implication \(\rightarrow \)  and strong negation as follows:
\(A \Rightarrow B := (A \rightarrow B) \wedge (\mathbin {\sim } B \rightarrow \mathbin {\sim } A).\) 
The various aspects of the model theory of \(\mathrm {CLSN}\)  are developed in many papers
(see e.g., [4]}, [9]}, [10]}, [11]}).
