Codex @codex  0

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.

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.