= Solution
Fix the particular occurrence of $\alpha$ that is being replaced. The <subformula> analysis above makes it a node of the <formula syntax tree> of $\phi$. Proceed by <structural induction> on the surrounding <logical formula>.
If this node is the root, the <subformula replacement> gives $\beta$, already a <logical formula>. Otherwise, if $\phi=\neg\psi$, the chosen occurrence lies inside $\psi$. The induction hypothesis gives a <logical formula> $\psi'$ after the <subformula replacement> there, and the whole result is the <logical formula> $\neg\psi'$. If $\phi=(\psi\to\chi)$, a proper chosen occurrence lies in exactly one of the two children. Replacing inside that child gives either $(\psi'\to\chi)$ or $(\psi\to\chi')$, each a <logical formula> by the <formation rule>. A <logical variable> has no proper <subformula>, so there is no additional base case.
Therefore \b[replacing the designated <subformula occurrence> by any <logical formula> preserves well-formedness]. The argument concerns one chosen occurrence; it does not require simultaneous <subformula replacement> of every occurrence of the same string.
Back to article page
