Classical propositional logic

Classical propositional logic interprets propositions as true or false and validates principles such as the law of excluded middle and double-negation elimination.

Assume $H=(P\to Q)\to P$ and temporarily assume $\neg P$. A further assumption $P$ yields a contradiction and hence $Q$ by the logical falsity elimination rule; discharge it to obtain $P\to Q$. Applying $H$ gives $P$, contradicting $\neg P$. Discharge the latter assumption to obtain $\neg \neg P$, apply double-negation elimination, and finally discharge $H$. This is a derivation from the primitive classical natural deduction rules. The principle is named for Charles Sanders Peirce.

A tautology is a propositional formula true under every Boolean valuation in classical propositional logic, such as the law of excluded middle $p\vee \neg p$. A primitive proposition $p$ is not a tautology, even if it represents a true statement. See forall x: Calgary, section 12.1.

An argument has logical validity in classical propositional logic when no Boolean valuation makes all premises $\Gamma$ true and the conclusion $A$ false: $\Gamma \models A$. With no premises, $\models A$ says that $A$ is a tautology. See forall x: Calgary, sections 12.4–12.6.

The law of excluded middle asserts that every proposition $A$ satisfies $A\vee \neg A$.

Double-negation elimination is the inference from $\neg \neg A$ to $A$.