Quantifier proof exercises Expressing Generality
The following sequents provide practice in the art of constructing proofs. Answers are given, but of course the idea is to come up with proofs of your own before looking them up. As ever, the answers are not unique: in some cases, alternative proofs are just as good as the ones given.
| ALLx(Fx IMP Gx) ⊢ ALLx((Fx AND Hx) IMP (Gx AND Hx)) | SH {Sample proof 101} SP {ALLx (Fx IMP Gx) ⊢ ALLx ((Fx AND Hx) IMP (Gx AND Hx))} PL {1} {1} {ALLx (Fx IMP Gx)} {A} PL {2} {2} {Fa AND Ha} {A} PL {2} {3} {Fa} {2 ANDE} PL {2} {4} {Ha} {2 ANDE} PL {1} {5} {Fa IMP Ga} {1 ALLE} PL {1,2} {6} {Ga} {3, 5 IMPE} PL {1,2} {7} {Ga AND Ha} {4, 6 ANDI} PL {1} {8} {(Fa AND Ha) IMP (Ga AND Ha)} {7 [2] IMPI} PL {1} {9} {ALLx ((Fx AND Hx) IMP (Gx AND Hx))} {8 ALLI} EP EH | Try it | Answer | |
| ALLx(Fx IMP Gx) ⊢ ALLx ((Gx IMP Hx) IMP (Fx IMP Hx)) | SH {Sample proof 102} SP {ALLx (Fx IMP Gx) ⊢ ALLx ((Gx IMP Hx) IMP (Fx IMP Hx))} PL {1} {1} {ALLx (Fx IMP Gx)} {A} PL {2} {2} {Ga IMP Ha} {A} PL {3} {3} {Fa} {A} PL {1} {4} {Fa IMP Ga} {1 ALLE} PL {1,3} {5} {Ga} {3, 4 IMPE} PL {1,2,3} {6} {Ha} {2, 5 IMPE} PL {1,2} {7} {Fa IMP Ha} {6 [3] IMPI} PL {1} {8} {(Ga IMP Ha) IMP (Fa IMP Ha)} {7 [2] IMPI} PL {1} {9} {ALLx ((Gx IMP Hx) IMP (Fx IMP Hx))} {8 ALLI} EP EH | Try it | Answer | |
| ALLx(Fx IMP Gx), ALLx(Fx IMP NOTGx) ⊢ ALLx NOTFx | SH {Sample proof 103} SP {ALLx (Fx IMP Gx), ALLx (Fx IMP NOTGx) ⊢ ALLx NOTFx} PL {1} {1} {ALLx (Fx IMP Gx)} {A} PL {2} {2} {ALLx (Fx IMP NOTGx)} {A} PL {3} {3} {Fa} {A} PL {1} {4} {Fa IMP Ga} {1 ALLE} PL {2} {5} {Fa IMP NOTGa} {2 ALLE} PL {1,3} {6} {Ga} {3, 4 IMPE} PL {2,3} {7} {NOTGa} {3, 5 IMPE} PL {1,2} {8} {NOTFa} {6, 7 [3] RAA} PL {1,2} {9} {ALLx NOTFx} {8 ALLI} EP EH | Try it | Answer | |
| ALLx(Fx IMP NOTGx) ⊢ NOTSOMEx (Fx AND Gx) | SH {Sample proof 104} SP {ALLx (Fx IMP NOTGx) ⊢ NOTSOMEx (Fx AND Gx)} PL {1} {1} {ALLx (Fx IMP NOTGx)} {A} PL {2} {2} {SOMEx (Fx AND Gx)} {A} PL {3} {3} {Fa AND Ga} {A} PL {3} {4} {Fa} {3 ANDE} PL {3} {5} {Ga} {3 ANDE} PL {1} {6} {Fa IMP NOTGa} {1 ALLE} PL {1,3} {7} {NOTGa} {4, 6 IMPE} PL {1,3} {8} {BAD} {5, 7 NOTE} PL {1,2} {9} {BAD} {2, 8 [3] SOMEE} PL {1} {10}{NOTSOMEx (Fx AND Gx)} {9 [2] NOTI} EP EH | Try it | Answer | |
| SOMEx (Fx OR Gx), ALLx (Fx IMP Hx), ALLx (Gx IMP Hx) ⊢ SOMEx Hx | SH {Sample proof 105} SP {SOMEx (Fx OR Gx), ALLx (Fx IMP Hx), ALLx (Gx IMP Hx) ⊢ SOMEx Hx} PL {1} {1} {SOMEx (Fx OR Gx)} {A} PL {2} {2} {ALLx (Fx IMP Hx)} {A} PL {3} {3} {ALLx (Gx IMP Hx)} {A} PL {4} {4} {Fa OR Ga} {A} PL {2} {5} {Fa IMP Ha} {2 ALLE} PL {3} {6} {Ga IMP Ha} {3 ALLE} PL {7} {7} {Fa} {A} PL {2,7} {8} {Ha} {5, 7 IMPE} PL {9} {9} {Ga} {A} PL {3,9} {10} {Ha} {6, 9 IMPE} PL {2,3,4} {11} {Ha} {4, 8 [7], 10 [9] ORE} PL {2,3,4} {12} {SOMEx Hx} {11 SOMEI} PL {1,2,3} {13} {SOMEx Hx} {1, 12 [4] SOMEE} EP EH | Try it | Answer | |
| p AND SOMEx Fx ⊢ SOMEx (Fx AND p) | SH {Sample proof 106} SP {p AND SOMExFx ⊢ SOMEx (Fx AND p)} PL {1} {1} {p AND SOMExFx} {A} PL {1} {2} {p} {1 ANDE} PL {1} {3} {SOMEx Fx} {1 ANDE} PL {4} {4} {Fa} {A} PL {1,4} {5} {Fa AND p} {2, 4 ANDI} PL {1,4} {6} {SOMEx (Fx AND p)} {5 SOMEI} PL {1} {7} {SOMEx (Fx AND p)} {3, 6 [4] SOMEE} EP EH | Try it | Answer | |
| SOMEx (Fx AND p) ⊢ p AND SOMEx Fx | SH {Sample proof 107} SP {SOMEx (p AND Fx) ⊢ p AND SOMExFx} PL {1} {1} {SOMEx (Fx AND p)} {A} PL {2} {2} {Fa AND p} {A} PL {2} {3} {p} {2 ANDE} PL {2} {4} {Fa} {2 ANDE} PL {2} {5} {SOMEx Fx} {4 SOMEI} PL {2} {6} {p AND SOMExFx} {3, 5 ANDI} PL {1} {7} {p AND SOMExFx} {1, 6 [2] SOMEE} EP EH | Try it | Answer | |
| ALLxALLy Rxy ⊢ ALLyALLx Rxy | SH {Sample proof 108} SP {ALLxALLy Rxy ⊢ ALLyALLx Rxy} PL {1} {1} {ALLxALLy Rxy} {A} PL {1} {2} {ALLy Ray} {1 ALLE} PL {1} {3} {Rab} {2 ALLE} PL {1} {4} {ALLx Rxb} {3 ALLI} PL {1} {5} {ALLyALLx Rxy} {4 ALLI} EP EH | Try it | Answer | |
| SOMExSOMEy Rxy ⊢ SOMEySOMEx Rxy | SH {Sample proof 109} SP {SOMExSOMEy Rxy ⊢ SOMEySOMEx Rxy} PL {1} {1} {SOMExSOMEy Rxy} {A} PL {2} {2} {SOMEy Ray} {A} PL {3} {3} {Rab} {A} PL {3} {4} {SOMEx Rxb} {3 SOMEI} PL {3} {5} {SOMEySOMEx Rxy} {4 SOMEI} PL {2} {6} {SOMEySOMEx Rxy} {2, 5 [3] SOMEE} PL {1} {7} {SOMEySOMEx Rxy} {1, 6 [2] SOMEE} EP EH | Try it | Answer | |
| ALLxALLy(Rxy IMP (Fx AND Gy)), ALLxSOMEy Rxy ⊢ SOMEx(Fx AND Gx) | SH {Sample proof 110} SP {ALLxALLy (Rxy IMP (Fx AND Gy)), ALLxSOMEy Rxy ⊢ SOMEx (Fx AND Gx)} PL {1} {1} {ALLxALLy (Rxy IMP (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} {ALLy (Ray IMP (Fa AND Gy))} {1 ALLE} PL {1} {6} {Rab IMP (Fa AND Gb)} {5 ALLE} PL {1,4} {7} {Fa AND Gb} {4, 6 IMPE} PL {1,4} {8} {Gb} {7 ANDE} PL {2} {9} {SOMEy Rby} {2 ALLE} PL {10} {10} {Rbc} {A} PL {1} {11} {ALLy (Rby IMP (Fb AND Gy))} {1 ALLE} PL {1} {12} {Rbc IMP (Fb AND Gc)} {11 ALLE} PL {1,10} {13} {Fb AND Gc} {10, 12 IMPE} PL {1,10} {14} {Fb} {13 ANDE} PL {1,2} {15} {Fb} {9, 14 [10] SOMEE} PL {1,2,4} {16} {Fb AND Gb} {8, 15 ANDI} PL {1,2,4} {17} {SOMEx(Fx AND Gx)} {16 SOMEI} PL {1,2} {18} {SOMEx(Fx AND Gx)} {3, 17 [4] SOMEE} EP EH | Try it | Answer | |
| ALLxALLy (Rxy IMP Sxy), ALLxSOMEy (Fy AND NOTSxy) ⊢ ALLxSOMEy (Fy AND NOTRxy) | SH {Sample proof 111} SP {ALLxALLy (Rxy IMP Sxy), ALLxSOMEy (Fy AND NOTSxy) ⊢ ALLxSOMEy (Fy AND NOTRxy)} PL {1} {1} {ALLxALLy (Rxy IMP Sxy)} {A} PL {2} {2} {ALLxSOMEy (Fy AND NOTSxy)} {A} PL {2} {3} {SOMEy (Fy AND NOTSay)} {2 ALLE} PL {4} {4} {Fb AND NOTSab} {A} PL {4} {5} {Fb} {4 ANDE} PL {4} {6} {NOTSab} {4 ANDE} PL {7} {7} {Rab} {A} PL {1} {8} {ALLy (Ray IMP Say)} {1 ALLE} PL {1} {9} {Rab IMP Sab} {8 ALLE} PL {1,7} {10} {Sab} {7, 9 IMPE} PL {1,4} {11} {NOT Rab} {6, 10 [7] RAA} PL {1,4} {12} {Fb AND NOT Rab} {5, 11 ANDI} PL {1,4} {13} {SOMEy (Fy AND NOTRay)} {12 SOMEI} PL {1,2} {14} {SOMEy (Fy AND NOTRay)} {3, 13 [4] SOMEE} PL {1,2} {15} {ALLxSOMEy (Fy AND NOTRxy)} {14 ALLI} EP EH | Try it | Answer | |
| ALLxALLyALLz ((Rxy AND Ryz) IMP Rxz), ALLxALLy (Rxy IMP Ryx) ⊢ ALLxALLy (Rxy IMP Rxx) | SH {Sample proof 112} SP {ALLxALLyALLz ((Rxy AND Ryz) IMP Rxz), ALLxALLy (Rxy IMP Ryx) ⊢ ALLxALLy (Rxy IMP Rxx)} PL {1} {1} {ALLxALLyALLz ((Rxy AND Ryz) IMP Rxz)} {A} PL {2} {2} {ALLxALLy (Rxy IMP Ryx)} {A} PL {3} {3} {Rab} {A} PL {1} {4} {ALLyALLz ((Ray AND Ryz) IMP Raz)} {1 ALLE} PL {1} {5} {ALLz ((Rab AND Rbz) IMP Raz)} {4 ALLE} PL {1} {6} {(Rab AND Rba) IMP Raa} {5 ALLE} PL {2} {7} {ALLy (Ray IMP Rya)} {2 ALLE} PL {2} {8} {Rab IMP Rba} {7 ALLE} PL {2,3} {9} {Rba} {3, 8 IMPE} PL {2,3} {10} {Rab AND Rba} {3, 9 ANDI} PL {1,2,3} {11} {Raa} {6, 10 IMPE} PL {1,2} {12} {Rab IMP Raa} {11 [3] IMPI} PL {1,2} {13} {ALLy (Ray IMP Raa)} {12 ALLI} PL {1,2} {14} {ALLxALLy (Rxy IMP Rxx)} {13 ALLI} EP EH | Try it | Answer | |
| ALLxFx IMP SOMEyGy ⊢ SOMExSOMEy(Fx IMP Gy) | SH {Sample proof 113} SP {ALLxFx IMP SOMEyGy ⊢ SOMExSOMEy (Fx IMP Gy)} PL {1} {1} {ALLxFx IMP SOMEyGy} {A} PL {2} {2} {NOTSOMExSOMEy (Fx IMP Gy)} {A} PL {3} {3} {NOTFa} {A} PL {4} {4} {Fa} {A} PL {3,4} {5} {NOTNOTGa} {3, 4 [ ] RAA} PL {3,4} {6} {Ga} {5 NOTNOTE} PL {3} {7} {Fa IMP Ga} {6 [4] IMPI} PL {3} {8} {SOMEy (Fa IMP Gy)} {7 SOMEI} PL {3} {9} {SOMExSOMEy (Fx IMP Gy)} {8 SOMEI} PL {2} {10} {NOTNOTFa} {2, 9 [3] RAA} PL {2} {11} {Fa} {10 NOTNOTE} PL {2} {12} {ALLx Fx} {11 ALLI} PL {1,2} {13} {SOMEy Gy} {1, 12 IMPE} PL {14} {14} {Ga} {A} PL {14} {15} {Fa IMP Ga} {14 [ ] IMPI} PL {14} {16} {SOMEy (Fa IMP Gy)} {15 SOMEI} PL {14} {17} {SOMExSOMEy (Fx IMP Gy)} {16 SOMEI} PL {1,2} {18} {SOMExSOMEy (Fx IMP Gy)} {13, 17 [14] SOMEE} PL {1} {19} {NOTNOTSOMExSOMEy (Fx IMP Gy)} {2, 18 [2] RAA} PL {1} {20} {SOMExSOMEy (Fx IMP Gy)} {19 NOTNOTE} EP EH | Try it | Answer |