First, break down the conclusion by the main operator, sub-main operator, etc, and get the associated introduction (I) rules:
Derivation strategy:
- Do ∀I to derive ∀x(Cx→~Wx).
- Do →I to derive Ca→~Wa. ("a" is just an arbitrary constant in place of "x" in Cx→~Wx).
- Assume Ca. That leaves ~Wa to derive.
- Do ~I to derive ~Wa.
- Assume Wa. That leaves ⊥ to derive.
- Do ⊥I to derive ⊥.
The proof strategy:
- Go from top to bottom and perform the assumptions.
- Perform elimination (E) rules where possible, going line by line.
- Work from the bottom to the top of the derivation strategy. D introduction (I) rules as they fulfill the steps.
- If an elimination (E) rule can't be performed, make an assumption of what's needed so that it can be.
- If there's a contradiction, take it! You can derive anything via ⊥E once you have it.
- ∃x[~Bxm&∀y(Cy→~Gxy)] : P
- ∀z[~∀y(Wy→Gzy)→Bzm] : P
- | Ca : SM→I
- Go from top to bottom and perform the assumptions.
- Step 3: Assume Ca. That leaves ~Wa to derive.
- || Wa : SM~I
- Step 5: Assume Wa. That leaves ⊥ to derive.
- ||| ~Bbm&∀y(Cy→~Gby) : SM∃E
- Make the necessary assumption to do ∃E on line (1).
- ||| ~∀y(Wy→Gby)→Bbm : ∀E (2)
- ||| ~Bbm : &E (5)
- ||| ∀y(Cy→~Gby) : &E (5)
- |||| ~∀y(Wy→Gby) : SM~I
- Make the necessary assumption to do →E on line (6).
- |||| Bbm : →E (6, 9)
- |||| ⊥ : ⊥I (7, 10)
- If there's a contradiction, take it! You can derive anything via ⊥E once you have it.
- ||| ~~∀y(Wy→Gby) : ~I (9 - 11)
- ||| Ca→~Gba : ∀E (8)
- Don't try elimination rules on lines (9 - 11), since that subproof has been discharged.
- ||| ∀y(Wy→Gby) : ~E (12)
- ||| ~Gba : →E (3, 13)
- ||| Wa→Gba : ∀E (14)
- ||| Gba : →E (4, 16)
- ||| ⊥ : ⊥I (16, 17)
- || ⊥ : ∃E (1, 5 - 18)
- Step 6: Do ⊥I to derive ⊥.
- Actually, Step 6 was done on line (18), but ∃E discharged what we needed to the right assumption depth.
- | ~Wa : ~I (4 - 19)
- Step 4: Do ~I to derive ~Wa.
- Ca→~Wa : →I (3 - 20)
- Step 2: Do →I to derive Ca → ~Wa.
- ∀x(Cx→~Wx) : ∀I (21)
- Step 1: Do ∀I to derive ∀x(Cx→~Wx).
- 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.