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.

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$.