is a subformula of ;
if is a subformula of for some -formula , then so is ;
if is a subformula of for some -formulas , then so are and ;
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
if is a subformula of for some -formula , then so is .
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.
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 .
|Date of creation||2013-03-22 12:42:52|
|Last modified on||2013-03-22 12:42:52|
|Last modified by||CWoo (3771)|