Appendix: Examples Expressing generality
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.
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.
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!