METHODS OF PROOF  (chapter 4)

We now make use of the ideas in chapters 2 and 3, to help us examine
methods for proving ordinary mathematical statements.

Most mathematical statements of interest have the form

(i) ForAll x (Px --> Qx)

although we also sometimes encounter the forms

(ii) Exists x (Px)

(iii) ~ForAll x (Px)

(iv) ~Exists x (Px)

We will mostly study type (i); but here are a few brief comments on
the others:  (ii) is most commonly proved by actually finding a value
for x that makes P(x) true; (iii) is logically equiv to Exists x (~Px)
and so is a case of type (ii); and (iv) is equivalent to ForAll x
(~Px), and the methods we will see for type (i) apply to it as well.

So now we turn to type (i).  There are several methods, including
induction which we will get to in chapter 5 (induction). For now we
concentrae on "direct" methods, which have this general form:

To prove ForAll x (Px --> Qx), start by assuming Px, and then in
a series of inference steps arrive at the conclusion Qx.  [It may seem
that this is the only way: show how to get from Px to Qx. But there
are "indirect" other ways, which we will see later.]  There are
however a few subtleties that are important. Let's start with an
example:

We will prove 
ForAll x [(x+1)^2 = x^2 + 2x + 1], where the intended domain is the
real numbers.
   Proof: Let x be a real number. We calculate:
          (x+1)^2 = (x+1)(x+1) = x^2 + x + x + 1
                  = x^2 + 2x + 1
          and so ForAll x [(x+1)^2 = x^2 + 2x + 1]

Comment: this is boringly obvious. But one thing needs to be pointed
out. We started with "Let x be a real number". But we are supposed to
prove ForAll x, not one particular x. So what we really mean by that
"Let" statement is this: x is a "generic particular", a stand-in for
an unknown (arbitrary, unspecified) real that could end up being any
real at all. So we leave off the ForAll x, and use a generic x whose
value we deliberately do not specify, precisely so that whatever we
say about it will apply to all possible values x could have (namely,
all reals). And that when we conclude something about x (such as the
equation above) we know that it holds no matter which value x has, and
that justifies our putting the ForAll x back on at the end.

Here is a slightly more complex example:
Theorem: The square of any odd number is odd.
Proof: We rewrite this as
       ForAll x [ Odd(x) --> Odd(x^2) ]
       and the we let x be a generic odd number. 
 [We need now to show that x^2 is also odd; but how?  We need to
  turn the notion of being odd into something we can do algebra
  with.] 
       By definition of "odd", x = 1 + 2n for some natural number n.
       Then we must show x^2 = 1 + 2m for some m.
       But x^2 = (1+2n)(1+2n) = 1 + 4n + 4n^2
               = 1 + 2(2n + 2n^2) = 1 + 2m, where m = (2n + 2n^2).
       So x^2 is odd.
       Finally, since x is a generic odd number, we conclude that
       ForAll x [ Odd(x) --> Odd(x^2) ].

This example, while also simple and obvious, illustrates more clearly
the crucial steps in proving ForAll x (Px --> Qx):
  - pick a generic particular satisfying Px
  - recall the definitions of key concepts expressed in P
  - show Qx
  - conclude ForAll x (Px --> Qx)

This is called the Method of Generalizing from the Generic Particular.
It is the most common method of proof in mathematics, and is very
powerful. Without it, we would have to prove each case (i.e. for each
separate value of x) separately, which would be tedious in a large
domain of x values, and impossible in infinite domains.  While the
above examples do not prove anything we did not already know very
well, we will give plenty of examples of far richer theorems that can
be proved by this same method.