= Solution
Assign to each <propositional formula> its finite symbol length. The set of lengths of formulas <logically equivalent> to $\alpha$ is a nonempty subset of the <natural numbers>, because it contains the length of $\alpha$. The <well-ordering principle> for the <natural numbers> gives a least such length, and hence a shortest equivalent formula.
\b[A shortest equivalent formula need not be unique.] For example $(p_0\to p_0)$ and $(p_0\leftrightarrow p_0)$ are distinct <tautologies> of the same minimal length. A shorter formula would contain no binary connective and hence be a variable with some number of negations, which is not a <tautology>. This counts each <propositional variable> as one symbol, as in the stated language, and proves that a <shortest equivalent formula need not be unique>.
Back to article page
