|
Let $L$ be a first order language and suppose $\varphi$ is a formula of $L$ A subformula of $\varphi$ is defined as any of the following:
- $\varphi$ is a subformula of $\varphi$
- if $\neg \psi$ is a subformula of $\varphi$ for some $L$ formula $\psi$ then so is $\psi$
- if $\alpha\wedge \beta$ is a subformula of $\varphi$ for some $L$ formulas $\alpha,\beta$ then so are $\alpha$ and $\beta$
- if $\exists x (\psi)$ is a subformula of $\varphi$ for some $L$ formula $\psi$ then so is $\psi[t/x]$ for any $t$ free for $x$ in $\psi$
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 $\varphi=\alpha \vee \beta$ then $\alpha$ and $\beta$ are subformulas of $\varphi$ This is so because $\alpha\vee \beta = \neg(\neg \alpha \wedge \neg \beta)$ so that $\neg \alpha\wedge \neg\beta$ is a subformula of $\varphi$ by applications of 1 followed by 2 above. By 3 above, $\neg \alpha$ and $\neg \beta$ are subformulas of $\varphi$ Therefore, by 2 again, $\alpha$ and $\beta$ are subformulas of $\varphi$
For another example, if $\varphi=\exists x (\exists y (x^2+y^2=1))$ then $\exists y (t^2+y^2=1)$ is a subformula of $\varphi$ 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 $\varphi$ In fact, if $y\in \mathbb{R}$ 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 $\varphi$ then $\alpha$ is a subformula of $\varphi$ ``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 $\varphi$ A formula $\psi$ is a literal subformula of $\varphi$ if it is a subformula of $\varphi$ obtained in any one of the first three ways above, or if $\exists x (\psi)$ is a literal subformula of $\varphi$
Note that any literal subformula of $\varphi$ is a subformula of $\varphi$ for if $\varphi=\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 $\varphi=\exists x (\exists y (x^2+y^2=1))$
| 
