18 ms·

'Equals' has more than one meaning in math

86 points by laktak 2y ago

Animats 2y ago
MathCAD once had about four equality symbols. Comparison, assignment, identity, and congruence, I think. Mathematica uses <=> for Boolean comparisons.
- gizmo686 2y ago
  Even general purpose programming languages have this. Java has at least 4 as well: * Assignment (=) * Referential equality (==) * Structural equality (.equals()) * Comparison equality (.compareTo(_) == 0 )
  - auggierose 2y ago
    .equals() and .compareTo(_) == 0 are required to be the same. If you program it differently, it is a bug.
    - gizmo686 2y ago
      From the javadoc: > It is strongly recommended, but not strictly required that (x.compareTo(y)==0) == (x.equals(y)). Generally speaking, any class that implements the Comparable interface and violates this condition should clearly indicate this fact. The recommended language is "Note: this class has a natural ordering that is inconsistent with equals."
      - auggierose 2y ago
        Nice catch. Now you also found buggy documentation / specification!
        xboxnolifes 2y ago
        Why is it buggy?
        auggierose 2y ago
        Why would you allow .equals and .compareTo to have inconsistent meanings? That is a guaranteed source of bugs. I cannot think of a single good reason to allow this. If you need a different order for some reason, that is what the Comparator interface is for.
        maxbond 2y ago
        If it's a bad idea but considered legal according to the documentation, then that would make it a footgun rather than a bug, no?
        auggierose 2y ago
        Yes, that makes this a footgun, and the specification containing this footgun buggy. It is a bug in the spec because there is no good reason for the footgun being there.
        maxbond 2y ago
        You have not yet imagined a reason, and neither have I. That doesn't mean one doesn't exist. Likely it would be something idiosyncratic involving legacy code that would only make sense in a real world context - "we have to change the way it sorts to fix ticket ABC123, but we can't change the equality, or we'll have a regression of ABC456."
        auggierose 2y ago
        Then provide a comparator to sort differently, no problem. There will never be a good reason for the spec to be like that. Just look how people here justify the mess of BigDecimal.
    - maple3142 2y ago
      Hmm, there was an article about Java's BigDecimal behaves differently for equals and compareTo: https://igorstechnoclub.com/java-bigdecimal/ https://igorstechnoclub.com/java-bigdecimal/
      - auggierose 2y ago
        That is a great example why I consider the spec buggy. With a proper spec, stuff like that would not fly from the start.
bravetraveler 2y ago
Much like words, or any created system, are inherently kind-of 'ambiguous-but-not'... by existing Words can be assertions or statements, these aren't necessarily the same thing The system was made to deal with the ambiguity, not remove it, so we're dancing around the actual fundamentals. I don't know what purpose this article serves other than to congratulate monkeys for their creation/entertainment
gus_massa 2y ago
In the first year of the University you write cpngruence with three horizontal lines. In the second, you just use two lines, aka an equal sign. Everyone knows = is overloaded. The same happens with other signs, like the arrow of limit. In many cases it's confusing so you add a small note to the arrow, unless it's obvious (whatever that means).
- SassyBird 2y ago
  > In the first year of the University you write cpngruence with three horizontal lines. In the second, you just use two lines, aka an equal sign. Obviously in the next step you achieve enlightenment when you then write them as just one horizontal line, but most don’t reach that stage.
  - programjames 2y ago
    Ah yes, the ~.
    - lupire 2y ago
      ~ is a — (em dash) that lacks the courage of its convictions.
