15.1 Introduction

In our discussion of Logic thus far, we have assumed that there is a one-to-one relationship between ground terms in our language and objects in the application area we are trying to describe. For example, in talking about people, we have been assuming a unique name for each person. In arithmetic, we have been assuming a unique term for each number. This makes things conceptually simple, and it is a reasonable way to go in many circumstances.

But not always. In natural language, we often find it convenient to use more than one term to refer to the same real world object. For example, we sometimes have multiple names for the same person - Michael, Mike, and so forth. And, in Arithmetic, we frequently use different terms to refer to the same number - 2+2, 2*2, and 4.

In Relational Logic, we can axiomatize the co-referentiality of terms in the form of equations. For example, to express the co-referentiality of f(a) and f(b), we write equal(f(a),f(b)). We can also distinguish terms by writing negated equations. To say that f(a) and f(b) refer to different objects, we write ¬equal(f(a),f(b)).

Since equality is such a common relation, in what follows we write equations with the infix operator =, for example writing (f(a)=f(b)) in place of equal(f(a),f(b)). However, this is just syntactic sugar. We must remember that, as far our logic is concerned, syntactically and semantically, an equation is a relational sentence involving a relation constant like any other.

We start this chapter by axiomatizing the equality relation as an ordinary binary relation. We then discuss the substitution of equals for equals in other expressions. Finally, we look at how to expand our proof system to reason with equality.

15.2 Properties of Equality

The semantics of Relational Logic does not, by itself, tell us which terms are equal and which are not. In fact, it is possible for each and every term to refer to a different object, and it is possible for all terms to refer to the same object.

Although the semantics of Relational Logic by itself does not constrain the equality relation, the idea of co-referentiality does impose some constraints. For example, we cannot believe a=b and b=c and at the same time believe that a≠c.

First of all, the equality relation must be reflexive. This means that the relation holds of every term in the language and itself.

The relation must also be symmetric. If two terms refer to the same thing, it does not matter which one we write first in an equation.

Finally, the relation must be transitive. If we believe that a and b refer to the same object and we believe that b and c refer to the same object, then a and c must refer to the same object as well.

The three properties of reflexivity, symmetry, and transitivity are the defining conditions for what is know as an equivalence relation, and equality is the quintessential example.

Let's see how we can use these properties to solve some problems of equality. Suppose we know that b=a and we know that b=c. The following is a proof that a=c. As usual, we start with our premises; and, since we are working with equations, we also include the three axioms of equality. We use two applications of Universal Elimination on our symmetry axiom to derive the sentence on line 6, substituting b for x and a for y. We then use Implication Elimination to conclude a=b. We then use Universal Elimination to instantiate the transitivity axiom, with x replaced by a, y replaced by b, and z replaced by c. We conjoin the result on line 7 with the premise on line 2 to derive the conjunction on line 9. Finally, we use Implication Elimination to derive our overall conclusion.

This proof is a little lengthy, but the method works. Later in the chapter, we show how to generate shorter proofs for simple results like this one.

15.3 Substitution

The properties of equality seen thus far are only part of the story. There is also substitution. If two terms are equal (i.e. they refer to the same object), then every sentence that is true of the first term must be true of the second; and every sentence that is false of the first term must be false of the second. In other words, it should be possible to substitute one term for an equal term without changing the truth value of any sentence. We can express this notion of substitutability by writing substitution axioms, one for each relation constant and one for each function constant in our vocabulary.

The sentence shown below is a substitution axiom for the unary relation constant p. If x=y and p(x) is true, then p(y) must also be true.

The following sentence is a substitution axiom for the binary relation constant q. Note that we need to allow for equations for all of the arguments of relational sentences.

The following is a substitution axiom for the unary function constant f.

Using the equality and substitution axioms, we can do proofs with equality. We simply add these additional axioms to our premises and prove our conclusions as before.

As an example, suppose that we believe f(a)=b and f(b)=a. Let's prove that f(f(a))=a. A proof of this conclusion using Fitch is shown below. The first two lines are our premises. The next four are our equality axioms and the substitution axiom for f.

