Now let's look at a couple of examples
that illustrate how equational reasoning
interacts with relational reasoning. The
father Quincy is Pat, fathers are older
than their children. Our job is to prove
that Pat is older than Quincy. As usual,
we start with our premises. If father of
Quincy is Pat, and fathers are older than
their children. First we use universal
elimination to stantiate our quantified
sentence. The father of Quincy is older
than Quincy. Next we use equality
elimination to replace father of Quincy
with Pat. And they're might derives a
conclusion that Pat is older than Quincy.
A conclusion that we wanted. Here's a
slightly more complicated example. We know
that p(a) is true and we know that p(b) is
true. Supposed we also know that a = c or
b = c but we do not know which. Let's
approve that despite this uncertainty we
still know that p(c) is true. Premises to
start p(a) p(b) and the disjunction a = c
or b = c. We start a new sub proof with
the assumption a = c. From this assumption
and our first premise, we can conclude
that p of c must be true. Of course we're
not done yet since we have proved the
result only under the assumption that a =
c. We make this clear with the reuse of
implication introduction to derive the
sentence a=z implies p of (c). Now, we
start another proof, sub proof this time
with the assumption b=c. As before, we
derive p of (c) and from this, we derive
the implication, e=c implies p of (c).
Finally, we use an or elimination to
combine our two partial results with our
disjunction of equations to produce p of c
at the top level.