Semantics

Here are three AXIOMS about =:

• Reflexivity: x = x
• Symmetry:
• Transitivity:

Here is the critical INFERENCE RULE for =:

• Substitution of Equals for Equals:
  a = b
  

The axioms should be familiar and obvious. The inference rule is simple, but extremely powerful. It says that if I know two entities (a and b) are equal then in the same expression (e), I can substitute one (say, a) for some variable x and get a new expression, e[a/x], and I can substitute the other (say, b) for the same variable x and get another new expression, e[b/x], and that the two new expressions are equal.

[Aside 1: Here is an example of how mathematical notation is much more concise than English!]

In other words, this rule allows us to substitute equals for equals in an expression without changing the value of that expression.

[Aside 2: It is because of this substitution rule that purely functional languages enjoy the property called referential transparency].