A bit messy, but it works. The simpler approach is to use built-in rules of inference for equality, as described in the next section.

15.4 Fitch With Equality

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 is such a pervasive and important relation, it makes sense to treat it specially in our proof system. In this section we show how to extend Fitch to handle equations. As it turns out, all we need is one axiom schema and one rule of inference.

The Equality Introduction rule allows the insertion of an arbitrary instance of reflexivity.

For example, without any premises whatsoever, we can write down equations like (a=a) and (f(a)=f(a)) and (f(x)=f(x)).

Our second rule of inference is called Equality Elimination (QE). Equality 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 in which that term is replaced by the other term in the equation.

In order to avoid the unintended capture of variables, QE 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 Elimination rule of inference.

Note that the equation in the Equality Elimination rule can be used in either direction, i.e. an occurrence of τ₁ can be replaced by τ₂ or an occurrence of τ₂ can be replaced by τ₁.

The following is a proof of the result in Section 2 using these extensions in lieu of the equality axioms. Note that with these rules we can do the proof in a single step.

The following is a proof of the result in Section 3 using these two extensions in lieu of the equality and substitution axioms. Again, we can do the proof in a single step. Clearly, building things into our proof system makes for much shorter proofs.

Now, let's look at a couple of examples that illustrate how equational reasoning interacts with relational reasoning. We know that Quincy is the father of Pat, and we know that fathers are older than their children. Our job is to prove that Quincy is older than Pat.

Our proof is shown below. As usual, we start with our premises. The father of Pat is Quincy, and fathers are older than their children. Next, we use Universal Elimination to instantiate our quantified sentence. The father of Pat is older than Pat. Next we use Equality Elimination to replace father(pat) with quincy and thereby derive the conclusion that Quincy is older than Pat.

Finally, let's work through an example involving a disjunction of equations. We know that p(a) is true and p(b) is true, and we know that (a=c ∨ b=c) is true. Our job is to prove p(c).

The proof follows. As always we start with our premises. On line 4 , we start a new subproof with the assumption that a=c is true. From this assumption and our first premise, we conclude that p(c) must be true. Of course, we are not done yet, since we have proved the result only under this assumption that a=c. We make this clear with a use of Implication Introduction to derive the sentence (a=c ⇒ p(c)). Now, we start another subproof, this time with the assumption b=c. As before, we derive p(c); and, from this, we derive the implication (b=c ⇒ p(c)). Finally, we use Or Elimination to combine our two partial results with our disjunction of equations.

15.5 Example - Group Theory

A group is an algebraic structure consisting of an arbitrary set of elements and a binary function on these elements such that the binary function is associative, there is a left and right identity for the function, and there is a left and right inverse for any element in the set.

We can express the group axioms in Relational Logic as shown below. Here, * is the binary function, e is the identity for *, and inv gives the inverse of any element.

Given these axioms, let's use Fitch with equality to prove that the inverse of the inverse of the element is equal to the original element, i.e ∀x.inv(inv(x))=x. As usual, we start with our axioms.

Next we instantiate the left inverse rule, substituting inv(c) for x. We then use Equality Introduction to write down an equation saying that (inv(inv(c))*inv(c))*c is equal to itself. Then, we use our instantiated left inverse rule to substitute e for inv(inv(c)) on the right hand side of our equation. We instantiate our left identity rule, and then we use that to simplify the right hand side of our equation to c.

We now instantiate the associativity rule three times, replacing x by inv(inv(c)), y by inv(c)), and z by c. We then use Equality Elimination to re-associate the left hand side of the equation on line 10.

We instantiate the left inverse rule again. We apply this to our equation to simplify the left hand side. We instantiate our right identity rule and apply the result to the simplified equation to produce inv(inv(c))=c. Finally, we use Universal Introduction to produce the desired result.

Groups have many interesting properties. They are interesting in and of themselves. However, Group Theory is also an interesting domain for Logic, especially for theorem proving with equality.