1
00:00:00,920 --> 00:00:07,722
The property that we have seen this far
are only part of the story. This is also

2
00:00:07,722 --> 00:00:14,524
substitution of equals for equals. Suppose
we believe the f of (a) = b and f of (b) =

3
00:00:14,524 --> 00:00:20,561
A. We'd like to prove f of (a) = a
Unfortunately, with our formalization does

4
00:00:20,561 --> 00:00:26,938
far, we cannot do this. Reflectivity does
not help us here since neither our

5
00:00:26,938 --> 00:00:33,570
premises nor our conclusion are reflexive.
All we can do with symmetry is to turn

6
00:00:33,570 --> 00:00:40,004
around the arguments on our premises and
our conclusion. For example, we're writing

7
00:00:40,004 --> 00:00:44,869
f (a) = b as b = f (A). We're writing f
(b) = a as a = F (b) and transitivity just

8
00:00:44,869 --> 00:00:50,833
to interpose new terms. Are there
variables for functional expressions about

9
00:00:50,833 --> 00:00:56,701
which we know nothing? The solution for
this problem is a substitution of equals

10
00:00:56,701 --> 00:01:01,895
for equals. If two terms are equal, then
any sentence involving one term should

11
00:01:01,895 --> 00:01:06,955
have the same truth value as that same
sentence involving the other term. In

12
00:01:06,955 --> 00:01:12,148
other words, we can substitute one term
for the other and any sentence without

13
00:01:12,148 --> 00:01:18,338
changing its truth value. We again express
this notion of substitute ability by

14
00:01:18,338 --> 00:01:24,779
writing substitution axioms for our
functions, for sense from here for example

15
00:01:24,779 --> 00:01:30,947
isn't is a case of a unary function. The
second sentence is an example for the case

16
00:01:30,947 --> 00:01:35,284
of a binary function Now that we need to
allow for equations for each of the

17
00:01:35,284 --> 00:01:42,506
arguments of our functional terms. Now
let's look at the problem we saw earlier.

18
00:01:42,506 --> 00:01:50,784
We know that f of a = b and f of b = a. We
include our axioms of equality and this

19
00:01:50,784 --> 00:01:58,636
time we include a substitution axiom for
the function f. Our first step is to

20
00:01:58,636 --> 00:02:05,718
instantiate the substitution axiom with
terms of our premises and our conclusion.

21
00:02:05,718 --> 00:02:13,955
Let x be b, and let y be f of a, and let z
be a. F of b = a and b = f of a implies

22
00:02:13,955 --> 00:02:23,057
that f of f of a = a. Now we instantiate
our symmetry axiom, that's if b = a

23
00:02:23,057 --> 00:02:31,120
implies b = f of a And we use implication
elimination on this result to derive b = f

24
00:02:31,120 --> 00:02:40,654
(A). We can join our second premise with
this result to produce the conjunction. F

25
00:02:40,654 --> 00:02:47,393
(b) = a and b = f (A). And finally, we use
implication and elimination to derive our

26
00:02:47,393 --> 00:02:54,672
overall result. Note that we need
substitution axioms for relations as well

27
00:02:54,672 --> 00:03:00,292
as functions. And again, in our multiple
arguments we must allow for equations with

28
00:03:00,292 --> 00:03:07,586
each of the arguments. This exercise tests
your understanding of the quality by

29
00:03:07,586 --> 00:03:11,240
asking you to answer some questions about
substitution.