dang 2y ago
Related. Others? Grothendieck’s use of equality - https://news.ycombinator.com/item?id=40414404 https://news.ycombinator.com/item?id=40414404 - May 2024 (129 comments) Grothendieck's Approach to Equality [pdf] - https://news.ycombinator.com/item?id=31557361 https://news.ycombinator.com/item?id=31557361 - May 2022 (37 comments)
woopwoop 2y ago
When I took Dan Freed's algebraic topology course, one time he asked us if two spaces were the same. Then he looked at us for a moment and said that actually that was a "Bill Clinton question: the answer depends on what the meaning of the word is is".
- 082349872349872 2y ago
  There's a (n improper) coarsest universe where anything is the same as everything else. (which reminds me of the buddhist monk at the hot dog stand: — Make me one with everything — Here ya go bud — Uhhh ... I gave you a twenty? — Change is an illusion ) EDIT: and Ireneo Funes (the Memorious) inhabits that other improper, finest, universe where nothing is the same as anything else. (OnlyNaNs?)
  - vinnyvichy 2y ago
    Btw, the following might come across as a little Borgean.. (Author of your Wikisourced cetacean) https://baike.baidu.com/item/%E4%BD%9A%E5%90%8D/37139#:~:text=%E4%BD%9A%E5%90%8D%E6%98%AF%E4%B8%80%E4%B8%AA%E6%B1%89%E8%AF%AD%E8%AF%8D%E8%AF%AD,%E6%84%BF%E9%80%8F%E6%BC%8F%E5%A7%93%E5%90%8D%E7%9A%84%E4%BA%BA%E3%80%82 https://baike.baidu.com/item/%E4%BD%9A%E5%90%8D/37139#:~:tex... (Not a Name) 与鬼神通 "Converse with gods and spectres" https://www.feirao.com/chengyu/32963S.html https://www.feirao.com/chengyu/32963S.html
    - vinnyvichy 2y ago
      My guess is that your cetacean originates from the Sui-Tang under a nihilizing influence of Buddhist rationalizations. "No creation without injury, no injury without creation." (My interpretation, cf the Japanese distillation) https://en.m.wiktionary.org/wiki/%E5%89%B5#Japanese https://en.m.wiktionary.org/wiki/%E5%89%B5#Japanese Compare with (note element of chance) https://en.m.wiktionary.org/wiki/incido https://en.m.wiktionary.org/wiki/incido More relevant to thread https://en.m.wiktionary.org/wiki/pare https://en.m.wiktionary.org/wiki/pare (Vs https://en.m.wiktionary.org/wiki/par#Latin https://en.m.wiktionary.org/wiki/par#Latin)
gizmo686 2y ago
Terence Tao wrote a blog post years ago dividing math education into 3 stages: pre-rigourus, rigourus, and post-rigorous. That distinction seems relevent here. Every mathamatician knows that the integer 1 and the real number 1 different objects [0]. We could make every invocation of a canonical isomorphism explicit, but that would make all of math far too unwieldy to do. This is the core problem with formal proof verification. Current provers need you to prove things at such a low level that they are simply unwieldy to use. That does not mean we need to reinvent all of math. It means we need to improve formal verification tooling. Maybe we also need to train mathamaticians in formal verification systems. In much the same way that they had to be trained to use computer algebra systems. We didn't reconstruct all of math. We just learned how to work within the limitations of tools when we use those tools. [0] Unless you go out of your way to construct them to be the same thing. There is not actually any official definition of, for example, what the integer 1 is. Since so many definitions of it are equivalent, that is a fundamentally pointless conversation to have. A few textbook authors need to make a decision for pedalogical purposes. No one else cares.
- auggierose 2y ago
  I think pretty much every mathematician agrees that you can assume ℕ ⊂ ℤ ⊂ ℚ ⊂ ℝ ⊂ ℂ, and that 1 the integer is the same as 1 the real number.
  - klodolph 2y ago
    You have to use a very funny notion of ⊂ for that to make sense. Mathematicians recognize that there is a lot of funny business going on behind the scenes… if you use the typical construction of these sets, then ℤ ⊂ ℚ is for sure false under the set-theoretic definition of what subsets are. So you are going to get a lot of funny explanations of why you can still say “ℤ ⊂ ℚ” and what that means. And what is “the same as” anyway?
    - hansvm 2y ago
      The typical construction is just to show that they _can_ be constructed. Once you have "primitive" integers, rationals, ..., you pick (for this finite example) the largest of them, and define the "integers" to be a subset with a certain property. That's also well-defined, and you find _exactly_ the same integers in the rationals and reals.
anon291 2y ago
Trouble arises in any logical system when we start to make statements on the system itself. As long as there's a strict separation between the target of your logic and the logic itself, you can make it all work out, but recursion is what kills you. To avoid this, many thinkers have come up with a sort of infinite tower of sorts. For example, in ZFC set theory, sets are ordered in cumulative ranks. In theorem proving languages like Coq, Agda, etc, there are a hierarchy of universes. Even Aristotle's four causes can be seen to be a small subset of the infinite hierarchy of cause. It's just the nature of logic. Similarly, there is a hierarchy of equality at increasing abstraction levels. There's naive equality which is that two things are literally the same. Then there's equality as to the 'class' of objects, and we can even go beyond that talking about equality of equalities (another word for analogies). Most stop there, but you can go on and on and on. I'm currently interested in homotopy type theory systematizes this notion of varying 'levels' of equality, but it too has issues. It's an open question. The article does sensationalize a bit because math is just a method of discourse. Equality means different things to different fields, and nothing about this kind of equality means that previous results are wrong.
- VirusNewbie 2y ago
  Unbounded recursion. Not recursion itself.
  - anon291 2y ago
    Good point.
