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 + strong negation. Constructive + explicit falsity.

Symbols.

Symbol	Unicode	Name	Meaning
~	—	Strong negation	Explicit falsity
¬	U+00AC	Weak negation	Not provable
N3	—	Nelson 3	Consistent
N4	—	Nelson 4	Paraconsistent

Metatheory. Decidable. Kripke semantics with strong negation. N4 related to Belnap. Cut elimination. Algebraic: Nelson algebras.

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

Limitations. Two negations complexity. Less familiar. Multiple variants. Integration with other systems.