Nelson Logic

Origin. David Nelson (1949). Constructive logic with strong negation. Two negations: ¬ (weak) and ~ (strong). N3 and N4 variants. Foundation for constructive falsity.

Models. Strong negation ~: explicit falsity information. Weak negation ¬: absence of proof. N3: consistent, N4: allows contradictions. Four-valued semantics for N4.

Formalism.

Two negations: ~A: A is strongly false (refuted) ¬A: A is not provable (weak, ¬A ≡ A → ⊥)

Strong negation axioms: ~~A ↔ A (involution) ~(A ∧ B) ↔ ~A ∨ ~B ~(A ∨ B) ↔ ~A ∧ ~B ~(A → B) ↔ A ∧ ~B

N3 (consistent): A ∧ ~A → B (explosion for strong negation) No gluts: cannot have both A and ~A.

N4 (paraconsistent): A ∧ ~A ↛ B Allows strong contradictions. Four values: T, F, Both, Neither.

Twist structures: N3, N4 semantics via twist structures. Pairs (a, b) where a: positive, b: negative info.

Relation to other logics: N3 extends intuitionistic logic. N4 = FDE + an intuitionistic implication (the strong negation is already FDE's). Constructive + explicit falsity.

Symbols.

Symbol	Unicode	Name	Meaning
~	U+007E	Tilde / Strong negation	Explicit refutation; a primitive, not defined
¬	U+00AC	Not sign / Weak negation	Intuitionistic negation, defined as A → ⊥
⊥	U+22A5	Up tack / Falsum	Absurdity, used to define ¬
∧	U+2227	Logical and / Conjunction	Distributes under ~ as a De Morgan law
∨	U+2228	Logical or / Disjunction	Distributes under ~ as a De Morgan law
→	U+2192	Rightwards arrow / Implication	Intuitionistic; ~(A → B) ↔ A ∧ ~B
↔	U+2194	Left right arrow / Biconditional	Strong equivalence, in the ~ axioms
↛	U+219B	Rightwards arrow with stroke	Non-entailment, as in A ∧ ~A ↛ B in N4
∀	U+2200	Universal quantifier	Nelson's axioms give ~∀x.A ↔ ∃x.~A
∃	U+2203	Existential quantifier	Nelson's axioms give ~∃x.A ↔ ∀x.~A
N3	—	Nelson's logic N3	Explosive: A ∧ ~A entails everything
N4	—	Nelson's logic N4	Paraconsistent: strong contradictions are tolerated
(a, b)	—	Twist pair	Positive information a, negative information b
T, F, Both, Neither	—	The four values	Belnap's values, carried by N4
A, B	—	Formula metavariables	Range over formulas

Metatheory. N3 is a conservative extension of intuitionistic logic: its strong-negation-free fragment is exactly IPC, so nothing is gained or lost about the positive connectives and the whole content of the system is what ~ adds. Rasiowa (1958) gave the algebraic semantics — N-lattices, now Nelson algebras — and proved completeness; Vakarelov (1977) showed every Nelson algebra is a twist structure over a Heyting algebra, so the two-component semantics of positive and negative information is a representation theorem rather than a convention. Spinks and Veroff (2008) established a term equivalence with a variety of residuated lattices, placing N3 inside substructural logic. Almukdad and Nelson (1984) introduced N4 by dropping explosion for ~, leaving the intuitionistic implication intact; its negation fragment is Belnap–Dunn first-degree entailment, which is where the four values come from. Both systems have cut-free sequent calculi, the disjunction property, and Nelson's constructible falsity property — if ~(A ∧ B) is provable then so is ~A or ~B. Both are decidable, and both are PSPACE-hard, since IPC embeds.

Applies to. Constructive falsity. Databases with negative info. Logic programming. Paraconsistent reasoning. Explicit refutation.

Limitations. Strong negation is not definable from the intuitionistic connectives and must be taken primitive, so N3 is not an intermediate logic and none of the machinery for the lattice of intermediate logics applies to it. The two negations are only one-way related — ~A → ¬A holds, its converse does not — so failing to prove A is never evidence of a refutation, which is exactly the asymmetry the system was built to record and also the reason it cannot close the gap. Replacement of equivalents fails for the weak biconditional: A ↔ B does not license substituting B for A inside ~, because congruence requires strong equivalence, so ordinary equational reasoning must be replaced throughout. N3 is explosive for ~, so it says nothing about inconsistent data; N4 is paraconsistent but loses disjunctive syllogism and contraposition, and has no ⊥, so intuitionistic negation has to be re-added as a separate primitive. At the predicate level Nelson's ~∀x.A ↔ ∃x.~A is a strong commitment: refuting a universal is required to yield a witness, which no constructive reading of ∀ delivers on its own.