'Equals' has more than one meaning in math

Overloaded meanings of “=” in math and CS

• Commenters agree “=” is heavily overloaded: identity, congruence, definitional equality, equation holding for specific values, etc.
• Similar overloading exists in programming: assignment vs value equality vs reference equality vs ordering (=, ==, .equals, .compareTo == 0, etc.).
• Some see this overloading as inevitable and mostly benign; others see it as a constant source of bugs and confusion.

Java, BigDecimal, and “footguns”

• Long subthread on Java’s recommendation that compareTo(x) == 0 should match .equals(x) but doesn’t have to.
• One side: allowing inconsistency is a “bug in the spec” and guarantees subtle bugs (BigDecimal cited as a bad example).
• Other side: sometimes different orderings vs equalities are reasonable (e.g., distinguishing +0 and -0 for ordering but not for equality), so the spec keeps that flexibility.
• General worry: specs that permit inconsistent equality notions create traps for developers.

Set-theoretic constructions and chains ℕ ⊂ ℤ ⊂ ℚ ⊂ ℝ ⊂ ℂ

• Debate over whether it is “literally true” that naturals are subsets of integers, integers of rationals, etc.
• From a raw ZF-style construction, this is false: e.g., integers as equivalence classes of pairs of naturals are not literally elements of ℚ-as-constructed.
• Workaround: embed smaller structures via canonical injections and then silently identify their images with the originals.
• Some argue this silent identification is standard practice and fine; others insist it hides important subtleties and breaks down in formal systems.

Isomorphism, identity, and structural views

• Repeated emphasis that many “equalities” are really isomorphisms or canonical identifications.
• Structuralist stance: what matters is the pattern of relations (universal properties), not which concrete construction you choose; all valid constructions of ℕ, ℤ, ℚ, ℝ are “the same” up to isomorphism.
• Critics push back that you still must say what objects are and which questions (like 0 ∈ 3) even make sense.

Formal verification and type theory vs set theory

• Thread notes that theorem provers (Lean, etc.) force distinctions the article talks about: different 1’s, coercions instead of literal subset relations, Prop vs Bool, etc.
• Some view current systems as unwieldy and missing basic conveniences (like treating ℕ as a true subset of ℤ); types and coercions are called “cumbersome workarounds.”
• Others argue this pain is inherent: once you care about formal soundness, you must track which notion of equality you’re using and when coercions are applied.
• There is optimism that tools and automation will evolve so that mathematicians can work “post‑rigorously” while machines handle the low-level distinctions.

Pedagogy: = vs ≡, quantifiers, and stages of rigor

• Several comments wish schools emphasized early the difference between:
  • “Equals here for all x” (identity / universal quantification),
  • “Equals only at certain x” (solutions of equations),
  • And different symbols like =, ≡.
• Mention of a 3‑stage view of learning math: pre‑rigorous (intuitive), rigorous (formal, picky about constructions), post‑rigorous (comfortable omitting details while knowing they can be supplied).

Foundations, category theory, HoTT

• Some highlight category theory and homotopy type theory as frameworks that treat equivalence/isomorphism as more fundamental than strict equality.
• Others caution that these are sophisticated responses to long-known issues, not evidence that “old math is wrong”; they refine how we talk about sameness rather than overturn results.