- zmgsabst 2y ago
  Homotopy type theory isn’t magic, but it nicely explores the difference between (strict) equality and context dependent equivalence. (Okay, technically that’s univalence.) I think HoTT nicely capstones the idea algebra and geometry are equivalent by pointing out that semantics itself is defined by the topology of categorical diagrams — and anywhere we find compatible topology is equivalent. Neat.
phlakaton 2y ago
As one of the high school geometers of all time, I was always rather partial to ≅ which we used for congruence. I'm happy to share it with other mathematicians if they'll agree to keep their mitts off of ":=".
vishnugupta 2y ago
Related https://www.quantamagazine.org/with-category-theory-mathematics-escapes-from-equality-20191010/ https://www.quantamagazine.org/with-category-theory-mathemat...
cesaref 2y ago
Is there a decent overview of what the aim of mathematics solvers is these days? In light of Hilbert's effort at formalism in the 1920s, and the incompleteness theorem, I was wondering where this was going, and what the known limitations are.
- klodolph 2y ago
  The incompleteness theorem isn’t an argument against formalism, it’s just a bound on what you can do with it (you can’t use one set of axioms and expect to prove everything). That’s ok, because you are, 1. Not required to prove everything which is true, 2. Not limited to one set of axioms. The nice thing about formalism is that you can use a computer program to check whether a proof is sound or not. Isn’t that nice? It has applications in e.g. computer science and engineering, where you can prove that a program does not crash, or prove that a traffic light never shows green in conflicting directions, or prove that a real-time kernel always provides enough computational time for your rocket computer to steer. Working math, there are more and more complex proofs that cannot reasonably be checked by humans. Having a computer check them is a nice alternative.
- ysofunny 2y ago
  it's pretty much a competition between niche programming languages which are interesting to different powerful academics
- singularity2001 2y ago
  Current hopes (even by Terrence Tao) are that you give a sketch of a proof to GPT-X and it will give you a link to the formally confirmed proof. Others hope that the next AI will come up with a sketch of a proof itself. GPT-4 sucks at lean because lean had it's syntax changed too often, and GPT-4 shows limited reasoning capabilities However it did come up with the following proof for my little order of pairs instance LT : LT (ℕ × ℕ) where lt f g := f.1 < g.1 ∨ (f.1 = g.1 ∧ f.2 < g.2) instance : DecidableRel (LT.lt : ℕ × ℕ → ℕ × ℕ → Prop) := fun (a,b) (c,d) => if h₁ : a < c then isTrue (Or.inl h₁) else if h₂ : a = c then if h₃ : b < d then isTrue (Or.inr ⟨h₂, h₃⟩) -- the rest is even more silly since we have to turn everything around else isFalse (λ (h : a < c ∨ (a = c ∧ b < d)) => Or.elim h (λ hlt : a < c => absurd hlt h₁) (λ heq : a = c ∧ b < d => absurd (And.right heq) h₃)) else isFalse (λ (h : a < c ∨ (a = c ∧ b < d)) => Or.elim h (λ hlt : a < c => absurd hlt h₁) (λ heq : a = c ∧ b < d => absurd (And.left heq) h₂) ) This may lead back to the original question because Bool ≠ Prop and the formula for LT should ideally lead directly to decidability without all this redundancy?
