Past exam of the logic and set theory course of the University of Oxford / 2008 / A / 1 / e / iv

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.