Restricted quantifier proofs More about first order logic

The following sequents provide practice in constructing proofs using binary (restricted) quantifiers. Some of them require the use of both restricted and unrestricted quantifiers, so be careful which rules you apply. In cases where the analogous proof with unrestricted quantifiers were earlier exercises, it may be useful to compare the two proofs.

The first few problems are fairly easy; the later ones a little more involved. The last one is fiendish: if you do it without looking at the answer, you have my respect!

ALL(x: Fx) Gx, ALL(x: Gx) Hx ⊢ ALL(x: Fx) Hx	SH {Sample proof 301} SP {ALL(x: Fx) Gx, ALL(x: Gx) Hx ⊢ ALL(x: Fx) Hx} PL {1} {1} {ALL(x: Fx) Gx} {A} PL {2} {2} {ALL(x: Gx) Hx} {A} PL {3} {3} {Fa} {A} PL {1,3} {4} {Ga} {1, 3 ALLE_R} PL {1,2,3} {5} {Ha} {2, 4 ALLE_R} PL {1,2} {6} {ALL(x: Fx) Hx} {5 [3] ALLI_R} EP EH	Try it	Answer
ALL(x: Fx) Gx ⊢ ALL(x: Gx IMP Hx) (Fx IMP Hx)	SH {Sample proof 302} SP {ALL(x: Fx) Gx ⊢ ALL(x: Gx IMP Hx) (Fx IMP Hx)} PL {1} {1} {ALL(x: Fx) Gx} {A} PL {2} {2} {Ga IMP Ha} {A} PL {3} {3} {Fa} {A} PL {1,3} {4} {Ga} {1, 3 ALLE_R} PL {1,2,3} {5} {Ha} {2, 4 IMPE} PL {1,2} {6} {Fa IMP Ha} {5 [3] IMPI} PL {1} {7} {ALL(x: Gx IMP Hx) (Fx IMP Hx)} {6 [2] ALLI} EP EH	Try it	Answer
ALL(x: NOTFx) Fx ⊢ ALLx Fx	SH {Sample proof 303} SP {ALL(x: NOTFx) ⊢ ALLx Fx} PL {1} {1} {ALL(x: NOTFx) Fx} {A} PL {2} {2} {NOTFa} {A} PL {1,2} {3} {Fa} {1, 2 ALLE_R} PL {1} {4} {NOTNOTFa} {2, 3 [2] RAA} PL {1} {5} {Fa} {4 NOTNOTE} PL {1} {6} {ALLx Fx} {5 ALLI} EP EH	Try it	Answer
ALL(x: Fx) NOTGx ⊢ NOTSOME(x: Fx) Gx	SH {Sample proof 304} SP {ALL(x: Fx) NOTGx ⊢ NOTSOME(x: Fx) Gx} PL {1} {1} {ALL(x: Fx) NOTGx} {A} PL {2} {2} {SOME(x: Fx) Gx} {A} PL {3} {3} {Fa} {A} PL {4} {4} {Ga} {A} PL {1,3} {5} {NOTGa} {1, 3 ALLE_R} PL {3,4} {6} {NOTALL(x: Fx) NOTGx} {4, 5 [1] RAA} PL {2} {7} {NOTALL(x: Fx) NOTGx} {2, 6 [3, 4] SOMEE_R} PL {1} {8} {NOTSOME(x: Fx) Gx} {1, 7 [2] RAA} EP EH	Try it	Answer
SOME(x: Fx) Fx ⊢ SOMEx Fx	SH {Sample proof 305} SP {SOME(x: Fx) Fx ⊢ SOMEx Fx} PL {1} {1} {SOME(x: Fx) Fx} {A} PL {2} {2} {Fa} {A} PL {2} {3} {SOMEx Fx} {2 SOMEI} PL {1} {4} {SOMEx Fx} {1, 3 [2, 2] SOMEE_R} EP EH	Try it	Answer
ALLxALL(y: Rxy) (Fx AND Gy), ALLxSOMEy Rxy ⊢ SOME(x: Fx) Gx	SH {Sample proof 306} SP {ALLxALL(y: Rxy) (Fx AND Gy), ALLxSOMEy Rxy ⊢ SOME(x: Fx) Gx} PL {1} {1} {ALLxALL(y: Rxy) (Fx AND Gy)} {A} PL {2} {2} {ALLxSOMEy Rxy} {A} PL {2} {3} {SOMEy Ray} {2 ALLE} PL {4} {4} {Rab} {A} PL {1} {5} {ALL(y: Ray) (Fa AND Gy)} {1 ALLE} PL {1,4} {6} {Fa AND Gb} {4, 5 ALLE_R} PL {1,4} {7} {Gb} {6 ANDE} PL {2} {8} {SOMEy Rby} {2 ALLE} PL {9} {9} {Rbc} {A} PL {1} {10} {ALL(y: Rby) (Fb AND Gy)} {1 ALLE} PL {1,9} {11} {Fb AND Gc} {9, 10 ALLE_R} PL {1,9} {12} {Fb} {11 ANDE} PL {1,2} {13} {Fb} {8, 12 [9] SOMEE} PL {1,2,4} {14} {SOME(x: Fx) Gx} {7, 13 SOMEI_R} PL {1,2} {15} {SOME(x: Fx) Gx} {3, 14 [4] SOMEE} EP EH	Try it	Answer
ALL(x: Fx) Gx ⊢ ALL(x: SOME(y: Fy) Rxy) SOME(y: Gy) Rxy	SH {Sample proof 307} SP {ALL(x: Fx) Gx ⊢ ALL(x: SOME(y: Fy) Rxy) SOME(y: Gy) Rxy} PL {1} {1} {ALL(x: Fx) Gx} {A} PL {2} {2} {SOME(y: Fy) Ray} {A} PL {3} {3} {Fb} {A} PL {4} {4} {Rab} {A} PL {1,3} {5} {Gb} {1, 3 ALLE_R} PL {1,3,4} {6} {SOME(y: Gy) Ray} {4, 5 SOMEI_R} PL {1,2} {7} {SOME(y: Gy) Ray} {2, 6 [3, 4] SOMEE_R} PL {1} {8} {ALL(x: SOME(y: Fy) Rxy) SOME(y: Gy) Rxy} {7 [2] ALLI_R} EP EH	Try it	Answer
NOTALL(x: NOTSOME(y: NOTRxy) Fy) NOTFx ⊢ SOME(x: ALL(y: Fy) Rxy) Fx	SH {Sample proof 308} SP {NOTALL(x: NOTSOME(y: NOTRxy) Fy) NOTFx ⊢ SOME(x: ALL(y: Fy) Rxy) Fx} PL {1} {1} {NOTALL(x: NOTSOME(y: NOTRxy) Fy) NOTFx} {A} PL {2} {2} {NOTSOME(x: ALL(y: Fy) Rxy) Fx} {A} PL {3} {3} {NOTSOME(y: NOTRay) Fy} {A} PL {4} {4} {Fa} {A} PL {5} {5} {Fb} {A} PL {6} {6} {NOTRab} {A} PL {5,6} {7} {SOME(y: NOTRay) Fy} {5, 6 SOMEI_{R} PL {3,5} {8} {NOTNOTRab} {3, 7 [6] RAA} PL {3,5} {9} {Rab} {3, 7 NOTNOTE} PL {3} {10} {ALL(y: Fy) Ray} {9 [5] ALLI_R} PL {3,4} {11} {SOME(x: ALL(y: Fy) Rxy) Fx} {4, 10 SOMEI_R} PL {2,3} {12} {NOTFa} {2, 11 [4] RAA} PL {2} {13} {ALL(x: NOTSOME(y: NOTRxy) Fy) NOTFx} {12 [3] ALLI_R} PL {1} {14} {NOTNOTSOME(x: ALL(y: Fy) Rxy) Fx} {1, 13 [2] RAA} PL {1} {15} {SOME(x: ALL(y: Fy) Rxy) Fx} {14 NOTNOTE} EP EH}	Try it	Answer