A unary negation operator $\neg$ that matches up with the behaviour of negation in classical logic in an appropriate way. Many conflicting explications of when a negation can be considered ‘classical’ exist but accounts tend to demand that the negation operator behaves in an analogous fashion to the operation of complement in a Boolean algebra. Axiomatic accounts often claim that a negation is classical when it satisfies the principle of excluded middle and principle of explosion:

• • $\phi ⊢\left(\psi \vee \neg \psi \right)$

• • $\left(\psi \wedge \neg \psi \right)⊢\phi$

To this definition, sometimes it is also suggested that a classical negation must satisfy the following form of contraposition:

• • $\left(\phi \to \neg \psi \right)\to \left(\psi \to \neg \phi \right)$

Semantic definitions of the classicality of a negation frequently identify the truth of a negated formula with the non-truth of the formula it negates, and the failure of truth of a negated formula with the truth of the formula it modifies. In a more perspicuous form, this definition states that a negation $\neg$ is classical (or Boolean) if for all formulae $\phi$ and any model $\mathfrak{M}$ (or whatever stands in for a model in the corresponding semantics),

$\neg \phi$ is true in $\mathfrak{M}$ if and only if $\phi$ is not true in $\mathfrak{M}$

On this definition, the intuitionistic account of negation is not classical because in the Kripke semantics, there exist occasions in which neither a formula $\phi$ nor its negation are true.