CSE 463/563, Spring 2005
Last Update: 25 February 2005
material is highlighted
I have used the expression "proper subproposition" or sometimes "proper
subformula" or even "proper subwff".
Here is a recursive definition of "proper subwff" for our language for FOL.
Let , , be wffs.
- If is ¬, then is a proper subwff of .
- If is ( v ), then and are proper subwffs of .
- If is ( ^ ), then and are proper subwffs of .
- If is (
), then and are proper subwffs of .
- If is ( ), then and are proper subwffs of .
- Let Q be a quantifier (either or
Let v be a variable.
Then if is Qv., then is a proper subwff of .
- Note that is not necessarily a "sentence" (i.e., a
wff with no free variables), since the variable v
can occur free in .
- If is a proper subwff of , and is a proper subwff of , then
is a proper subwff of .
- Nothing else is a proper subwff.
The proper subwffs of:
- ((¬P ¬(Q ^ R)) v ((S ^ T) v (U ^ P)))
- (¬ P ¬(Q ^ R))
- ((S ^ T) v (U ^ P))
- ¬(Q ^ R)
- (S ^ T)
- (U ^ P)
- (Q ^ R)
You can make a nice (recursive) tree diagram with the main wff at the
root, and the proper subwffs as children; the leaves will be the atomic
wffs. (However, in the case of an FOL wff, some of the leaves might
not be sentences, because of the presence of free
Copyright © 2005 by
William J. Rapaport