Equality

Equality (s = t) is a fundamental relationship between entities. When we state an equality s = t, we are saying that there is no way to tell the two individuals s and t apart from the point of view of the logical setting we are working in.

Syntax and Proof Rules for Equality

In the syntax, equality is a binary predicate symbol that is usually written infix: t1 = t2.

Equivalence Relations

For doing proofs about equality, we could think about just adding some axioms that describe it. It is possible to define what it means to be an equivalence relation (i.e., a relation that acts like equality) by the following three properties. Here we do this for some binary relation ≈ to emphasise that these laws are not enough to define proper equality.

1. Reflexivity: everything is equal to itself; t ≈ t, for all terms t.

2. Symmetry: if s ≈ t then t ≈ s, for all terms s and t.

3. Transitivity: if s ≈ t and t ≈ u, then s ≈ u.

These can be written as formulas to give three axioms of an equivalence relation:

1. reflexivity: ∀ x. x ≈ x

2. symmetry: ∀ x. ∀ y. x ≈ y → y ≈ x

3. transitivity: ∀ x. ∀ y. ∀ z. x ≈ y → y ≈ z → x ≈ z

There's not much one can prove directly from these axioms without making further assumptions. One thing that can be proved is that, even without reflexivity, if x is equal to something, then it must be equal to itself:

(A binary relation that only has symmetry and transitivity is called a partial equivalence relation. They are useful for describing the semantics of programming languages.)

Equality

These three axioms are the minimum for a relation ≈ to be considered some form of equivalence. However, they are not enough to properly define equality because they do not specify the effect that two things being equal has on everything else in the system.

Specifically, equality has the following special property, usually attributed to the philosopher Leibniz:

If t1 = t2 then everything that is true about t1 is true about t2.

Or, in more symbols:

If t1 = t2 and P[x ↦ t1] then P[x ↦ t2].

This property is known as “substitutivity” or, more philosophically, as “indiscernability of equivalents”. It can be read in two ways:

1. If two things are equal, there is no way to write a formula that is true about one and false about the other.

2. If two things are equal, then we can replace one with the other wherever we want with no effect on what is true; i.e., we can substitute one for the other.

Because it applies for all formulas P We can't express this property as an axiom in our system, so we add it as a new rule.

This rule, when combined with reflexivity, is enough to prove the other two properties symmetry and transitivity for equality.

Equality and its proof rules are explained in more depth in this video:

Slides for the video (PDF)

What things are equal?

One consequence of treating equal things as always substitable for one another is that what we consider to be equality depends on exactly what and how we are modelling. What is considered equal for one application domain might not make sense for another.

Sentences involving quotation in Natural Language are a rich source of tricky examples. For example the sentence “‘Edinburgh’ has 9 letters” might be considered true, but if we were to also consider “Edinburgh” to be equal to “The capital of Scotland”, then we would be able to derive the obviously false fact that “‘The capital of Scotland’ has 9 letters”.

The fundamental problem here is that the statement “‘X’ has N letters” states facts about individuals that are not preserved by our notion of equality. The relation “‘X’ has N letters” makes distinctions between individuals (in this case, it looks at their descriptive names) which are not preserved if we consider “Edinburgh” as just a different name for the capital of Scotland. To fix this example, we need to make sure that our predicates and our equalities are consistent, either by not admitting that “Edinburgh” and “The capital of Scotland” are equal, or by not allowing statements of the form “‘X’ has N letters” in our vocabulary.

This kind of example crops up in Computer Science whenever we have to make a distinction between the description of a process (i.e., the program that implements it) and the observable behaviour of a process. In some cases equality should track the implementation (e.g., a text editor application should treat different program texts differently), and in others it should track the behaviour (e.g., an optimising compiler is allowed to change the implementation if it preserves the behaviour). In philosophical jargon, these two aspects are referred to the intension (how a thing is built) and extension (how a thing acts) of an object.

Using Equality in the Proof Editor

The following video demonstrates the use of the proof rules for equality in the proof editor. Watch the video before attempting the exercises below. Warning: the question about addition has been moved to the next page on Arithmetic and Induction.

Exercises

{ goal: <some formula> }

{ focus: <formula1>; goal: <formula2> }

Exercise 1 : Symmetry

Exercise 2 : Transitivity

Exercise 3 : Abelian Groups

An abelian group is a generalisation of the ideas of addition and multiplication of numbers. We assume there is an operation ‘combine’ that combines two things (e.g., adding or multiplying), an operation ‘inv’ that takes the inverse of a thing (e.g., negation or reciprocal), and a value ‘emp()’ that has no effect when combined with something else (e.g., zero for addition, or one for multiplication). What makes an abelian group abelian and not just a group is that it does not matter what order things are combined in: ‘combine(x,y) = combine(y,x)’.

The axioms of an abelian group are:

1. combine-assoc : ∀x. ∀y. ∀z. combine(x, combine(y, z)) = combine(combine(x, y), z)

   This axiom states that if you have three things to combine together, then it does matter which order you do the ‘combine’ operations in, the answers are always the same. Axioms like this are usually called associativity, or assoc for short.

2. combine-comm : ∀x. ∀y. combine(x, y) = combine(y, x)

   This axiom states that combining ‘x’ with ‘y’ is the same as combining ‘y’ with ‘x’, just as it is for normal addition and multiplication. Axioms like this are usually called commutativity, or comm for short.

3. combine-inv : ∀x. combine(x, inv(x)) = emp()

   This axiom states that combining something with its inverse is equal to the empty thing. E.g., x + (-x) = 0 for addition on numbers.

4. combine-emp : ∀x. combine(x, emp()) = x

   This axiom states that combining ‘x’ with ‘emp()’ is the same as ‘x’. We can think of ‘emp()’ as being like ‘0’ for addition, or ‘1’ for multiplication.

Exercise 3.1

‘emp()’s in the middle of a combination can always be removed:

Exercise 3.2

The ‘combine-emp’ axiom works the other way round as well:

Exercise 3.3

The ‘combine-inv’ axiom works the other way round as well:

Exercise 4

This example demonstrates what can go wrong if we have a mismatch between the properties we assume of things, and what things are equal. Two things can be equal only if we do not talk about any properties that may separate them. Here is the example with letter counts from above:

More generally, if we have two things that have different properties (one is P and one is not P), then they must be not equal: