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

5.
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 \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 $\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))$.
Title  subformula 

Canonical name  Subformula 
Date of creation  20130322 12:42:52 
Last modified on  20130322 12:42:52 
Owner  CWoo (3771) 
Last modified by  CWoo (3771) 
Numerical id  13 
Author  CWoo (3771) 
Entry type  Definition 
Classification  msc 03C07 
Classification  msc 03B10 
Related topic  Substitutability 
Defines  literal subformula 