Both symbolization and derivations with multiple quantifiers and two-place predicates require considerable practice. One special problem is that in some situations, because of the new-name rule, any mechanical test for validity (such as the consistency tree) may fail to establish validity. In more technical terms, such problems are undecidable. A good working rule is to examine the overall argument pattern and think of its analogues in a propositional (P and Q) logic.

EXAMPLE

All students read novels. Every novel is a long book. Therefore, all students read long books.

Use F for the students, G for the novels, H for the long books, Fxy for x reads y.

1. (x)[Fx->(Ey)(Gy & Fxy)]
2. (x)(Gx->Hx) \show (x)[Fx->(Ey)(Hy & Fxy)

3. Fa......................hyp
4. Fa->(Ey)(Gy & Fay)......1 UQ elim
5. (Ey)(Gy & Fay)..........3,4 -> elim
6. Gb & Fab................5 EQ elim watch for the new name rule
7. Gb->Hb..................2 UQ elim
8. Gb......................6 & elim
9. Hb......................7,8 ->elim
10. Fab....................6 & elim
11. Hb & Fab...............9,10 & int
12. (Ey)(Hy & Fay).........11 EQ int
13. Fa->(Ey)(Hy & Fay).....3-12 hyp elim
14. (x)[Fx->(Ey & Fxy)]....14 UQ int the name is now free