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.