Besides quantifiers, FOL also has the identity predicate, =.

We can build = into formal proofs just like the other symbols, by adding Intro and Elim rules.

=Elim is how we use an = sentence.

We will start with =Elim. Remember, to use an Elim rule you must already have a sentence with that symbol.

Let’s see if you can figure out how to cite it.

If we know p=a, then p and a are two names for the same object.

That means you can substitute one name for the other in any sentence of FOL, like we did above.

When you cite =Elim, you must always cite exactly two things.

When you cite =Elim, you must always cite exactly two things: the = you are “eliminating”, or using to do the substitution, as well as the sentence that you are doing the substitution into.

If this seems familiar, you’re right! It is exactly how substitutions in math with = work.

In algebra, for example, you might have learned how to solve equations with multiple unknowns:

a+2=3

2b+a=5

We first compute a=1 from the top equation. Then we * use* that identity to do a substitution in the second equation:

2b+1=5

When we do that, we are doing =Elim.

When you do substitutions with =Elim, the order of the names doesn’t matter. For example, whether the order is a=1 or 1=a.

Those = sentences are logically equivalent, and you can use either one to do a substitution of a for 1 or 1 for a.

Just like all rules, though, we write the citation numbers in numerical order.

=Elim also allows us to substitute * one or more* occurrences of a name.

=Elim also allows us to substitute * one or more* occurrences of a name.

Say we know:

1. a=b

2. T(a,e,a,c)

Premise

Premise

=Elim always cites the = we are using for the substitution, as well as the sentence we are substituting into.

This can get confusing, though, if the sentence we are substituting into is * also* an identity.

In that problem, we need to ignore premise 2.

**Transitivity of identity:** if a=b and b=c, then a=c.

If we know a=b (premise 1) and b=c (premise 3), then we know a=c. That is called the * transitivity of identity*.

It might seem weird that we can justify a=c with =Elim, though, because a=c still has identity in it!

Here’s what’s going on. Both lines we cite are = sentences, and we are only eliminating * one* of them, the one we are using for the substitution.

It just so happens that the sentence we are substituting into is also an identity, and we don’t get rid of that one.

Now, you might be wondering which identity we are “eliminating” in this example, premise 1 or premise 3?

The answer is that it doesn’t matter. Either way, it comes to the same thing.

If you want to use multiple different identities, you have to do it one step at a time.

Our last lesson about =Elim is this. Since =Elim requires citing exactly 2 lines, if you want to use multiple different identities, you have to do it one step at a time.

Say we know:

1. a=e

2. b=c

3. R(a,b)

Premise

Premise

Premise

If we want to prove R(e,c) we are * not* allowed to write it on line 4 with the justification =Elim;1,2,3 because we can’t cite three lines with =Elim.

See if you can figure out how we did it below.

The way we did it above is not the only correct way to complete that proof.

See if you can figure out below the other way that takes the same number of lines.

Login

Accessing this textbook requires a login. Please enter your credentials below!