Double negation Within a system of
classical logic, double negation, that is, the negation of the negation of a proposition P, is
logically equivalent to P. Expressed in symbolic terms, \neg \neg P \equiv P. In
intuitionistic logic, a proposition implies its double negation, but not conversely. This marks one important difference between classical and intuitionistic negation. Algebraically, classical negation is called an
involution of period two. However, in
intuitionistic logic, the weaker equivalence \neg \neg \neg P \equiv \neg P does hold. This is because in intuitionistic logic, \neg P is just a shorthand for P \rightarrow \bot, and we also have P \rightarrow \neg \neg P . Composing that last implication with triple negation \neg \neg P \rightarrow \bot implies that P \rightarrow \bot . As a result, in the propositional case, a sentence is classically provable if its double negation is intuitionistically provable. This result is known as
Glivenko's theorem.
Distributivity De Morgan's laws provide a way of
distributing negation over
disjunction and
conjunction: :\neg(P \lor Q) \equiv (\neg P \land \neg Q), and :\neg(P \land Q) \equiv (\neg P \lor \neg Q).
Linearity Let \oplus denote the logical
xor operation. In
Boolean algebra, a linear function is one such that: If there exists a_0, a_1, \dots, a_n \in \{0,1\}, f(b_1, b_2, \dots, b_n) = a_0 \oplus (a_1 \land b_1) \oplus \dots \oplus (a_n \land b_n), for all b_1, b_2, \dots, b_n \in \{0,1\}. Another way to express this is that each variable always makes a difference in the
truth-value of the operation, or it never makes a difference. Negation is a linear logical operator.
Self dual In
Boolean algebra, a self dual function is a function such that: f(a_1, \dots, a_n) = \neg f(\neg a_1, \dots, \neg a_n) for all a_1, \dots, a_n \in \{0,1\}. Negation is a self dual logical operator.
Negations of quantifiers In
first-order logic, there are two quantifiers, one is the universal quantifier \forall (means "for all") and the other is the existential quantifier \exists (means "there exists"). The negation of one quantifier is the other quantifier (\neg \forall xP(x)\equiv\exists x\neg P(x) and \neg \exists xP(x)\equiv\forall x\neg P(x)). For example, with the predicate
P as "
x is mortal" and the domain of x as the collection of all humans, \forall xP(x) means "a person x in all humans is mortal" or "all humans are mortal". The negation of it is \neg \forall xP(x)\equiv\exists x\neg P(x), meaning "there exists a person
x in all humans who is not mortal", or "there exists someone who lives forever". ==Rules of inference==