= Shortest equivalent formula need not be unique
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, $(p\to p)$ and $(p\leftrightarrow p)$ 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.
Back to article page