= Solution
First note that a substring which is itself a <logical formula> must coincide with a subtree of the <formula syntax tree> of the surrounding <logical formula>. Indeed, a <logical formula> can begin only at a <logical variable>, a <negation> symbol or an opening parenthesis. Every such position in a valid <logical formula> is the start of one of its parsed subtrees. If $\beta$ is the <logical formula> at that subtree and $\alpha$ is another <logical formula> starting at the same position, one is an initial segment of the other; <prefix-freeness of fully parenthesized formulas> from the preceding part forces $\alpha=\beta$.
Now consider a final <subformula>. For a <logical variable>, it can only be the whole <logical formula>. For a binary <logical implication> $(\psi\to\chi)$, every proper subtree is contained in $\psi$ or $\chi$ and finishes before the final closing parenthesis of the whole expression. It therefore cannot be a final substring of the whole. The only remaining possible outer formation is <negation>. Thus
$$
\boxed{\alpha=\phi\quad\text{or}\quad\phi=\neg\psi\text{ for some formula }\psi.}
$$
The second alternative is a necessary possibility, not a claim that every negated <logical formula> has every one of its <subformulas> as a suffix.
Back to article page
