# Contents

## Idea

In logic, the negation of a statement $p$ is a statement $¬p$ which is true if and only if $p$ is false.

In classical logic, we have the double negation law:

$¬¬p\equiv 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.

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 $¬¬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}^{\perp }$, 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 type theory syntax

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

## In categorical semantics

The categorical semantics of negation is the internal hom into the initial object: $¬=\left[-,\varnothing \right]$.

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=\varnothing$ 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)