I was thinking about this last night. A friend once told me that he sucked at math through most of high school until the very end when he realized that the equal sign meant that the two things are either side were equal to each other. After realizing this he finished in the top ten (or maybe first) in Canada in the SIN contest.
I can see why he was mislead. Throughout grade school the equal sign is used as a place holder between successive steps in computation. Worse yet, people have a habit of stringing together equal signs as in
This totally obscures the fact that equality is a binary relation. Suddenly when kids start doing algebra, the use of equality changes. No wonder they are so confused. They try to learn various used of this strange symbol. Rules like you can add one number to both sides, or you can move a term from one side to the other if you change its sign. But there are so many rules to remember.
I propose that we avoid using the equal sign in cases that we are doing computation, instead use the reduction symbol which more accurately reflects what we are trying to express. So the above would be written as
If you feeling like being a little less formal, omit the subscript and maybe the superscript.
Some occasions we are just changing form, rather than doing computation. In this case we can use the symmetric-transitive closure of the reduction operation.
Once again type theory outdoes set theory. Set theory doesn’t even have a fundamental notion of computation, and this arrow notation makes no sense. But type theory, being a more accurate reflection of how people actually do math, has just the operation we need.
Once students get to algebra, they can learn the deduction (e1 ↔β e2) ⇒ (e1 = e2), and the other rules of equality. One can emphasise that equality means that the two terms evaluate to the same object in all cases.