= Solution
A useful consequence of the <formation rules> is that <logical formulas> form a prefix-free <set> of strings. To see this, describe a deterministic <parser> that reads one <logical formula> from its starting position. On a <logical variable> it consumes that one symbol. On a <negation> symbol it recursively reads one following <logical formula>. On an opening parenthesis it recursively reads a left <logical formula>, requires a <logical implication> symbol, recursively reads a right <logical formula>, and requires the closing parenthesis. Induction on formation proves that, if a valid <logical formula> begins at the current position, this procedure consumes exactly that <logical formula> and stops at its end.
Suppose now that both $\alpha$ and $\phi$ are <logical formulas> and $\phi=\alpha\epsilon$. The same <parser>, started at their common first symbol, must stop both at the end of $\alpha$ and at the end of $\phi$. Its deterministic stopping position cannot differ, so $\epsilon$ is empty. Hence
$$
\boxed{\alpha=\phi.}
$$
This argument applies to symbol strings; it does not use <truth values> or <logical equivalence>.
Back to article page