ganzuul 2y ago
https://en.wikipedia.org/wiki/The_Treachery_of_Images https://en.wikipedia.org/wiki/The_Treachery_of_Images Leads to https://en.wikipedia.org/wiki/Ontology https://en.wikipedia.org/wiki/Ontology Which compares everything to a self which we won't agree on, so it is expedient if we just pin it down https://en.wikibooks.org/wiki/X86_Assembly/Control_Flow#Comparison_Instructions https://en.wikibooks.org/wiki/X86_Assembly/Control_Flow#Comp... This presumes a sequential model of computation but we are actually free to discover functional and concurrent models as they are equivalent, but give philosophical freedom and yet retain rigor.
crsn 2y ago
I’ve been working on a glossary of “Notions of Equality & Sameness” every few months for the last ~8 years (and looking for collaborators: carson@carsonkahn.com) - surprised not to have had this one in my list already!
voidUpdate 2y ago
I know it's not related to the content of the article but I hate when websites redirect me to a page of articles when I click the back button, if that isn't where I came from. I've already decided I want to go back to what I was looking at before, shoving a load of stuff that I didn't want into my face isn't going to make me change my mind
lordnacho 2y ago
I don't think you need to go to higher level math to run into this sort of problem. When we're in school solving equations, getting to the initial stages of calculus, you start running into identities like sin^2(x) + cos^2(x) = 1, which sometimes but not often are written with three parallel lines instead of two. What this means is that the functions on either side of the sign are equivalent, any x you pick doesn't change the graph. At some point, you will be solving simultaneous equations, and someone will have the bright idea that you can just differentiate both sides and just solve that. This happens to be true if you have something like above, it's still valid that the derivative anywhere is the same, since they are the same function. But if you are actually just finding the crossing point of two graphs, like one normally does at that level, then the equality is only for a particular value of x, and there's no reason the derivative would be the same. In general there's a lot of these little notation things that creep up around that stage. The big one is treating dy/dx like a fraction, which you can do in certain cases to solve differential equations, but only in certain cases. If you don't understand why, you might get very confused about what the symbols actually mean.
hilbert42 2y ago
Leaving aside the more advanced definitions of equals, it'd be good if more emphasis were put on the difference between '=' and '≡' early on in one's training. That is explaining why is equivalent different to equals. I recall the difference in the definitions being confusing for most of us kids.
- housecarpenter 2y ago
  The way I see it, the distinction between = and ≡ isn't really to do with equality having more than one meaning. An "identity" like sin^2 x + cos^2 x ≡ 1 is really just shorthand for "for every real number x, we have sin^2 x + cos^2 x = 1". The equals sign here has the same meaning as in a statement such as "there is a real number x such that sin^2 x + cos^2 x = 1"; the difference is in the surrounding language, and what meaning it assigns to the variable x. So perhaps rather than just emphasizing the difference between = and ≡ more, it would be better to go further and emphasize the difference between universal and existential quantification more. Quantifiers can be confusing, but I think people also find having two different equals signs confusing; and it wouldn't be necessary to give a full account of predicate logic to high schoolers, I'm thinking more of just informally describing the difference between "for all" and "there exists" and reminding them that a bare variable has no meaning if you don't know what set it ranges over and how it's quantified. This is just my speculation, I have no experience with mathematical education whatsoever.
  - hilbert42 2y ago
    "...emphasize the difference between universal and existential quantification more. Quantifiers can be confusing..." Right, I've uni math also formal logic so I've knowledge of universal and existential quantification, etc. thus an understanding of the issues. You're right, that stuff's a bit too heavy for highschoolers. Perhaps all that's needed is to be told 'that at times these appear the same but later on you'll need to understand there's a mathematical distinction' then emphasize the difference aspect to drive the point home. Even though it was a long time ago I mostly recall what the teacher said and whilst he gave a few examples he never emphasized that there was a mathematical difference and that it was an important fact to know. Matters became more ambiguous from our science courses, the use of 'equivalent' was very loose. I reckon the same or similar should apply to other topics, calculus for example.
sproutini 2y ago
This isn't news to any logician or people working in formal methods. More like a mathematician getting his head around what has been thought about for decades, if not centuries. Also, -1 for not mentioning Leibniz equality.
vinnyvichy 2y ago
tl;dr as an acolyte is that sometimes the bug can be fixed by adding extra data (e.g. number of minus signs, or method to compute minus signs) to your declaration of equality. Concrete example from Kev Buzzard's "Lean proof of Fermat's Last Theorem" from yesterday (2024-06-19 UT) p34: "It is impossible to say which of the two canonical isomorphisms is “the most canonical”; people working in different areas make different choices in order to locally minimise the number of minus signs in their results." https://imperialcollegelondon.github.io/FLT/blueprint.pdf https://imperialcollegelondon.github.io/FLT/blueprint.pdf A lot of the subtleties seem to come from the pecularities of what is meant by "canonical" rather than by "isomorphic"

