Last Update: 25 February 2005
Note: or material is highlighted |

In lecture, 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.

Then:

- 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 Q*v*., 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 .

- Note that is not necessarily a "sentence" (i.e., a
wff with no free variables), since the variable
- If is a proper subwff of , and is a proper subwff of , then is a proper subwff of .
- Nothing else is a proper subwff.

- ((¬P ¬(Q ^ R)) v ((S ^ T) v (U ^ P)))

- (¬ P ¬(Q ^ R))
- ((S ^ T) v (U ^ P))
- ¬P
- ¬(Q ^ R)
- (S ^ T)
- (U ^ P)
- P
- (Q ^ R)
- S
- T
- U
- 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
variables.)

Copyright © 2005 by William J. Rapaport (rapaport@cse.buffalo.edu)

file: 563S05/propersubwff-2005-02-25.html