negation in nLab

Contents

Contents

Idea

In (classical) logic, the negation of a statement pp is a statement ¬p\neg{p} which is true if and only if pp is false. Hence, viewed algebraically, the negation corresponds to the complement operator of the corresponding Boolean algebra which satisfies a∧¬a=⊥a\wedge\neg a=\bot as well as a∨¬a=⊤a\vee \neg a=\top.

More generally, as different logics correspond to different types of lattices, one calls negation antitone, or polarity reversing, lattice operators that mimic or approximate the algebraic and proof-theoretic behavior of ¬\neg.

As a logic gate

As a logic gate on bits and as a quantum logic gate on qbits (XX-Pauli matrix):

Negation in different logics

In classical logic, we have the double negation law:

¬¬p≡p. \neg\neg{p} \;\equiv\; p \,.

In intuitionistic logic, we only have

¬¬p⊣p, \neg\neg{p} \;\dashv\; p \,,

while in paraconsistent logic, we instead have

¬¬p⊢p. \neg\neg{p} \;\vdash\; p \,.

One may interpret intuitionistic negation as ‘denial’ and paraconsistent negation as ‘doubt’. So when one says that one doesn't deny pp, that's weaker than actually asserting pp; while when one says that one doesn't doubt pp, that's stronger than merely asserting pp. Paraconsistent logic has even been applied to the theory of law: if pp is a judgment that normally requires only the preponderance of evidence, then ¬¬p\neg\neg{p} is a judgment of pp beyond reasonable doubt.

Linear logic features (at least) three different forms of negation, one for each of the above. (The default meaning of the term ‘negation’ in linear logic, p ⊥p^\bot, is the one that satisfies the classical double-negation law.)

Accordingly, negation mediates de Morgan duality in classical and linear logic but not in intuitionistic or paraconsistent logic.

Antithesis interpretation

In the antithesis interpretation of intuitionistic logic, one considers, instead of single propositions, pairs of mutually exclusive propositions, i.e. propositions pp and qq such that ¬(p∧q)\neg (p \wedge q). These are generalisations of the intuitionistic denial negation since we have by currying the statements p→¬qp \to \neg q and q→¬pq \to \neg p. The intuitionistic negation is simply a special case of the above since we have the true statements p→¬¬pp \to \neg \neg p and ¬p→¬p\neg p \to \neg p from the law of non-contradiction ¬(p∧¬p)\neg (p \wedge \neg p).

There is an affine linear logic associated with mutually exclusive propositions where the affine negation of mutually exclusive propositions pp and qq is just qq and pp respectively. Thus, we can say that qq is the negation of pp and vice versa, for mutually exclusive propositions pp and qq. This is very important for constructive mathematics, where the terms “equal/not equal” and related concepts such as “rational number/irrational number” and “algebraic number/transcendental number” are usually defined using equality/tight apartness relation for objects such as the real numbers and the p-adic numbers. These terms only makes sense in this context if one is using the affine negation of the mutually exclusive propositions rather than intuitionistic denial negation, the latter which in general is not an involution on propositions.

In type theory syntax

In usual type theory syntax negation is obtained as the function type into the empty type: ¬a=a→∅\not a = a \to \varnothing.

Equivalently, in type theory with equivalence types but without function types, negation is the equivalence type with the empty type: ¬a=a≃∅\not a = a \simeq \varnothing.

In categorical semantics

The categorical semantics of negation is the internal hom into the initial object: ¬=[−,∅]\not = [-, \emptyset].

In a topos, the negation of an object AA (a proposition under the propositions as types-interpretation) is the internal hom object 0 A0^A, where 0=∅0 = \emptyset denotes the initial object.

This matches the intuitionistic notion of negation in that there is a natural morphism A→0 0 AA \to 0^{0^A} but not the other way around.

Negation as implying triviality of rings

There are some mathematicians working in ring theory and algebra, such as Lombardi & Quitté 2010, who define negation for a proposition PP about a ring RR as PP implies that the ring RR is trivial 0= R10 =_R 1. The proposition P→(0= R1)P \to (0 =_R 1) is the same as the usual negation ¬P\neg P for a non-trivial commutative ring, but is always true for the trivial ring. Hence, this leads to the concepts of a possibly trivial integral domain and a possibly trivial field, which the authors Lombardi & Quitté call simply an “integral domain” and a “field” respectively.

One can also extend this notion of negation from rings to other bi-pointed sets such as rigs, lattices, frames, pointed abelian groups, absorption monoids, bounded total orders, closed midpoint algebras, scales, and interval coalgebras.

• double negation

• complement

• De Morgan duality

• co-Heyting negation

• adjoint cylinder

• strong negation

References

• Y. Gauthier, A Theory of Local Negation: The Model and some Applications , Arch. Math. Logik 25 (1985) pp.127-143. (gdz)

• H. Wansing, Negation , pp.415-436 in Goble (ed.), The Blackwell Guide to Philosophical Logic , Blackwell Oxford 2001.

• Henri Lombardi, Claude Quitté (2010): Commutative algebra: Constructive methods (Finite projective modules) Translated by Tania K. Roblo, Springer (2015) (doi:10.1007/978-94-017-9944-7, pdf)

• Michael Shulman, Affine logic for constructive mathematics. Bulletin of Symbolic Logic, Volume 28, Issue 3, September 2022. pp. 327 - 386 (doi:10.1017/bsl.2022.28, arXiv:1805.07518)