# 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} EPThis 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} EPThis 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!