## 1. IntroductionIn our discussion of Relational 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 - In Relational Logic, we can axiomatize the co-referentiality of terms in the form of equations. For example, to express the co-referentiality of Since equality is such a common relation, in what follows we write equations with the infix operator =, for example writing ( 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. ## 2. Properties of EqualityThe 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 First of all, the equality relation must be x.x=x
The relation must also be x.∀y.(x=y ⇒ y=x)
Finally, the relation must be x.∀y.∀z.(x=y ∧ y=z ⇒ x=z)
The three properties of reflexivity, symmetry, and transitivity are the defining conditions for what is know as an Let's see how we can use these properties to solve some problems of equality. Suppose we know that
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. ## 3. SubstitutionThe 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
The following sentence is a substitution axiom for the binary relation constant
The following is a substitution axiom for the unary function constant
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
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. ## 4. Fitch With EqualityAs 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 ( Our second rule of inference is called
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 τ 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
Finally, let's work through an example involving a disjunction of equations. We know that The proof follows. As always we start with our premises. On line 4 , we start a new subproof with the assumption that
## 5. Example - Group TheoryA 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,
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 ∀
Next we instantiate the left inverse rule, substituting
We now instantiate the associativity rule three times, replacing
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
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. ## RecapThe ## ExercisesExercise 1: Given Exercise 2: Given Exercise 3: Given Exercise 4: Given Exercise 5: Starting with the group axioms from Section 5, prove the left cancellation law for groups, i.e. prove ∀ |