Back to the index. Or to the chambers

This article has 9 links. View as Cloud or List.

Equation Variable Obvious Reflexive Non Degenerate Sesquilinear Induction Terms And Formulas Superset Transitive Free And Bound Variables

1	Reflexive Non Degenerate Sesquilinear
1	Obvious
1	Variable
1	Superset
1	Terms And Formulas
1	Induction
1	Equation
2	Transitive
2	Free And Bound Variables

Loading ...

Planetmath Browser (2008—2009)

BSD licence | A django site

All articles taken from PlanetMath.org snapshot under CC-BY-SA licence.

→ The original article on PlanetMath.org

Other Formats: LaTeX

New! You can click on formulas to copy the LaTeX source to your clipboard. | Math Videos

Subformula

Let be a first order language and suppose $\varphi$ is a formula of . 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 -formula $\psi$ , then so is $\psi$ ;
if $\alpha\wedge \beta$ is a subformula of $\varphi$ for some -formulas $\alpha,\beta$ , then so are $\alpha$ and $\beta$ ;
if $\exists x (\psi)$ is a subformula of $\varphi$ for some -formula $\psi$ , then so is $\psi[t/x]$ for any free for in $\psi$ .

The phrase “

is free for

in $\psi$ ” means that after substituting the term

for the variable

in the formula $\psi$ , no free variables in

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 is a term that does not contain the variable . Therefore, if , then $\exists y ((y+2)^2+y^2=1)$ is not a subformula of $\varphi$ . In fact, if $y\in \mathbb{R}$ , the equation 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 -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 occurs free in $\psi$ and $\psi=\psi[x/x]$ .

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