Prove that the following argument is valid in QL: ∃x[~Bxm& ∀y(Cy → ~Gxy)], ∀z[~∀y(Wy →Gzy) → Bzm], ∴∀x(Cx → ~Wx)

Question

General ways to approach and how to start would be greatly appreciated.

Answer 1

First, break down the conclusion by the main operator, sub-main operator, etc, and get the associated introduction (I) rules:

Derivation strategy:

1. Do ∀I to derive ∀x(Cx→~Wx).
2. Do →I to derive Ca→~Wa. ("a" is just an arbitrary constant in place of "x" in Cx→~Wx).
3. Assume Ca. That leaves ~Wa to derive.
4. Do ~I to derive ~Wa.
5. Assume Wa. That leaves ⊥ to derive.
6. Do ⊥I to derive ⊥.

The proof strategy:

1. Go from top to bottom and perform the assumptions.
2. Perform elimination (E) rules where possible, going line by line.
3. Work from the bottom to the top of the derivation strategy. D introduction (I) rules as they fulfill the steps.
4. If an elimination (E) rule can't be performed, make an assumption of what's needed so that it can be.
5. If there's a contradiction, take it! You can derive anything via ⊥E once you have it.

1. ∃x[~Bxm&∀y(Cy→~Gxy)] : P
2. ∀z[~∀y(Wy→Gzy)→Bzm] : P
3. | Ca : SM→I
4. Go from top to bottom and perform the assumptions.
5. Step 3: Assume Ca. That leaves ~Wa to derive.
6. || Wa : SM~I
7. Step 5: Assume Wa. That leaves ⊥ to derive.
8. ||| ~Bbm&∀y(Cy→~Gby) : SM∃E
9. Make the necessary assumption to do ∃E on line (1).
10. ||| ~∀y(Wy→Gby)→Bbm : ∀E (2)
11. ||| ~Bbm : &E (5)
12. ||| ∀y(Cy→~Gby) : &E (5)
13. |||| ~∀y(Wy→Gby) : SM~I
14. Make the necessary assumption to do →E on line (6).
15. |||| Bbm : →E (6, 9)
16. |||| ⊥ : ⊥I (7, 10)
17. If there's a contradiction, take it! You can derive anything via ⊥E once you have it.
18. ||| ~~∀y(Wy→Gby) : ~I (9 - 11)
19. ||| Ca→~Gba : ∀E (8)
20. Don't try elimination rules on lines (9 - 11), since that subproof has been discharged.
21. ||| ∀y(Wy→Gby) : ~E (12)
22. ||| ~Gba : →E (3, 13)
23. ||| Wa→Gba : ∀E (14)
24. ||| Gba : →E (4, 16)
25. ||| ⊥ : ⊥I (16, 17)
26. || ⊥ : ∃E (1, 5 - 18)
27. Step 6: Do ⊥I to derive ⊥.
28. Actually, Step 6 was done on line (18), but ∃E discharged what we needed to the right assumption depth.
29. | ~Wa : ~I (4 - 19)
30. Step 4: Do ~I to derive ~Wa.
31. Ca→~Wa : →I (3 - 20)
32. Step 2: Do →I to derive Ca → ~Wa.
33. ∀x(Cx→~Wx) : ∀I (21)
34. Step 1: Do ∀I to derive ∀x(Cx→~Wx).
35. QED.

This strategy works for the vast majority of proofs, and on all proofs once you learn a few transformation strategies when the main operator is a negation.