86 points by laktak 2y ago

MathCAD once had about four equality symbols. Comparison, assignment, identity, and congruence, I think. Mathematica uses <=> for Boolean comparisons.

gizmo686 2y ago
Even general purpose programming languages have this. Java has at least 4 as well: * Assignment (=) * Referential equality (==) * Structural equality (.equals()) * Comparison equality (.compareTo(_) == 0 )
- auggierose 2y ago
  .equals() and .compareTo(_) == 0 are required to be the same. If you program it differently, it is a bug.
  - gizmo686 2y ago
    From the javadoc: > It is strongly recommended, but not strictly required that (x.compareTo(y)==0) == (x.equals(y)). Generally speaking, any class that implements the Comparable interface and violates this condition should clearly indicate this fact. The recommended language is "Note: this class has a natural ordering that is inconsistent with equals."
    - auggierose 2y ago
      Nice catch. Now you also found buggy documentation / specification!
      - xboxnolifes 2y ago
        Why is it buggy?
        auggierose 2y ago
        Why would you allow .equals and .compareTo to have inconsistent meanings? That is a guaranteed source of bugs. I cannot think of a single good reason to allow this. If you need a different order for some reason, that is what the Comparator interface is for.
        maxbond 2y ago
        If it's a bad idea but considered legal according to the documentation, then that would make it a footgun rather than a bug, no?
        auggierose 2y ago
        Yes, that makes this a footgun, and the specification containing this footgun buggy. It is a bug in the spec because there is no good reason for the footgun being there.
        maxbond 2y ago
        You have not yet imagined a reason, and neither have I. That doesn't mean one doesn't exist. Likely it would be something idiosyncratic involving legacy code that would only make sense in a real world context - "we have to change the way it sorts to fix ticket ABC123, but we can't change the equality, or we'll have a regression of ABC456."
        auggierose 2y ago
        Then provide a comparator to sort differently, no problem. There will never be a good reason for the spec to be like that. Just look how people here justify the mess of BigDecimal.
  - maple3142 2y ago
    Hmm, there was an article about Java's BigDecimal behaves differently for equals and compareTo: https://igorstechnoclub.com/java-bigdecimal/ https://igorstechnoclub.com/java-bigdecimal/
    - auggierose 2y ago
      That is a great example why I consider the spec buggy. With a proper spec, stuff like that would not fly from the start.

bravetraveler 2y ago

Much like words, or any created system, are inherently kind-of 'ambiguous-but-not'... by existing Words can be assertions or statements, these aren't necessarily the same thing The system was made to deal with the ambiguity, not remove it, so we're dancing around the actual fundamentals. I don't know what purpose this article serves other than to congratulate monkeys for their creation/entertainment

gus_massa 2y ago

In the first year of the University you write cpngruence with three horizontal lines. In the second, you just use two lines, aka an equal sign. Everyone knows = is overloaded. The same happens with other signs, like the arrow of limit. In many cases it's confusing so you add a small note to the arrow, unless it's obvious (whatever that means).

SassyBird 2y ago
> In the first year of the University you write cpngruence with three horizontal lines. In the second, you just use two lines, aka an equal sign. Obviously in the next step you achieve enlightenment when you then write them as just one horizontal line, but most don’t reach that stage.
- programjames 2y ago
  Ah yes, the ~.
  - lupire 2y ago
    ~ is a — (em dash) that lacks the courage of its convictions.

dang 2y ago

Related. Others? Grothendieck’s use of equality - https://news.ycombinator.com/item?id=40414404 https://news.ycombinator.com/item?id=40414404 - May 2024 (129 comments) Grothendieck's Approach to Equality [pdf] - https://news.ycombinator.com/item?id=31557361 https://news.ycombinator.com/item?id=31557361 - May 2022 (37 comments)

woopwoop 2y ago

When I took Dan Freed's algebraic topology course, one time he asked us if two spaces were the same. Then he looked at us for a moment and said that actually that was a "Bill Clinton question: the answer depends on what the meaning of the word is is".

