1
00:00:01,800 --> 00:00:06,618
As we have seen, we can use Fitch to
create proofs for theories with equality

2
00:00:06,618 --> 00:00:11,561
by adding the equality and substitution
axioms to our premise set. However, this

3
00:00:11,561 --> 00:00:16,692
is not the only way to go. Since equality
of such pervasive and important relation,

4
00:00:16,692 --> 00:00:21,635
it makes sense to treat it especially in
our proof system. In this section we're

5
00:00:21,635 --> 00:00:26,328
going to show how to extend Fitch to
handle equations and it turns out all we

6
00:00:26,328 --> 00:00:31,918
need is one axiom schema and one rule of
inference. Our axiom scheme is called

7
00:00:31,918 --> 00:00:37,886
equality introduction or QI. It allows us
to write down arbitrary equations with the

8
00:00:37,886 --> 00:00:44,192
first term and the second term, are equal.
For example, without any premises

9
00:00:44,192 --> 00:00:51,362
whatsoever, we can write down equations
like a = a and f of a = f of a and even

10
00:00:51,362 --> 00:01:00,562
non-ground equations like f of x = f of x.
Our rule of inference is called equality

11
00:01:00,562 --> 00:01:06,106
elimination or QE. Equality of elimination
tells us that when we have an equation and

12
00:01:06,106 --> 00:01:10,231
a sentence containing one or more
occurrences of one of the terms in the

13
00:01:10,231 --> 00:01:14,978
equation. Then we can deduce a version of
the sentence to which that term replace by

14
00:01:14,978 --> 00:01:19,432
the other term in the equation. In order
to avoid the unintended capture of

15
00:01:19,432 --> 00:01:24,101
variables query requires that the
replacement must be substitutable for the

16
00:01:24,101 --> 00:01:29,015
term being replaced in the sentence. This
is the same substitutability condition

17
00:01:29,015 --> 00:01:33,438
that adorns the, universal, the
elimination rule of instance that we saw

18
00:01:33,438 --> 00:01:38,230
earlier. Now that the equation in the
equality elimination rule can be used in

19
00:01:38,230 --> 00:01:43,451
either direction and that is an occurrence
of Tal one can be replace by Tal two or in

20
00:01:43,451 --> 00:01:50,119
occurrence of Tal two can be replaced by
Tal one. For example, if we have the

21
00:01:50,119 --> 00:01:57,745
identity x equals b, and the sentence
[inaudible]. We can infer [inaudible] of

22
00:01:57,745 --> 00:02:07,253
xb. You can also infer [inaudible] of bx
and we can even infer [inaudible] of. See

23
00:02:07,253 --> 00:02:13,189
how this features helping proofs of
equality. Let's assume consider one of the

24
00:02:13,189 --> 00:02:18,980
properties we saw earlier in the lesson
namely proving a = c from b = a and b = c.

25
00:02:20,040 --> 00:02:26,760
Here's the old proof with the two premises
and three equality axioms and five steps

26
00:02:26,760 --> 00:02:33,032
of proof. And here's is the proof in our m
odified [inaudible] system. We are in two

27
00:02:33,032 --> 00:02:42,176
premises and just one step of reduction.
That's all that is needed. Here's the

28
00:02:42,176 --> 00:02:49,698
other problem we saw earlier. From f(a) =
b and f(b) = a. We want to prove f(f)(a) =

29
00:02:49,698 --> 00:02:56,127
a. Once again we have our old proof Two
premises, three equality axioms, one

30
00:02:56,127 --> 00:03:02,040
substitution axiom, and five steps of
proof. And here is the proof in our

31
00:03:02,040 --> 00:03:07,291
modified Fitch system. Again, we have two
premises and once again just one step of

32
00:03:07,291 --> 00:03:13,124
deduction. Building things into our system
makes much shorter proofs. This exercise

33
00:03:13,124 --> 00:03:16,700
is test to understanding a fetch with
equality.