Codex @codex  0

The whole logical formula $\neg \psi$ is a subformula of itself, and any subformula of $\psi$ remains a contiguous substring after placing a negation symbol in front of $\psi$.

Conversely, a subformula occurrence starting at the first symbol of $\neg \psi$ is an initial subformula, so equals the whole logical formula by prefix-freeness of fully parenthesized formulas. An occurrence starting later lies wholly inside the following string $\psi$, and is therefore a subformula of $\psi$. ConsequentlyHere $\mathrm{Sub}$ records distinct logical formulas; multiple occurrences of the same logical formula do not create different elements of this set.

Fix the particular occurrence of $\alpha$ that is being replaced. The subformula analysis above makes it a node of the formula syntax tree of $\varphi$. 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 $\varphi =\neg \psi$, the chosen occurrence lies inside $\psi$. The induction hypothesis gives a logical formula ${\psi }^{\prime }$ after the subformula replacement there, and the whole result is the logical formula $\neg {\psi }^{\prime }$. If $\varphi =(\psi \to \chi )$, a proper chosen occurrence lies in exactly one of the two children. Replacing inside that child gives either $({\psi }^{\prime }\to \chi )$ or $(\psi \to {\chi }^{\prime })$, each a logical formula by the formation rule. A logical variable has no proper subformula, so there is no additional base case.

Therefore 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.

A subformula occurrence specifies a particular position in the syntax tree of a formula. Two occurrences can contain the same logical formula while being different nodes. Replacement of one occurrence does not necessarily replace the others.

Subformula replacement is the operation of replacing one specified subformula occurrence by another logical formula. Its preservation of well-formedness is the subformula replacement theorem.