subformula

Let $L$ be a first order language and suppose $\phi$ is a formula of $L$. A subformula of $\phi$ is defined as any of the following:

1. $\phi$ is a subformula of $\phi$;

2. if $\mathrm{\neg }\psi$ is a subformula of $\phi$ for some $L$-formula $\psi$, then so is $\psi$;

3. if $\alpha \wedge \beta$ is a subformula of $\phi$ for some $L$-formulas $\alpha ,\beta$, then so are $\alpha$ and $\beta$;

4. if $\exists x(\psi )$ is a subformula of $\phi$ for some $L$-formula $\psi$, then so is $\psi [t/x]$ for any $t$ free for $x$ in $\psi$.

Remark. And if the language contains a modal connective, say $\mathrm{\square }$, then we also have

1. if $\mathrm{\square }\alpha$ is a subformula of $\phi$ for some $L$-formula $\alpha$, then so is $\alpha$.

The phrase “$t$ is free for $x$ in $\psi$” means that after substituting the term $t$ for the variable $x$ in the formula $\psi$, no free variables in $t$ will become bound variables in $\psi [t/x]$.

For example, if $\phi =\alpha \vee \beta$, then $\alpha$ and $\beta$ are subformulas of $\phi$. This is so because $\alpha \vee \beta =\mathrm{\neg }(\mathrm{\neg }\alpha \wedge \mathrm{\neg }\beta )$, so that $\mathrm{\neg }\alpha \wedge \mathrm{\neg }\beta$ is a subformula of $\phi$ by applications of 1 followed by 2 above. By 3 above, $\mathrm{\neg }\alpha$ and $\mathrm{\neg }\beta$ are subformulas of $\phi$. Therefore, by 2 again, $\alpha$ and $\beta$ are subformulas of $\phi$.

For another example, if $\phi =\exists x(\exists y(x^2+y^2=1))$, then $\exists y(t^2+y^2=1)$ is a subformula of $\phi$ as long as $t$ is a term that does not contain the variable $y$. Therefore, if $t=y+2$, then $\exists y({(y+2)}^2+y^2=1)$ is not a subformula of $\phi$. In fact, if $y\in ℝ$, the equation ${(y+2)}^2+y^2=1$ is never true.

Finally, it is easy to see (by induction) that if $\alpha$ is a subformula of $\psi$ and $\psi$ is a subformula of $\phi$, then $\alpha$ is a subformula of $\phi$. “Being a subformula of” is a reflexive transitive relation on $L$-formulas.

Remark. There is also the notion of a literal subformula of a formula $\phi$. A formula $\psi$ is a literal subformula of $\phi$ if it is a subformula of $\phi$ obtained in any one of the first three ways above, or if $\exists x(\psi )$ is a literal subformula of $\phi$.

Note that any literal subformula of $\phi$ is a subformula of $\phi$, for if $\phi =\exists x(\psi )$, then $x$ occurs free in $\psi$ and $\psi =\psi [x/x]$.

In the second example above, $\exists y(x^2+y^2=1)$ and $x^2+y^2=1$ are both literal subformulas of $\phi =\exists x(\exists y(x^2+y^2=1))$.