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