negation

**natural deduction** metalanguage, practical foundations

**type theory** (dependent, intensional, observational type theory, homotopy type theory)

**computational trinitarianism** = **propositions as types** +**programs as proofs** +**relation type theory/category theory**

In logic, the **negation** of a statement $p$ is a statement $\neg{p}$ which is true if and only if $p$ is false.

In classical logic, we have the double negation law:

$\neg\neg{p} \equiv p.$

In intuitionistic logic, we only have

$\neg\neg{p} \dashv p,$

while in paraconsistent logic, we instead have

$\neg\neg{p} \vdash p.$

You can interpret intuitionistic negation as ‘denial’ and paraconsistent negation as ‘doubt’. So when one says that one doesn't deny $p$, that's weaker than actually asserting $p$; while when one says that one doesn't doubt $p$, that's stronger than merely asserting $p$. Paraconsistent logic has even been applied to the theory of law: if $p$ is a judgment that normally requires only the preponderance of evidence, then $\neg\neg{p}$ is a judgment of $p$ 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^\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.

In usual type theory syntax negation is obtained as the function type into the empty type: $\not a = a \to \emptyset$.

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

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

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

Revised on August 20, 2012 23:48:05
by Urs Schreiber
(89.204.138.177)