082349872349872 2y ago
There's a (n improper) coarsest universe where anything is the same as everything else. (which reminds me of the buddhist monk at the hot dog stand: — Make me one with everything — Here ya go bud — Uhhh ... I gave you a twenty? — Change is an illusion ) EDIT: and Ireneo Funes (the Memorious) inhabits that other improper, finest, universe where nothing is the same as anything else. (OnlyNaNs?)
- vinnyvichy 2y ago
  Btw, the following might come across as a little Borgean.. (Author of your Wikisourced cetacean) https://baike.baidu.com/item/%E4%BD%9A%E5%90%8D/37139#:~:text=%E4%BD%9A%E5%90%8D%E6%98%AF%E4%B8%80%E4%B8%AA%E6%B1%89%E8%AF%AD%E8%AF%8D%E8%AF%AD,%E6%84%BF%E9%80%8F%E6%BC%8F%E5%A7%93%E5%90%8D%E7%9A%84%E4%BA%BA%E3%80%82 https://baike.baidu.com/item/%E4%BD%9A%E5%90%8D/37139#:~:tex... (Not a Name) 与鬼神通 "Converse with gods and spectres" https://www.feirao.com/chengyu/32963S.html https://www.feirao.com/chengyu/32963S.html
  - vinnyvichy 2y ago
    My guess is that your cetacean originates from the Sui-Tang under a nihilizing influence of Buddhist rationalizations. "No creation without injury, no injury without creation." (My interpretation, cf the Japanese distillation) https://en.m.wiktionary.org/wiki/%E5%89%B5#Japanese https://en.m.wiktionary.org/wiki/%E5%89%B5#Japanese Compare with (note element of chance) https://en.m.wiktionary.org/wiki/incido https://en.m.wiktionary.org/wiki/incido More relevant to thread https://en.m.wiktionary.org/wiki/pare https://en.m.wiktionary.org/wiki/pare (Vs https://en.m.wiktionary.org/wiki/par#Latin https://en.m.wiktionary.org/wiki/par#Latin)

gizmo686 2y ago

Terence Tao wrote a blog post years ago dividing math education into 3 stages: pre-rigourus, rigourus, and post-rigorous. That distinction seems relevent here. Every mathamatician knows that the integer 1 and the real number 1 different objects [0]. We could make every invocation of a canonical isomorphism explicit, but that would make all of math far too unwieldy to do. This is the core problem with formal proof verification. Current provers need you to prove things at such a low level that they are simply unwieldy to use. That does not mean we need to reinvent all of math. It means we need to improve formal verification tooling. Maybe we also need to train mathamaticians in formal verification systems. In much the same way that they had to be trained to use computer algebra systems. We didn't reconstruct all of math. We just learned how to work within the limitations of tools when we use those tools. [0] Unless you go out of your way to construct them to be the same thing. There is not actually any official definition of, for example, what the integer 1 is. Since so many definitions of it are equivalent, that is a fundamentally pointless conversation to have. A few textbook authors need to make a decision for pedalogical purposes. No one else cares.

auggierose 2y ago
I think pretty much every mathematician agrees that you can assume ℕ ⊂ ℤ ⊂ ℚ ⊂ ℝ ⊂ ℂ, and that 1 the integer is the same as 1 the real number.
- klodolph 2y ago
  You have to use a very funny notion of ⊂ for that to make sense. Mathematicians recognize that there is a lot of funny business going on behind the scenes… if you use the typical construction of these sets, then ℤ ⊂ ℚ is for sure false under the set-theoretic definition of what subsets are. So you are going to get a lot of funny explanations of why you can still say “ℤ ⊂ ℚ” and what that means. And what is “the same as” anyway?
  - hansvm 2y ago
    The typical construction is just to show that they _can_ be constructed. Once you have "primitive" integers, rationals, ..., you pick (for this finite example) the largest of them, and define the "integers" to be a subset with a certain property. That's also well-defined, and you find _exactly_ the same integers in the rationals and reals.

anon291 2y ago

Trouble arises in any logical system when we start to make statements on the system itself. As long as there's a strict separation between the target of your logic and the logic itself, you can make it all work out, but recursion is what kills you. To avoid this, many thinkers have come up with a sort of infinite tower of sorts. For example, in ZFC set theory, sets are ordered in cumulative ranks. In theorem proving languages like Coq, Agda, etc, there are a hierarchy of universes. Even Aristotle's four causes can be seen to be a small subset of the infinite hierarchy of cause. It's just the nature of logic. Similarly, there is a hierarchy of equality at increasing abstraction levels. There's naive equality which is that two things are literally the same. Then there's equality as to the 'class' of objects, and we can even go beyond that talking about equality of equalities (another word for analogies). Most stop there, but you can go on and on and on. I'm currently interested in homotopy type theory systematizes this notion of varying 'levels' of equality, but it too has issues. It's an open question. The article does sensationalize a bit because math is just a method of discourse. Equality means different things to different fields, and nothing about this kind of equality means that previous results are wrong.

