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

Math Lingo vs. Plain English: Double Entendre (1997)(cut-the-knot.org)

13 points by merraksh 7 years ago | 4 comments

Animats 7 years ago |

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.)

gnulinux 7 years ago | |

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.

lodi 7 years ago |

> In plain English, "Tea or coffee?" means one or the other, not both. It's called the "exclusive or."

And then the followup, "Milk or sugar?" is an inclusive or. English... amirite?

Another favourite of mine: pluralization rules. Duck->ducks, mouse->mice, moose->moose.

trombonechamp 7 years ago |

> Distance is a monotonic increasing function of time, so the inverse function exists.

Not to be pedantic, but I think they mean a "strictly increasing" function, as f(x)=1 for x∈ℝ does not have an inverse.