Math Lingo vs. Plain English: Double Entendre (1997)

And if you get into machine proofs, you find the need to nail all those concepts down.

"'Equal' is used freely, from kindergarten to postgraduate. It's never defined or explained."

Which is a problem.

Uses of "equal" include:

- Constraint. "x = y" as "x and y are constrained to have the same value." This is a common algebraic usage.

- Definition: "f(x) = x + 1"

- Equivalence: "x * 2 = 2 * x"

- Assignment: "x = 1"

- Comparison: "x = 1"

You're supposed to decide from context which usage is meant.

MathCAD used to use different symbols for each of these. Not a bad idea. (MathCAD is still around, but PTC bought it and it's now $620 a year.)

I think you're onto something. When you formalize math you suddenly see how things summarized to one word or even implied implicitly can require pages of proof. But in this particular case, you're a little off. At least in conventional theorem proving (Coq, HOL, Agda) you mostly need 2 of those ("definition" and "equivalence") and for meta programmatic heuristic purposes (to help the solver) "constraint" too (except this has nothing to do with "proof proper").

Assignment isn't really needed for formal proofs since assignments usually requires a computational context that's not pure and most proofs are done tactics-like or functional style. I also can't see how "comparison" any different than "equivalence".

I would say the notion of "=" isn't the biggest difference here. I think what bugs people about "=" in automated proof systems is because (somehow?) our brain is really good at graph searching mathematical proofs and so typing equality proof in Coq, Agda, HOL is inherently too verbose.

Sorry to nitpick but this is an important topic as equality-reasoning is one of the harder parts of automated proof systems.