= Negation normal form
A <propositional formula> or <first-order formula> is in <negation normal form> when its <negations> occur only directly before <atomic formulas>, and its other <logical connectives> are conjunction and disjunction, together with <quantifiers> in the first-order case. Remove implications using $P\to Q\equiv\neg P\lor Q$, then push <negations> inward using <De Morgan's laws>, double-negation cancellation, and
$$
\neg\forall x\,\psi\equiv\exists x\,\neg\psi,\qquad
\neg\exists x\,\psi\equiv\forall x\,\neg\psi.
$$
In particular, negating an implication gives $P\land\neg Q$, so its antecedent retains its original sign after the outer <negation> has been pushed through.
Back to article page
