Subsection 7.6.5 Equality
But, getting back to the formal system that we’re setting up here: There is one restricted use of higher order reasoning that is so important that even most computational logic systems support it. We’ll allow it too.
The thing we can’t live without is equality. We want to be able to say (typically because we’ve managed to prove it) that two things are equal.
But what does it actually mean for two things to be equal? What we want it to mean is that the two things share all the same properties. Oops. That’s a second-order logic idea. What we want to be able to say is:
∀P (∀x, y (((x = y) ∧ P(x)) → P(y)))
What this says is that, for any property P, if there are two objects x and y and they are known to be equal, then if P is true of x it must also be true of y.
Let’s look at an example where equality is exactly what we need. Suppose that we are given the following premises:
[1] Roommates share an address. In other words, if x and y are roommates and if z is the address of one of them, then z is the address of the other.
[2] Kelly’s address is prestigious.
[3] Kelly and Chris are roommates.
We can write these formally as follows, assuming the existence of a function, addressOf, that returns the address of its argument:
[1] x, y (Roomates(x, y) (addressOf(x) = addressOf(y)))
[2] Prestigious(addressOf(Kelly))
[3] Roomates(Kelly, Chris)
We’d like to be able to show that Chris also lives at a prestigious address. Let’s assume that we have the premise that tells us that if two objects are equal then they share all properties. That’s (as stated above):
[4] P (x, y (((x = y) P(x)) P(y)))
Then we can reason as follows:
Since Kelly and Chris are roommates, addressOf(Kelly) = addressOf(Chris). (from [1])
Prestigious(addressOf(Kelly)) is a premise.
But addressOf(Chris) has all the same properties as addressOf(Kelly).
So we have Prestigious(addressOf(Chris)).
We need this interpretation of what equality actually means if we want to do arithmetic and algebra in the way we are used to doing them.
Suppose that we have:
[1] x = y
[2] x + b > 10
We should be able to reason that, since x and y are equal, we can substitute one for the other anywhere. So we should be able to derive:
[3] y + b > 10
A first-order system that branches out just enough to allow equality, in this meaningful sense, is called (of all things) a first-order system with equality.
Big Idea
Equality is such an important concept that almost all practical first-order systems are extended to support it.