Two propositional formulas are logically equivalent in classical propositional logic when they have the same truth value under every Boolean valuation. Identical output columns in a truth table prove logical equivalence; one differing row refutes it. De Morgan's laws give useful examples.
Lengths of formulas logically equivalent to a fixed propositional formula form a nonempty subset of the natural numbers, so a minimum exists. With variables counted as atomic symbols and no truth constants, and are distinct shortest tautologies. A formula with no binary connective is a variable preceded by negations and cannot be a tautology. Thus minimization need not give a canonical representative.