VirusNewbie 2y ago
Unbounded recursion. Not recursion itself.
- anon291 2y ago
  Good point.
zmgsabst 2y ago
Homotopy type theory isn’t magic, but it nicely explores the difference between (strict) equality and context dependent equivalence. (Okay, technically that’s univalence.) I think HoTT nicely capstones the idea algebra and geometry are equivalent by pointing out that semantics itself is defined by the topology of categorical diagrams — and anywhere we find compatible topology is equivalent. Neat.

phlakaton 2y ago

As one of the high school geometers of all time, I was always rather partial to ≅ which we used for congruence. I'm happy to share it with other mathematicians if they'll agree to keep their mitts off of ":=".

vishnugupta 2y ago

Related https://www.quantamagazine.org/with-category-theory-mathematics-escapes-from-equality-20191010/ https://www.quantamagazine.org/with-category-theory-mathemat...

cesaref 2y ago

Is there a decent overview of what the aim of mathematics solvers is these days? In light of Hilbert's effort at formalism in the 1920s, and the incompleteness theorem, I was wondering where this was going, and what the known limitations are.

klodolph 2y ago
The incompleteness theorem isn’t an argument against formalism, it’s just a bound on what you can do with it (you can’t use one set of axioms and expect to prove everything). That’s ok, because you are, 1. Not required to prove everything which is true, 2. Not limited to one set of axioms. The nice thing about formalism is that you can use a computer program to check whether a proof is sound or not. Isn’t that nice? It has applications in e.g. computer science and engineering, where you can prove that a program does not crash, or prove that a traffic light never shows green in conflicting directions, or prove that a real-time kernel always provides enough computational time for your rocket computer to steer. Working math, there are more and more complex proofs that cannot reasonably be checked by humans. Having a computer check them is a nice alternative.
ysofunny 2y ago
it's pretty much a competition between niche programming languages which are interesting to different powerful academics
singularity2001 2y ago
Current hopes (even by Terrence Tao) are that you give a sketch of a proof to GPT-X and it will give you a link to the formally confirmed proof. Others hope that the next AI will come up with a sketch of a proof itself. GPT-4 sucks at lean because lean had it's syntax changed too often, and GPT-4 shows limited reasoning capabilities However it did come up with the following proof for my little order of pairs instance LT : LT (ℕ × ℕ) where lt f g := f.1 < g.1 ∨ (f.1 = g.1 ∧ f.2 < g.2) instance : DecidableRel (LT.lt : ℕ × ℕ → ℕ × ℕ → Prop) := fun (a,b) (c,d) => if h₁ : a < c then isTrue (Or.inl h₁) else if h₂ : a = c then if h₃ : b < d then isTrue (Or.inr ⟨h₂, h₃⟩) -- the rest is even more silly since we have to turn everything around else isFalse (λ (h : a < c ∨ (a = c ∧ b < d)) => Or.elim h (λ hlt : a < c => absurd hlt h₁) (λ heq : a = c ∧ b < d => absurd (And.right heq) h₃)) else isFalse (λ (h : a < c ∨ (a = c ∧ b < d)) => Or.elim h (λ hlt : a < c => absurd hlt h₁) (λ heq : a = c ∧ b < d => absurd (And.left heq) h₂) ) This may lead back to the original question because Bool ≠ Prop and the formula for LT should ideally lead directly to decidability without all this redundancy?

ganzuul 2y ago

https://en.wikipedia.org/wiki/The_Treachery_of_Images https://en.wikipedia.org/wiki/The_Treachery_of_Images Leads to https://en.wikipedia.org/wiki/Ontology https://en.wikipedia.org/wiki/Ontology Which compares everything to a self which we won't agree on, so it is expedient if we just pin it down https://en.wikibooks.org/wiki/X86_Assembly/Control_Flow#Comparison_Instructions https://en.wikibooks.org/wiki/X86_Assembly/Control_Flow#Comp... This presumes a sequential model of computation but we are actually free to discover functional and concurrent models as they are equivalent, but give philosophical freedom and yet retain rigor.

