As we have seen, we can use Fitch to
create proofs for theories with equality
by adding the equality and substitution
axioms to our premise set. However, this
is not the only way to go. Since equality
of such pervasive and important relation,
it makes sense to treat it especially in
our proof system. In this section we're
going to show how to extend Fitch to
handle equations and it turns out all we
need is one axiom schema and one rule of
inference. Our axiom scheme is called
equality introduction or QI. It allows us
to write down arbitrary equations with the
first term and the second term, are equal.
For example, without any premises
whatsoever, we can write down equations
like a = a and f of a = f of a and even
non-ground equations like f of x = f of x.
Our rule of inference is called equality
elimination or QE. Equality of elimination
tells us that when we have an equation and
a sentence containing one or more
occurrences of one of the terms in the
equation. Then we can deduce a version of
the sentence to which that term replace by
the other term in the equation. In order
to avoid the unintended capture of
variables query requires that the
replacement must be substitutable for the
term being replaced in the sentence. This
is the same substitutability condition
that adorns the, universal, the
elimination rule of instance that we saw
earlier. Now that the equation in the
equality elimination rule can be used in
either direction and that is an occurrence
of Tal one can be replace by Tal two or in
occurrence of Tal two can be replaced by
Tal one. For example, if we have the
identity x equals b, and the sentence
[inaudible]. We can infer [inaudible] of
xb. You can also infer [inaudible] of bx
and we can even infer [inaudible] of. See
how this features helping proofs of
equality. Let's assume consider one of the
properties we saw earlier in the lesson
namely proving a = c from b = a and b = c.
Here's the old proof with the two premises
and three equality axioms and five steps
of proof. And here's is the proof in our m
odified [inaudible] system. We are in two
premises and just one step of reduction.
That's all that is needed. Here's the
other problem we saw earlier. From f(a) =
b and f(b) = a. We want to prove f(f)(a) =
a. Once again we have our old proof Two
premises, three equality axioms, one
substitution axiom, and five steps of
proof. And here is the proof in our
modified Fitch system. Again, we have two
premises and once again just one step of
deduction. Building things into our system
makes much shorter proofs. This exercise
is test to understanding a fetch with
equality.