Free logic proof exercises Identity and existence
The following sequents are (mostly) quite easy to prove in ordinary first order logic, but proving them in free logic requires a little more thought. As for the earlier pages of exercises, specimen answers are given, but the point is for you to try constructing proofs before looking them up. The proof editor tool is set up to expect the free logic versions of the quantifier rules in place of the conventional ones.
| EST(a) ⊢ SOMEx (x = a) | SH {Sample proof 401 (in free logic)} SP {EST(a) ⊢ SOMEx (x = a))} PL {1} {1} {EST(a)} {A} PL { } {2} {a = a} {=I} PL {1} {3} {SOMEx (x = a)} {1, 2 SOMEIf} EP EH | Try it | Answer | |
| SOMEx (x = a) ⊢ EST(a) | SH {Sample proof 402 (in free logic)} SP {EST(a) ⊢ SOMEx (x = a))} PL {1} {1} {SOMEx (x = a)} {A} PL {2} {2} {b = a} {A} PL {3} {3} {EST(b)} {A} PL {2,3} {4} {EST(a)} {2, 3 =E} PL {1} {5} {EST(a)} {1, 4 [2, 3] SOMEEf} EP EH | Try it | Answer | |
| ALLx Fx, ALLx Gx ⊢ ALLx(Fx AND Gx) | SH {Sample proof 403 (in free logic)} SP {ALLx Fx , ALLx Gx ⊢ ALLx (Fx AND Gx)} PL {1} {1} {ALLx Fx} {A} PL {2} {2} {ALLx Gx} {A} PL {3} {3} {EST(a)} {A} PL {1,3} {4} {Fa} {1, 3 ALLEf} PL {2,3} {5} {Ga} {2, 3 ALLEf} PL {1,2,3} {6} {Fa AND Ga} {4, 5 ANDI} PL {1,2} {7} {ALLx (Fx AND Gx)} {6 [3] ALLIf} EP EH | Try it | Answer | |
| SOMEx (Fx OR Gx) ⊢ SOMExFx OR SOMExGx | SH {Sample proof 404 (in free logic)} SP {SOMEx (Fx OR Gx) ⊢ SOMExFx OR SOMExGx} PL {1} {1} {SOMEx (Fx OR Gx)} {A} PL {2} {2} {Fa OR Ga} {A} PL {3} {3} {EST(a)} {A} PL {4} {4} {Fa} {A} PL {3,4} {5} {SOMEx Fx} {3, 4 SOMEIf} PL {3,4} {6} {SOMExFx OR SOMExGx} {5 ORI} PL {5} {7} {Ga} {A} PL {3,5} {8} {SOMEx gx} {3, 7 SOMEIf} PL {3,5} {9} {SOMExFx OR SOMExGx} {8 ORI} PL {2,3} {10} {SOMExFx OR SOMExGx} {2, 6 [4], 9 [5] ORE} PL {1} {11} {SOMExFx OR SOMExGx} {1, 10 [2, 3] SOMEEf} EP EH | Try it | Answer | |
| ALLx(Fx IMP Gx) ⊢ ALLx((Fx AND Hx) IMP (Gx AND Hx)) | SH {Sample proof 405 (in free logic)} SP {ALLx (Fx IMP Gx) ⊢ ALLx ((Fx AND Hx) IMP (Gx AND Hx))} PL {1} {1} {ALLx (Fx IMP Gx)} {A} PL {2} {2} {EST(a)} {A} PL {3} {3} {Fa AND Ha} {A} PL {3} {4} {Fa} {3 ANDE} PL {3} {5} {Ha} {3 ANDE} PL {1,2} {6} {Fa IMP Ga} {1, 2 ALLEf} PL {1,2,3} {7} {Ga} {4, 6 IMPE} PL {1,2,3} {8} {Ga AND Ha} {5, 7 ANDI} PL {1,2} {9} {(Fa AND Ha) IMP (Ga AND Ha)} {8 [3] IMPI} PL {1} {10} {ALLx ((Fx AND Hx) IMP (Gx AND Hx))} {9 [2] ALLIf} EP EH | Try it | Answer | |
| ALLx(Fx IMP Gx) SOMEx(Fx AND Hx) ⊢ SOMEx(Gx AND Hx) | SH {Sample proof 406 (in free logic)} SP {ALLx (Fx IMP Gx), SOMEx (Fx AND Hx) ⊢ SOMEx (Gx AND Hx)} PL {1} {1} {ALLx (Fx IMP Gx)} {A} PL {2} {2} {SOMEx (Fx AND Hx)} {A} PL {3} {3} {Fa AND Ha} {A} PL {4} {4} {EST(a)} {A} PL {3} {5} {Fa} {3 ANDE} PL {3} {6} {Ha} {3 ANDE} PL {1,4} {7} {Fa IMP Ga} {1, 4 ALLEf} PL {1,3,4} {8} {Ga} {5, 7 IMPE} PL {1,3,4} {9} {Ga AND Ha} {6, 8 ANDI} PL {1,3,4} {10} {SOMEx (Gx AND Hx)} {4, 9 SOMEIf} PL {1,2} {11} {SOMEx (Gx AND Hx)} {2, 10 [3, 4] SOMEEf} EP EH | Try it | Answer | |
| ALLxALLy(Fx IMP Gy) ⊢ SOMExFx IMP ALLyGy | SH {Sample proof 407 (in free logic)} SP {ALLxALLy (Fx IMP Gy) ⊢ SOMExFx IMP ALLyGy} PL {1} {1} {ALLxALLy (Fx IMP Gy)} {A} PL {2} {2} {SOMEx Fx} {A} PL {3} {3} {Fa} {A} PL {4} {4} {EST(a)} {A} PL {1,4} {5} {ALLy (Fa IMP Gy)} {1, 4 ALLEf} PL {5} {6} {EST(b)} {A} PL {1,4,5} {7} {Fa IMP Gb} {5, 6 ALLEf} PL {1,3,4,5} {8} {Gb} {3, 7 IMPE} PL {1,3,4} {9} {ALLy Gy} {8 [5] ALLIf} PL {1,2} {10} {ALLy Gy} {2, 9 [3, 4] SOMEEf} PL {1,2} {11} {SOMExFx IMP ALLyGy} {2, 9 [3, 4] SOMEEf} EP EH | Try it | Answer | |
| ALLx Fx ⊢ Fa OR NOTEST(a) | SH {Sample proof 408 (in free logic)} SP {ALLx Fx ⊢ Fa OR NOTEST(a)} PL {1} {1} {ALLx Fx} {A} PL {2} {2} {NOT(Fa OR NOTEST(a))} {A} PL {3} {3} {EST(a)} {A} PL {1,3} {4} {Fa} {1, 3 ALLEf} PL {1,3} {5} {Fa OR NOTEST(a)} {4 ORI} PL {1,2} {6} {NOTEST(a)} {2, 5 [3] RAA} PL {1,2} {7} {Fa OR NOTEST(a)} {6 ORI} PL {1} {8} {NOTNOT(Fa OR NOTEST(a))} {2, 7 [2] RAA} PL {1} {9} {Fa OR NOTEST(a)} {8 NOTNOTE} EP EH | Try it | Answer | |
| ALLx Fx, ALLx NOTFx ⊢ NOTSOMEx Gx | SH {Sample proof 409 (in free logic)} SP {ALLx Fx, ALLx NOTFx ⊢ NOTSOMEx Gx} PL {1} {1} {ALLx Fx} {A} PL {2} {2} {ALLx NOTFx} {A} PL {3} {3} {SOMEx Gx} {A} PL {4} {4} {Ga} {A} PL {5} {5} {EST(a)} {A} PL {1,5} {6} {Fa} {1, 5 ALLEf} PL {2,5} {7} {NOTFa} {2, 5 ALLEf} PL {1,2,5} {8} {NOTSOMEx Gx} {6, 7 [3] RAA} PL {1,2,3} {9} {NOTSOMEx Gx} {3, 8 [4, 5] SOMEEf} PL {1,2} {10} {NOTSOMEx Gx} {3, 9 [3] RAA} EP EH | Try it | Answer | |
| ALLx(p AND Fx) ⊢ p OR ALLxGx | SH {Sample proof 410 (in free logic)} SP {ALLx (p AND Fx) ⊢ p OR ALLxGx} PL {1} {1} {ALLx (p AND Fx)} {A} PL {2} {2} {NOT(p OR ALLxGx)} {A} PL {3} {3} {EST(a)} {A} PL {1,3} {4} {p AND Fa} {1, 3 ALLEf} PL {1,3} {5} {p} {4 ANDE} PL {1,3} {6} {p OR ALLxGx} {5 ORI} PL {1,2,3} {7} {NOTNOTGa} {2, 6 [ ] RAA} PL {1,2,3} {8} {Ga} {7 NOTNOTE} PL {1,2} {9} {ALLxGx} {8 [3] ALLIf} PL {1,2} {10} {p OR ALLxGx} {9 ORI} PL {1} {11} {NOTNOT(p OR ALLxGx)} {2, 10 [2] RAA} PL {1} {12} {p OR ALLxGx} {11 NOTNOTE} EP EH | Try it | Answer | |
| ⊢ SOMExFx OR SOMExNOTFx OR ALLxGx | SH {Sample proof 411 (in free logic)} SP {⊢ SOMExFx OR SOMExNOTFx OR ALLxGx} PL {1} {1} {NOT(SOMExFx OR SOMExNOTFx OR ALLxGx)} {A} PL {2} {2} {EST(a)} {A} PL {3} {3} {Fa} {A} PL {2,3} {4} {SOMEx Fx} {2, 3 SOMEIf} PL {2,3} {5} {SOMExFx OR SOMExNOTFx} {4 ORI} PL {2,3} {6} {SOMExFx OR SOMExNOTFx OR ALLxGx} {5 ORI} PL {1,2} {7} {NOTFa} {1, 6 [3] RAA} PL {1,2} {8} {SOMExNOTFx} {7 SOMEIf} PL {1,2} {9} {SOMExFx OR SOMExNOTFx} {8 ORI} PL {1,2} {10} {SOMExFx OR SOMExNOTFx OR ALLxGx} {9 ORI} PL {1,2} {11} {NOTNOTGa} {1, 10 [ ] RAA} PL {1,2} {12} {Ga} {11 NOTNOTE} PL {1} {13} {ALLx Gx} {12 [2] ALLIf} PL {1} {14} {SOMExFx OR SOMExNOTFx OR ALLxGx} {13 ORI} PL { } {15} {NOTNOT(SOMExFx OR SOMExNOTFx OR ALLxGx)} {1, 14 [1] RAA} PL { } {16} {SOMExFx OR SOMExNOTFx OR ALLxGx} {15 NOTNOTE} EP EH | Try it | Answer |