The property that we have seen this far
are only part of the story. This is also
substitution of equals for equals. Suppose
we believe the f of (a) = b and f of (b) =
A. We'd like to prove f of (a) = a
Unfortunately, with our formalization does
far, we cannot do this. Reflectivity does
not help us here since neither our
premises nor our conclusion are reflexive.
All we can do with symmetry is to turn
around the arguments on our premises and
our conclusion. For example, we're writing
f (a) = b as b = f (A). We're writing f
(b) = a as a = F (b) and transitivity just
to interpose new terms. Are there
variables for functional expressions about
which we know nothing? The solution for
this problem is a substitution of equals
for equals. If two terms are equal, then
any sentence involving one term should
have the same truth value as that same
sentence involving the other term. In
other words, we can substitute one term
for the other and any sentence without
changing its truth value. We again express
this notion of substitute ability by
writing substitution axioms for our
functions, for sense from here for example
isn't is a case of a unary function. The
second sentence is an example for the case
of a binary function Now that we need to
allow for equations for each of the
arguments of our functional terms. Now
let's look at the problem we saw earlier.
We know that f of a = b and f of b = a. We
include our axioms of equality and this
time we include a substitution axiom for
the function f. Our first step is to
instantiate the substitution axiom with
terms of our premises and our conclusion.
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
that f of f of a = a. Now we instantiate
our symmetry axiom, that's if b = a
implies b = f of a And we use implication
elimination on this result to derive b = f
(A). We can join our second premise with
this result to produce the conjunction. F
(b) = a and b = f (A). And finally, we use
implication and elimination to derive our
overall result. Note that we need
substitution axioms for relations as well
as functions. And again, in our multiple
arguments we must allow for equations with
each of the arguments. This exercise tests
your understanding of the quality by
asking you to answer some questions about
substitution.