Appendix: Examples Expressing generality

Proof 1

SP {ALLx ALLy (Rxy OR Ryx) ⊢ ALLx Rxx} PL {1} {1} {ALLx ALLy (Rxy OR Ryx)} {A} PL {1} {2} {ALLy (Ray OR Rya)} {1 ALLE} PL {1} {3} {Raa OR Raa} {2 ALLE} PL {4} {4} {Raa} {A} PL {1} {5} {Raa} {3, 4 [4], 4 [4] ORE} PL {1} {6} {ALLx Rxx} {5 ALLI} EP

If all x and y are related one way or the other, then everything is related to itself. Why? Well, one of the cases is where x and y are the same thing, in which case Rxy and Ryx come to the same as well. The proof follows this reasoning. Instantiating both x and y to the same thing a (lines 2 and 3) produces a formula of the form p OR p, which we have already seen in Chapter 3 of these notes is equivalent to p. Finally, the application of ALLI is allowed because no assumptions have been made about a.

Proof 2

SP {ALLx (Fx IMP Gx) ⊢ ALLx (SOMEy (Fy AND Pxy) IMP SOMEz (Gz AND Pxz))} PL {1} {1} {ALLx (Fx IMPGx)} {A} PL {2} {2} {SOMEy (Fy AND Pay)} {A} PL {3} {3} {Fb AND Pab} {A} PL {3} {4} {Fb} {3 ANDE} PL {3} {5} {Pab} {3 ANDE} PL {1} {6} {Fb IMP Gb} {1 ALLE} PL {1,3} {7} {Gb} {4, 6 IMPE} PL {1,3} {8} {Gb AND Pab} {5, 7 ANDI} PL {1,3} {9} {SOMEz (Gz AND Paz)} {8 SOMEI} PL {1,2} {10} {SOMEz (Gz AND Paz)} {2, 9 [3] SOMEE} PL {1} {11} {SOMEy (Fy AND Pay) IMP SOMEz (Gz AND Paz)} {10 [2] IMPI} PL {1} {12} {ALLx (SOMEy (Fy AND Pay) IMP SOMEz (Gz AND Paz))} {11 ALLI} EP

This argument form was famously noted in the 19th century by Augustus De Morgan, who pointed out that the argument

All horses are animals;
therefore all horses' heads are animals' heads

is obviously valid but cannot be formulated in the formal systems of logic of the time. Attempts to deal with anomalies like this were a significant factor in the development of modern symbolic logic.

Proof 3

SP {ALLx (Fx OR Rxa), ALLy ALLz (Rf(y)z IMP Gz) ⊢ ALLx(Ff(x) OR Ga)} PL {1} {1} {ALLx(Fx OR Rxa)} {A} PL {2} {2} {ALLy ALLz (Rf(y)z IMP Gz)} {A} PL {1} {3} {Ff(b) OR Rf(b)a} {1 ALLE} PL {2} {4} {ALLz (Rf(b)z IMPGz)} {2 ALLE} PL {2} {5} {Rf(b)a IMP Ga} {4 ALLE} PL {6} {6} {Ff(b)} {A} PL {6} {7} {Ff(b) OR Ga} {6 ORI} PL {8} {8} {Rf(b)a} {A} PL {2,8} {9} {Ga} {5,8 IMPE} PL {2,8} {10} {Ff(b) OR Ga} {9 ORI} PL {1,2} {11} {Ff(b) OR Ga} {3, 7 c[6], 10 [8] ORE} PL {1,2} {12} {ALLx (Ff(x) OR Ga)} {11 ALLI} EP

This slightly more complicated example illustrates the technique of making substitutions so as to unify two atomic formulae. The expressions Rxa in the first premise and Rf(y)z in the second have instances in common. One of the simplest of these is obtained by substituting f(x) for x, x for y and a for z. The conclusion is then the result of cutting out the common formula Rf(x)a, leaving the disjunction of the other atoms with the substitution applied. In our calculus, of course, we have to go further and substitute a constant (name) b for x in order to strip off the quantifiers and do some propositional reasoning before putting the quantifier back at line 12. This style of inference, called "unification and resolution", is the basis of most automated reasoning for first order logic. Machines find it easier than we do!