THE LOGIC NOTES

Appendix: Examples Identity and existence

The following proofs illustrate the rules of immediate consequence for identity and for quantifiers in free logic.

Proof 1

SP {ALLx(Fx IMP x=a), SOMEx(Fx AND Gx) ⊢ ALLx(Fx IMP Gx)} PL {1} {1} {ALLx (Fx IMP x=a)} {A} PL {2} {2} {SOMEx (Fx AND Gx)} {A} PL {3} {3} {Fb} {A} PL {1} {4} {Fb IMP b=a} {1 ALLE} PL {1,3} {5} {b=a} {3, 4 IMPE} PL {6} {6} {Fc AND Gc} {A} PL {6} {7} {Fc} {6 ANDE} PL {6} {8} {Gc} {6 ANDE} PL {1} {9} {Fc IMP c=a} {1 ALLE} PL {1,6} {10} {c=a} {7, 9 IMPE} PL {1,6} {11} {Ga} {8, 10 =E} PL {1,3,6} {12} {Gb} {5, 11 =E} PL {1,2,3} {13} {Gb} {2, 12 [6] SOMEE} PL {1,2} {14} {Fb IMP Gb} {13 [3] IMPI} PL {1,2} {15} {ALLx(Fx IMP Gx)} {14 ALLI} EP

If there is only one F, then among the Fs, "some" is the same as "all". The proof requires names b and c which must be different from each other, and from a, so that the side conditions on the SOMEE and ALLI rules are met.


Proof 2

SP {SOMEx (Fx AND Gx), SOMEx (Fx AND NOTGx) ⊢ NOTALLxALLy ((Fx AND Fy) IMP x=y)} PL {1} {1} {SOMEx (Fx AND Gx)} {A} PL {2} {2} {SOMEx (Fx AND NOTGx)} {A} PL {3} {3} {ALLxALLy ((Fx AND Fy) IMP x=y)} {A} PL {4} {4} {Fa AND Ga} {A} PL {4} {5} {Fa} {4 ANDE} PL {4} {6} {Ga} {4 ANDE} PL {7} {7} {Fb AND NOTGb} {A} PL {7} {8} {Fb} {7 ANDE} PL {7} {9} {NOTGb} {7 ANDE} PL {3} {10} {ALLy ((Fa AND Fy) IMP a=y)} {3 ALLE} PL {3} {11} {(Fa AND Fb) IMP a=b} {10 ALLE} PL {4,7} {12} {Fa AND Fb} {5, 8 ANDI} PL {3,4,7} {13} {a=b} {11, 12 IMPE} PL {3,4,7} {14} {Gb} {6, 13 =E} PL {4,7} {15} {NOTALLxALLy ((Fx AND Fy) IMP x=y)} {9, 14 [3] RAA} PL {2,4} {16} {NOTALLxALLy ((Fx AND Fy) IMP x=y)} {2, 15 [7] SOMEE} PL {1,2} {17} {NOTALLxALLy ((Fx AND Fy) IMP x=y)} {1, 16 [4] SOMEE} EP

Proof 3 (in free logic)

SP {NOTALLx Fx ⊢ SOMEx NOTFx} PL {1} {1} {NOTALLx Fx} {A} PL {2} {2} {NOTSOMEx NOTFx} {A} PL {3} {3} {EST(a)} {A} PL {4} {4} {NOTFa} {A} PL {3,4} {5} {SOMEx NOTFx} {3, 4 SOMEIf} PL {2,3} {6} {NOTNOTFa} {2, 5 [4] RAA} PL {2,3} {7} {Fa} {6 NOTNOTE} PL {2} {8} {ALLx Fx} {7 [3] ALLIf} PL {1} {9} {NOTNOTSOMEx NOTFx} {1, 8 [2] RAA} PL {1} {10} {SOMEx NOTFx} {9 NOTNOTE} EP

Proof 4 (in free logic)

SP {SOMEx NOTFx ⊢ NOTALLx Fx} PL {1} {1} {SOMEx NOTFx} {A} PL {2} {2} {EST(a)} {A} PL {3} {3} {NOTFa} {A} PL {4} {4} {ALLx Fx} {A} PL {2,4} {5} {Fa} {2, 4 ALLEf} PL {2,3} {6} {NOTALLx Fx} {3, 5 [4] RAA} PL {1} {7} {NOTALLx Fx} {1, 6 [2,3] SOMEEf} EP

These two proofs, showing that the duality between the existential and universal quantifiers still holds in free logic, should be compared with the analogous proofs of the same sequents in ordinary first order logic. The extra assumption that a exists is needed, for the SOMEIf move in the proof 3 and the ALLEf move in proof 4; in each case it is discharged by the dual quantifier rule.


Proof 5 (in free logic)

SP {p, SOMEx Gx ⊢ SOMEx (p OR Fx)} PL {1} {1} {p} {A} PL {2} {2} {SOMEx Gx} {A} PL {3} {3} {EST(a)} {A} PL {4} {4} {Ga} {A} PL {1} {5} {p OR Fa} {1 ORI} PL {1,3} {6} {SOMEx (p OR Fx)} {3, 5 SOMEIf} PL {1,2} {7} {SOMEx (p OR Fx)} {2, 6 [3,4] SOMEEf} EP

The third assumption is essential, as the existence of a is required at line 6. Note that the discharge of assumption 4 on line 7 is vacuous as it does not matter for this purpose whether a is a G or not, but only that it exists.