Proper Subformula

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:

1. If is ¬, then is a proper subwff of .
2. If is ( v ), then and are proper subwffs of .
3. If is ( ^ ), then and are proper subwffs of .
4. If is ( ), then and are proper subwffs of .
5. If is ( ), then and are proper subwffs of .

6. 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 .

7. If is a proper subwff of , and is a proper subwff of , then is a proper subwff of .
8. Nothing else is a proper subwff.

An Example:

• ((¬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.)