subformula
Let be a first order language and suppose is a formula of . A subformula of is defined as any of the following:
-
1.
is a subformula of ;
-
2.
if is a subformula of for some -formula , then so is ;
-
3.
if is a subformula of for some -formulas , then so are and ;
-
4.
if is a subformula of for some -formula , then so is for any free for in .
Remark. And if the language contains a modal connective, say , then we also have
-
5.
if is a subformula of for some -formula , then so is .
The phrase “ is free for in ” means that after substituting the term for the variable in the formula , no free variables in will become bound variables in .
For example, if , then and are subformulas of . This is so because , so that is a subformula of by applications of 1 followed by 2 above. By 3 above, and are subformulas of . Therefore, by 2 again, and are subformulas of .
For another example, if , then is a subformula of as long as is a term that does not contain the variable . Therefore, if , then is not a subformula of . In fact, if , the equation is never true.
Finally, it is easy to see (by induction) that if is a subformula of and is a subformula of , then is a subformula of . “Being a subformula of” is a reflexive transitive relation on -formulas.
Remark. There is also the notion of a literal subformula of a formula . A formula is a literal subformula of if it is a subformula of obtained in any one of the first three ways above, or if is a literal subformula of .
Note that any literal subformula of is a subformula of , for if , then occurs free in and .
In the second example above, and are both literal subformulas of .
Title | subformula |
---|---|
Canonical name | Subformula |
Date of creation | 2013-03-22 12:42:52 |
Last modified on | 2013-03-22 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 |