1
00:00:00,000 --> 00:00:05,896
Now let's look at a couple of examples
that illustrate how equational reasoning

2
00:00:05,896 --> 00:00:11,720
interacts with relational reasoning. The
father Quincy is Pat, fathers are older

3
00:00:11,720 --> 00:00:18,211
than their children. Our job is to prove
that Pat is older than Quincy. As usual,

4
00:00:18,211 --> 00:00:24,074
we start with our premises. If father of
Quincy is Pat, and fathers are older than

5
00:00:24,074 --> 00:00:31,362
their children. First we use universal
elimination to stantiate our quantified

6
00:00:31,362 --> 00:00:38,182
sentence. The father of Quincy is older
than Quincy. Next we use equality

7
00:00:38,182 --> 00:00:43,691
elimination to replace father of Quincy
with Pat. And they're might derives a

8
00:00:43,691 --> 00:00:51,673
conclusion that Pat is older than Quincy.
A conclusion that we wanted. Here's a

9
00:00:51,673 --> 00:00:58,287
slightly more complicated example. We know
that p(a) is true and we know that p(b) is

10
00:00:58,287 --> 00:01:04,650
true. Supposed we also know that a = c or
b = c but we do not know which. Let's

11
00:01:04,650 --> 00:01:13,278
approve that despite this uncertainty we
still know that p(c) is true. Premises to

12
00:01:13,278 --> 00:01:24,033
start p(a) p(b) and the disjunction a = c
or b = c. We start a new sub proof with

13
00:01:24,033 --> 00:01:31,730
the assumption a = c. From this assumption
and our first premise, we can conclude

14
00:01:31,730 --> 00:01:37,046
that p of c must be true. Of course we're
not done yet since we have proved the

15
00:01:37,046 --> 00:01:44,254
result only under the assumption that a =
c. We make this clear with the reuse of

16
00:01:44,254 --> 00:01:52,039
implication introduction to derive the
sentence a=z implies p of (c). Now, we

17
00:01:52,039 --> 00:01:58,935
start another proof, sub proof this time
with the assumption b=c. As before, we

18
00:01:58,935 --> 00:02:05,680
derive p of (c) and from this, we derive
the implication, e=c implies p of (c).

19
00:02:07,180 --> 00:02:12,564
Finally, we use an or elimination to
combine our two partial results with our

20
00:02:12,564 --> 00:02:16,760
disjunction of equations to produce p of c
at the top level.