1
00:00:02,780 --> 00:00:08,940
The semantics of relational logic is not
by itself to tell us which terms are equal

2
00:00:08,940 --> 00:00:14,660
and which are not. In fact, it's possible
for every term to refer to a distinct

3
00:00:14,660 --> 00:00:20,453
object in the real world and it's possible
for every term to refer to the same

4
00:00:20,453 --> 00:00:25,953
object. Well, the semantics relational
logic does not constrain your quality

5
00:00:25,953 --> 00:00:31,600
relation. The idea of coreferentiality
does. For example, it's not possible for

6
00:00:31,600 --> 00:00:38,013
us to believe a=b and b=c and at the same
time, not believe a=c. We can capture

7
00:00:38,013 --> 00:00:44,873
these constraints through axioms. First of
all the equality relation must be

8
00:00:44,873 --> 00:00:52,004
reflexive. This means that the relation
holds of every term in the language for

9
00:00:52,004 --> 00:00:58,839
itself for all x, x = x. Relation must
also be symmetric. If two terms refer to

10
00:00:58,839 --> 00:01:05,367
the same thing, it does not matter which
one we write in the equation, for all x is

11
00:01:05,367 --> 00:01:11,355
equals y implies y=x. Finally the relation
must be transitive. If we believe that a =

12
00:01:11,355 --> 00:01:16,860
b refer to the same object and we believe
that b and c refer to the same object then

13
00:01:16,860 --> 00:01:23,576
a and c must refer to the same object as
well. Let's see how we can use these

14
00:01:23,576 --> 00:01:29,793
properties to solve some problems of
equality. Suppose we know that b = a and

15
00:01:29,793 --> 00:01:37,723
we know that b = c. Let's prove that a = c
as well. As usual we start our proof with

16
00:01:37,723 --> 00:01:46,154
our premises. B = a and b = c. We add our
axioms for equality First reflexivity then

17
00:01:46,154 --> 00:01:54,105
symmetry and then transitivity. Now we go
to work on the proof. First, we use two

18
00:01:54,105 --> 00:02:01,849
applications of universal elimination on
our symmetry axiom to derive the fact that

19
00:02:01,849 --> 00:02:12,115
b = a implies a = b. I'm substituting b
for x and a for y. We then use implication

20
00:02:12,115 --> 00:02:22,416
elimination on line six and line one to
produce a=b. We then use universal

21
00:02:22,416 --> 00:02:27,914
elimination again to instantiate the
transitivity axiom this time with x

22
00:02:27,914 --> 00:02:36,475
replaced by a, y replaced by b and z
replaced by c. We can join the result on

23
00:02:36,475 --> 00:02:42,207
line seven with the premise on line two
to, to derive the conjunction on line

24
00:02:42,207 --> 00:02:47,736
nine. And finally we use implication
elimination to derive our overall

25
00:02:47,736 --> 00:02:53,066
conclusion so it works as expected though
it's a bit lengthy. We'll see a so much

26
00:02:53,066 --> 00:02:59,325
faster way to solve problems like this in
j ust a short while. This exercise test,

27
00:02:59,325 --> 00:03:04,654
of understanding of equality by asking you
to prove the results, using the basic

28
00:03:04,654 --> 00:03:05,720
equality axioms.