crsn 2y ago

I’ve been working on a glossary of “Notions of Equality & Sameness” every few months for the last ~8 years (and looking for collaborators: carson@carsonkahn.com) - surprised not to have had this one in my list already!

voidUpdate 2y ago

I know it's not related to the content of the article but I hate when websites redirect me to a page of articles when I click the back button, if that isn't where I came from. I've already decided I want to go back to what I was looking at before, shoving a load of stuff that I didn't want into my face isn't going to make me change my mind

lordnacho 2y ago

I don't think you need to go to higher level math to run into this sort of problem. When we're in school solving equations, getting to the initial stages of calculus, you start running into identities like sin^2(x) + cos^2(x) = 1, which sometimes but not often are written with three parallel lines instead of two. What this means is that the functions on either side of the sign are equivalent, any x you pick doesn't change the graph. At some point, you will be solving simultaneous equations, and someone will have the bright idea that you can just differentiate both sides and just solve that. This happens to be true if you have something like above, it's still valid that the derivative anywhere is the same, since they are the same function. But if you are actually just finding the crossing point of two graphs, like one normally does at that level, then the equality is only for a particular value of x, and there's no reason the derivative would be the same. In general there's a lot of these little notation things that creep up around that stage. The big one is treating dy/dx like a fraction, which you can do in certain cases to solve differential equations, but only in certain cases. If you don't understand why, you might get very confused about what the symbols actually mean.

hilbert42 2y ago

Leaving aside the more advanced definitions of equals, it'd be good if more emphasis were put on the difference between '=' and '≡' early on in one's training. That is explaining why is equivalent different to equals. I recall the difference in the definitions being confusing for most of us kids.

housecarpenter 2y ago
The way I see it, the distinction between = and ≡ isn't really to do with equality having more than one meaning. An "identity" like sin^2 x + cos^2 x ≡ 1 is really just shorthand for "for every real number x, we have sin^2 x + cos^2 x = 1". The equals sign here has the same meaning as in a statement such as "there is a real number x such that sin^2 x + cos^2 x = 1"; the difference is in the surrounding language, and what meaning it assigns to the variable x. So perhaps rather than just emphasizing the difference between = and ≡ more, it would be better to go further and emphasize the difference between universal and existential quantification more. Quantifiers can be confusing, but I think people also find having two different equals signs confusing; and it wouldn't be necessary to give a full account of predicate logic to high schoolers, I'm thinking more of just informally describing the difference between "for all" and "there exists" and reminding them that a bare variable has no meaning if you don't know what set it ranges over and how it's quantified. This is just my speculation, I have no experience with mathematical education whatsoever.
- hilbert42 2y ago
  "...emphasize the difference between universal and existential quantification more. Quantifiers can be confusing..." Right, I've uni math also formal logic so I've knowledge of universal and existential quantification, etc. thus an understanding of the issues. You're right, that stuff's a bit too heavy for highschoolers. Perhaps all that's needed is to be told 'that at times these appear the same but later on you'll need to understand there's a mathematical distinction' then emphasize the difference aspect to drive the point home. Even though it was a long time ago I mostly recall what the teacher said and whilst he gave a few examples he never emphasized that there was a mathematical difference and that it was an important fact to know. Matters became more ambiguous from our science courses, the use of 'equivalent' was very loose. I reckon the same or similar should apply to other topics, calculus for example.

sproutini 2y ago

This isn't news to any logician or people working in formal methods. More like a mathematician getting his head around what has been thought about for decades, if not centuries. Also, -1 for not mentioning Leibniz equality.

vinnyvichy 2y ago

tl;dr as an acolyte is that sometimes the bug can be fixed by adding extra data (e.g. number of minus signs, or method to compute minus signs) to your declaration of equality. Concrete example from Kev Buzzard's "Lean proof of Fermat's Last Theorem" from yesterday (2024-06-19 UT) p34: "It is impossible to say which of the two canonical isomorphisms is “the most canonical”; people working in different areas make different choices in order to locally minimise the number of minus signs in their results." https://imperialcollegelondon.github.io/FLT/blueprint.pdf https://imperialcollegelondon.github.io/FLT/blueprint.pdf A lot of the subtleties seem to come from the pecularities of what is meant by "canonical" rather than by "isomorphic"