10 ms·

With Category Theory, Mathematics Escapes from Equality (2019)

123 points by sebg 5y ago

smitty1e 5y ago
Maybe Jacob Lurie and Stephen Wolfram can collaborate on doing Higher Categories in finite automata for the win.
dataflow 5y ago
Except equality never meant "exactly the same" to begin with, though, right? Like we write 1 / (1 - x) = 1 + x + x^2 + ..., but one of them diverges for x = 2 and the other doesn't, so they're not "exactly the same", just equivalent in some sense. Or heck, even x / x = 1 doesn't mean the two are exactly the same. I'm not sure how far you could take math if you treat equality as meaning "exactly the same"; it seems even middle-school math requires understanding that that's not the case. Edit: In case it wasn't clear, I'm hoping someone can explain how this notion of equivalence differs from what we've traditionally called equality since middle school, given that the latter doesn't appear to mean exactly the same either.
- alecst 5y ago
  In both of your examples equality holds for x in some specified domain. The first equation is not valid (outside of, say, analytical continuation) for x >= 1. I thought the article was cool. From this comment, you are coming across as someone who is trivializing a potentially important piece of work. I didn’t really understand it, but I take mathematicians at IAS seriously.
  - dataflow 5y ago
    Why the ad hominem? I have nothing against the mathematicians or their work. I don't even know the math; that's why I'm reading the article. And I'm just trying to wrap my head around the article's explanation and trying to figure out why its premise seems inconsistent with my understanding. The problem is more likely somewhere in my understanding, so I posted it here in case somebody could clarify whether/what I'm misunderstanding of the difference between what we've called "equality" and what they're calling "equivalent", given neither of them seems to necessarily mean "exactly the same".
    - Quekid5 5y ago
      Well, as a disinterested observer, I think it was the > Except equality never meant... ... opening to your comment which immediately makes you look like you're being antagonistic. ("except", and "never" probably being the key words. Especially opening with "except"...)
  - yesenadam 5y ago
    > you are coming across as someone who is trivializing a potentially important piece of work. I didn't get that impression at all. Rather, you came across as needlessly insulting. Why add that sentence, even if you thought so?! "Be kind."
    - alecst 5y ago
      Hey so I was replying to this part: > I'm not sure how far you could take math if you treat equality as meaning "exactly the same"; it seems even middle-school math requires understanding that that's not the case. I honestly didn't mean that in a rude way, more like a "hey dude, be careful how you're coming across here, as there may be things you don't understand." I read the above phrase as describing a mathematician's work as something a middle schooler should already know. But I take back what I said. I'm all good, everyone's good, I think there was just a misunderstanding here. In the same vein, I don't see how you could read my message as needlessly insulting, as I thought it was pretty softly worded. But I guess that's the nature of written communication. I think you should have given me the benefit of the doubt, just as I should have done for the original poster.
      - yesenadam 5y ago
        No, it wasn't softly worded. Now you take back what you said, although it was fine and I'm the one in the wrong to think it was insulting?! Etc. I don't think those are reasonable interpretations. Your comment was good without the last paragraph. Can't help sinking the boot in, eh? That's not a very nice habit. But anyway, I have things to do today! See ya.
  - Sheneneh 5y ago
    > you are coming across as someone who is trivializing a potentially important piece of work. I doubt it. The parent is confused and hence the question obviously. But I get the impression that the parent would benefit from reading an elementary textbook on discrete math as the post is gibberish (as are a few other posts in this thread). I know it sounds rude, but I don't know how else to put it. It's not only the fact that the parent doesn't have a conceptual idea about equivalence relations and in particular equality, isomorphism, let alone homotopy, but is also very confused about what it means for a series to converge which is also very elementary. Before discussing the merits of Dostoevsky in Russian, one must learn and know the Russian alphabet at the very least or something.
- linkdd 5y ago
  In ZFC theory (fundamental maths), "A in B" means "there is a relation between A and B, and this relation is called 'in'". Replace 'in' by the correct math symbol or anything you want, it works the same. From this, we can define a new relation called "=" such as: for all x in A and for all y in B, x in B and y in A We don't care what A, B, x or y are. We don't care what "x in A" means. It's just logical statements that are useful, and we build the rest of maths upon it. For me "=" does not mean "equal", "equivalent", or anything. It means "there is a relation between 2 objects". For example: - in a programming language "a = 3" means that "a" is related to "3" - in a BNF grammar "rule := term term term" means that "rule" is related to "term term term" - in a math equation "y = x + 1" means there is a relation between "y" and "x + 1" - on some old calculator "A <- 1" means there is a relation between "A" and "1" In each of those domains, the relation is precisely defined. But it does not need to be the same relation (they are different math theories). Another example, "y = x + 1" could be interpreted as "there is a value for x for which I can replace x + 1 by y". You don't even have to care about what "x + 1" means.
- macrolocal 5y ago
  Two maybe helpful examples: - Objects are equal to themselves canonically, but they can be equivalent to themselves in many ways, often called "symmetries." - Bool is equivalent to a single bit in two ways, depending on whether 0 or 1 means True.
- sharkbot 5y ago
  You’ve hit upon one of the key insights in category theory. It’s been awhile, let me see if I can remember enough to describe the sketch… “Equality” is a tricky concept, and various branches of mathematics have slightly different ideas (or axioms) of equality. Simple arithmetic is based upon strict equality: two things are equal if and only if a sequence of logical steps are followed precisely and the final answer matches exactly. Other branches have looser (or just different) versions of equality: set theory may use a relation to induce an equivalence relation, topology may see things as equal based on structure preserving transformations, computer science has notions of program equivalence based on identical outputs given identical inputs, etc. Category theory is an attempt to identify and unify various similar concepts across mathematical branches, including “equality”. Category theorists are limited to talking about objects (which are opaque), and arrows between those objects. Using those (incredibly) abstract tools, how does one define “equality”? The answer is, one can’t, so what are the closest things possible that capture “equality”, and can be specialized back into more traditional notions as needed. Part of the confusion is that category theory is described from the “arrows and objects” perspective, when the really interesting stuff happens two layers higher (natural transformations and above). And another part of the confusion is that many mathematicians see category theory as needless nonsense :)
  - User23 5y ago
    > “Equality” is a tricky concept, and various branches of mathematics have slightly different ideas (or axioms) of equality. Due to my own circumstances I’m drawn to notions of equality that have pragmatic value. One of my favorite is Leibniz’s rule x=y => f(x)=f(y) I use that rule so frequently and effectively when reasoning about programs that pragmatically I’m not interested in a model where it doesn’t hold. It looks very simple, but it’s practically foundational for reasoning about predicate transformers. Incidentally, I’d be really interested in a rigorous rendition of Dijkstra and Scholten’s work on program semantics in the language of category theory.
    - zozbot234 5y ago
      Leibniz's rule does hold under these generalized notions of isomorphism and equivalence. Each of these notions implicitly sets apart some class of functions `f` as "not evil", i.e. as respecting Leibniz's rule wrt. that equivalence. So as long as your predicate transformers are not "evil" in that sense, you'll be covered. And in practice, trying to work with possibly "evil" functions without a clear notion of what equivalences would render them "not evil" is generally a waste of effort and leads to results that are not semantically useful.
- Sheneneh 5y ago
  What you have up there is an equality. For example, x = y means x and y are the exact same thing. Equality is one example of equivalence relation of which there are a ton. Equivalence relation is a more general concept. A set is a bag of items. We usually call these items elements of a set. For example, {1, 2, 4} is a set containing elements 1, 2, 4. Ordered pairs are tuples written like so: (a, b) where (a, b) != (b, a). Relation is an association from one set to another. For example, a -> x, b -> &, c -> apple is a relation from {a, b, c} to {x, &, apple}. Let R stand for this relation, then we write R = {(a, x), (b, &), (c, apple)} where R associates a with x, b with & and c with apple. Consider the sets X = {1, 2, 4, 5} and Y = {6, 9, 1000, 5} with the following association R from X to Y: 1 -> 9, 2 -> 6, 4 -> 1000, 5 -> 5. This R looks like an ordering relation meaning this R is ≤. Let's see, 1 ≤ 9, 2 ≤ 6, 4 ≤ 1000, 5 ≤ 5. Then ≤ = {(1, 9), (2, 6), (4, 1000), (5, 5)}. Some relations are called functions if they meet certain criteria. If a relation R abides by the following rules it is called an equivalence relation. For any a, b, c in a set S: 1. (a, a) in R 2. If (a, b) in R, then (b, a) in R 3. If (a, b) and (b, c) in R, then (a, c) in R. For example, congruence modulo integer n is an equivalence relation as it abides by the three rules above which can be easily shown. Two integers a, b are congruent modulo n if n divides a - b. Equality is but one of many different equivalence relations. What I wrote above doesn't even come close to scratching the surface of this topic. However, any introductory textbook on abstract algebra, discrete math or elementary number theory will have this material well fleshed out. Also, every intro to proofs book dedicates significant number of pages to the topic of relations. But this stuff is very elementary and many steps removed from category theory and so you are missing some foundational background to understand the topic broached in the article. You want to have some experience with abstract algebra and general topology before approaching category theory. As for the equality you gave above, let X = 1 + x + x^2 + ... and Y = 1/(1 - x). Then X is a geometric series and X = Y only if |x| < 1. If |x| >= 1, then X diverges. When X = Y, you cannot talk about one side of the equality diverging and the other not as they both are the same object. This topic of geometric series (and many others) can be found in any textbook on elementary real analysis. Textbooks are great because they start from the beginning, don't leave out (or add) some random topics, give airtight definitions and the statements are given watertight proofs (like that one above about X = Y needs proof).
- civilized 5y ago
  Mathematician here. I understand why some people interpreted this post as dismissive of the article's premise. But I wish it could be okay, on a forum that putatively exists for founders and makers and challengers of the status quo, to say "this doesn't make sense when I think about it on a deeper level". Even if the reason it doesn't make sense to the speaker is because the speaker isn't an expert, and ultimately the thing does make sense. A challenge or contradiction doesn't have to be disparaging. We are all laymen sometimes, and sometimes we just want to scratch an itch. It usually comes from a place of curiosity, not arrogance. We want to understand how something that seems weird to us can actually make sense, even if our understanding of only limited and superficial. Why not let people express that in a direct way, without a bunch of deferential throat-clearing ("not an expert, just my thoughts here, this doesn't make sense to me...")? Who is hurt?
  - yesenadam 5y ago
    Great comment, thank you. Also, bravely asking these obvious, "stupid", elephant-in-the-room, naive questions on HN is a great place for a discussion to start, and will attract people who can explain things in simple terms. The comments will be more useful reading to more people than ones on a high, technical level. 'Being wrong on the internet' attracts truth. It's not the experts who will object to such questions!
    - civilized 5y ago
      And as a complete non-expert in this subfield of math (or anything within a hundred miles of it) I would love to hear why people are saying stuff like "equality is a fundamental mistake of mathematics and this approach is fixing it" rather than "this approach is developing a more refined/general/flexible notion of equality". After a few minutes of deferential throat clearing, I'd like to say "in all seriousness, come on, equality isn't a mistake, and whatever brilliant insight your theory affords still isn't going to do away with it."
  - galaxyLogic 5y ago
    Programs and logical proofs are "isomorphic" according to Curry-Howard. So logical theories like math in general are "programs". Two programs can be "equal" in the sense that same inputs produce the same outputs, yet their source-code can be very different. Therefore to explain a theory to a layman or anybody consider that your theory is a program, and therefore there can be any number of equal/equivalent but different programs, i.e. representations of that theory that are "equivalent" but have a different representation. Therefore, and this is the point I'm trying to make, (and maybe I'm wrong) any good explanation of a theory could also be presented in some other way, and possibly in a simpler way. Programmers know this intuitively: You can write the same program in a complicated way or in a much simpler way, sometimes. Therefore the fact that some math is difficult to understand may in fact not be the fault of the student, but of that "math" itself. And therefore it is useful that people come up with questions about what they find difficult to understand about a given theory. The "stupid" questions reveal something about the theory, they reveal what is difficult about it, what kind of mistakes people make when trying to understand it.
- zozbot234 5y ago
  > In case it wasn't clear, I'm hoping someone can explain how this notion of equivalence differs from what we've traditionally called equality since middle school, given that the latter doesn't appear to mean exactly the same either. The point is that what's called "equality" in current foundations of mathematics is not equality in the middle-school math sense, but something far more restrictive. There are older, property-based notions of "equivalence relation" that broaden this a bit, but not nearly enough for many uses. OP describes a logical formalism that might enable us to make rigorous, watertight inferences about something really, really close to what a middle-schooler would call "equality". It gets rid of a pervasive abuse of mathematical language and notation, a worrying "gap" in previous attempts to make mathematical reasoning rigorous.
- charcircuit 5y ago
  >even x / x = 1 They aren't equal if x is 0. The full statement would be x / x = 1, x ≠ 0. Or in English any number divided by itself except for 0 is 1.
harshreality 5y ago
tl;dr seems to be that some mathematicians think Jacob Lurie's work on infinity categories points to a better concept of equivalence than normal equivalence relations. Those mathematicians have been playing fast and loose with developing this theory, and now a few of them are trying to construct infinity categories of infinity categories that they think might fill holes in some of the less than rigorous work that's been going on. That sounds interesting, but unless higher category theory has any meaningful applications to non-mathematicians learning math in high school or undergraduate, saying that any of this will replace the equals sign or the standard notion of equivalence relations is overselling it.
- Koshkin 5y ago
  This page lists some applications outside mathematics: https://ncatlab.org/nlab/show/applications+of+%28higher%29+category+theory https://ncatlab.org/nlab/show/applications+of+%28higher%29+c...
- stepchowfun 5y ago
  > That sounds interesting, but unless higher category theory has any meaningful applications to non-mathematicians learning math in high school or undergraduate, saying that any of this will replace the equals sign or the standard notion of equivalence relations is overselling it. It's possible that our new understanding of equality as it appears in higher category theory and homotopy type theory will finally make working with proof assistants sufficiently practical for mathematicians, since it enables reasoning in a way that is closer to how mathematicians reason informally (treating isomorphic objects as equal, working with quotients, etc.). This area of research is obviously an active construction site, but we've seen incredible progress in the past two decades (e.g., cubical type theory). In high school, we often work informally with notions that have a more formal treatment as one progresses to university and graduate school. For example, in high school, one might be introduced to calculus by learning some rules for calculating derivatives and antiderivatives. Later, in university, those calculations are justified by real analysis. One could imagine a similar treatment of equality: in high school, we learn how to do equational reasoning by substitution, and then in university maybe we'd learn about (for example) how equality is defined as an inductive family and how substitution is justified by its corresponding induction principle. So, your comment seems a bit short-sighted or closed-minded to me, even if you're correct that this will not have any impact on high school mathematics. I just think that's a poor measuring stick for impact.
VirusNewbie 5y ago
Hopefully someone can explain here because I feel like equivalence fails in the same way equality does. Is 1 + 2 == 3? well, I understand they're equivalent, but they're not the same terms. Is (1+(1+1)) the same amount of equivalence to 3 as 1+2 is? I'd much prefer a notion that could look at how 'equivalent' terms are opposed to just looking at equality after β-reduction.
- openfuture 5y ago
  There is such a notion. You write a number on the equality sign saying essentially how many operations can be performed so 1+2 is equal to 3 if that number is larger than 0 (the special case of 0 is reflexivity, i.e. true equality). This is used a lot in some computer science stuff I've seen.
  - VirusNewbie 5y ago
    thanks for letting me know, do you know if there's a term for that notation?
- hither_shores 5y ago
  That's the "infinity": ordinary (1-)categories have (1-)arrows between objects, 2-categories have 2-arrows between 1-arrows, 3-categories have 3-arrows between 2-arrows, and so on. Infinity-categories have (k+1)-arrows between k-arrows all the way up. (And a 0-category is just a set: objects, but no arrows) > Is (1+(1+1)) the same amount of equivalence to 3 as 1+2 is? I'd much prefer a notion that could look at how 'equivalent' terms are opposed to just looking at equality after β-reduction. "Amounts" of equivalence between terms isn't really the right notion here: there's not much you can do with "an equivalence exists", which is all that "X and Y are equivalent" really means. A 2-equivalence (which in this context I think is going to end up being something like a rewrite rule?) should be an equivalence between particular programs, not the whole space of programs implementing a given function.
- edflsafoiewq 5y ago
  In algebra, monads are used to reify the notion of an "explicit expression". So you have the integers, Z, and the monad m gives m(Z), the set of expressions (let's say sums) over Z. And then you have m(m(Z)) which is nested expressions and so on. An algebra for a monad evaluates an expression m(Z)->Z, and all the monad laws basically enforce the kind of equational reasoning ordinary notation takes for granted (eg sub-expressions can be replaced by their value, 1+(1+1)=1+2). So those would be related in this way join (1)+(1+1) : m(m(Z)) -----> 1+1+1 : m(Z) | | fmap(eval) | | eval v v 1+2 : m(Z) -----------> 3 : Z eval
stepchowfun 5y ago
To the folks in this thread who think they know better than researchers at the forefront of foundational mathematics: I encourage you to learn type theory, and especially homotopy type theory. In doing so, you'll be forced to confront the various notions of judgmental and propositional equality. You'll see why it's useful to have a formal justification for treating isomorphic objects as equal (this is called "univalence"), which is something you may have even been doing informally/subconsciously all along. In particular, homotopy type theory is a type theory, which means it looks like a programming language. So people here might find it a bit more familiar than, say, higher category theory. It'll be much easier if you know functional programming, so you may need to learn that first if you haven't already.
- spekcular 5y ago
  This is not "foundational mathematics." This is about the foundations of algebraic topology. The experts in the foundations of mathematics as a whole (set theorists, logicians, model theorists, etc.) don't care about homotopy type theory. It's sort of pointless for the study of the foundations of mathematics. That is, they really just care about ZF or ZFC, because those are already formulated so that they are maximally useful for foundational investigations. (And the e.g. reverse mathematics people who want to work outside of ZF/ZFC already have more direct ways of doing so.) Some idea of what people in foundations think about day-to-day can be gleaned by searching the Foundations of Math mailing list archive: https://cs.nyu.edu/pipermail/fom/ https://cs.nyu.edu/pipermail/fom/ In particular: don't confuse higher category theory (of interest to the algebraic topology community at large) with homotopy type theory (which is not). Jacob Lurie has a rather pointed conversation with Urs Schreiber about this, linked to here: https://mathematicswithoutapologies.wordpress.com/2015/05/18/jacob-lurie-explains-and-elaborates-on-his-no-comment/ https://mathematicswithoutapologies.wordpress.com/2015/05/18.... edit: I'd love to hear from the downvoters why they disagree with this take. It's pretty standard, afaik.
  - zozbot234 5y ago
    > I'd love to hear from the downvoters why they disagree with this take. It's pretty standard, afaik. Because it's obtuse. There are well-known ways of phrasing all of this stuff in set theory (or rather, "legitimate" varieties of set theory) should anyone really care, replicating type-theoretical constructions by adding increasingly large "inaccessible cardinals" to one's pre-existing notion of set. But it's a pointless exercise when the type-theoretical description of these foundations is so much easier to work with. It's only useful if one believes that "set theory" is the only legitimate language for talking about anything foundational, which is again quite silly.
mark_l_watson 5y ago
I bought a book on Category Theory by Emily Riehl that I find myself unable to get through. I both find her talks on YouTube to be more digestible, and I also wish I was better at mathematics.
- kevinventullo 5y ago
  I learned a lot from The Catsters on YouTube, way back in 2007 or so.
- Koshkin 5y ago
  Yeah, in the continuum of texts on category theory, Riehl’s book is somewhere on the advanced side…
  - throwoutway 5y ago
    What exists in the most elementary side?
    - Koshkin 5y ago
      On a reasonably elementary level, I like Perrone's Notes (with examples from basic math) and Barr's book "for computer scientists." Books for a more general audience I know of are Conceptual Mathematics by Lawvere and Schanuel, and one "for the sciences" by Spivak.
hamiltonians 5y ago
imagine if this guy became a trader. He would crush it, like james simmons. i wish there was more research into mathamatical finance, but if anyone had something good they would use it to make money, not publish it.
- jmeister 5y ago
  Quanta is funded by Jim Simons, so it seems JS himself disagrees with you on the value of academic research.
  - hamiltonians 5y ago
    what are the odds james would divulge his highly profitable trading secrets for the sake of knowledge.
rocqua 5y ago
One thing I did not find in thr article is what the improvement here is. If I read it (and some of the comments here) correctly the idea is to replace equality from ZFC (so isomorphic sets) with equality in categories (so isomorphic objects in a k-category). The article says something about better describing all the isomorphisms, but doesn't explain why that is better. A comment here suggested to me that this system might make it easier to rigorously 'compose' different types of equivalence relationships. Something like "this field extension has a galois group 'equivalent' to A. And field extensions of A have this other property so this field extensions must also have this property". Am I on the right track as to what improvements this system offers?
- Twisol 5y ago
  As a relative layperson alongside you, I'm not sure what precise deficit Lurie is addressing. But having spent some deep time in a proof assistant (Agda) lately, I think there is a related issue. Formally, equality can be "intensional" or "extensional". An intensional theory equality says that things are the same only when they are defined the same way. So, for instance, "the set of even primes" and "the set of primes less than 3" are not intensionally the same. In contrast, an extensional theory says that things are the same when they behave the same. Both sets answer the same membership questions the same way -- 2 is the only element of either -- so they are the same set. ZFC is fundamentally extensional -- one of its axioms is literally called the axiom of extensionality, defining equality in terms of membership. In deeply identifying the above sets, we lose some of the ability to distinguish them formally and model the way in which they are equivalent. That's one guess. Another, less specific guess is that it's much like how the dual of a vector space is isomorphic to the original vector space, but in a way that depends on certain arbitrary choices. Meanwhile, the dual of the dual is naturally isomorphic to the original vector space. Thus, there are qualities of equivalence that we're interested in. (But this example is perfectly well captured by linear algebra as it stands.)
- mattalex 5y ago
  In standard mathmatics you cannot identify isomorphic objects without the use of an informal argument or abuse of notation: The issue is that the two equivalent objects aren't actually identical, they just behave the same in some way. This becomes necessary if you look at more complex objects than the ones equality was originally designed to tackle: a permutationsort and a quicksort are not the same, therefore you can't (at least in the original sense of equality) write permutationsort=quicksort. Of course you can invoke the notion of Leibniz equality and say that ∀x. permutationsort(x) = quicksort(x), therefore they are the same. However, you can't generally replace every occurrence of "quicksort" in your program with "permutationsort" because most likely your program is not going to finish before the heat-death of the universe. So for your program, you need to be able to express the notion of "they two algorithms have to be the same wrt. their (input,output) pairs and asymptotic runtime". However, if you ask your friend, the pure mathematician, you will notice he is quite fine with either one of them, because for the soundness of his new algorithm he just needs _some_ sorting algorithm: In fact, he wants that every sorting algorithm works, not just the specific one he chose to prove his algorithm with. The third person you go to is your old computational-complexity theory professor: From his point of view, permutationsort and quicksort aren't the same at all, but quicksort and matrix-multiplicationa are: after all, they are both P-TIME algorithms. Meanwhile your, at this point very confused, mathematics student comes up to you and asks "if we take a vector space with basis {(1,0),(0,1)} and transform it into a new vectorspace {(1,2),(0,1)}, are they still the same?" and simultaneously two mathmaticians stand up, one saying "yes of course, both describe the ℝ²" and the second will say "no they are not: clearly one is an orthogonal basis, while the other isn't". Depending on the proof you want to do, both can be right. Importantly here is that all of these aren't only considered "equivalent" they are considered "equal", just like you would consider the same algorithm written in Java and C++ as the same, even though they clearly aren't. Therefore, what you want to do is extend the notion of equality such that these notions of equivalence are covered by it. For that, you need a more fine-grained notion of equality, which leads to the equality to be "indexed" by its proof (after all, you need to know which "equality" you were talking about). This will very quickly lead you to the notion of "paths as equalities" and the univalence axiom. So you get rid of the uniqueness of identity axiom, and instead build different notions of equality on different "levels" to have all these notions of equality (and many more) in your system natively.

123 points by sebg 5y ago

Maybe Jacob Lurie and Stephen Wolfram can collaborate on doing Higher Categories in finite automata for the win.

Except equality never meant "exactly the same" to begin with, though, right? Like we write 1 / (1 - x) = 1 + x + x^2 + ..., but one of them diverges for x = 2 and the other doesn't, so they're not "exactly the same", just equivalent in some sense. Or heck, even x / x = 1 doesn't mean the two are exactly the same. I'm not sure how far you could take math if you treat equality as meaning "exactly the same"; it seems even middle-school math requires understanding that that's not the case. Edit: In case it wasn't clear, I'm hoping someone can explain how this notion of equivalence differs from what we've traditionally called equality since middle school, given that the latter doesn't appear to mean exactly the same either.

alecst 5y ago
In both of your examples equality holds for x in some specified domain. The first equation is not valid (outside of, say, analytical continuation) for x >= 1. I thought the article was cool. From this comment, you are coming across as someone who is trivializing a potentially important piece of work. I didn’t really understand it, but I take mathematicians at IAS seriously.
- dataflow 5y ago
  Why the ad hominem? I have nothing against the mathematicians or their work. I don't even know the math; that's why I'm reading the article. And I'm just trying to wrap my head around the article's explanation and trying to figure out why its premise seems inconsistent with my understanding. The problem is more likely somewhere in my understanding, so I posted it here in case somebody could clarify whether/what I'm misunderstanding of the difference between what we've called "equality" and what they're calling "equivalent", given neither of them seems to necessarily mean "exactly the same".
  - Quekid5 5y ago
    Well, as a disinterested observer, I think it was the > Except equality never meant... ... opening to your comment which immediately makes you look like you're being antagonistic. ("except", and "never" probably being the key words. Especially opening with "except"...)
- yesenadam 5y ago
  > you are coming across as someone who is trivializing a potentially important piece of work. I didn't get that impression at all. Rather, you came across as needlessly insulting. Why add that sentence, even if you thought so?! "Be kind."
  - alecst 5y ago
    Hey so I was replying to this part: > I'm not sure how far you could take math if you treat equality as meaning "exactly the same"; it seems even middle-school math requires understanding that that's not the case. I honestly didn't mean that in a rude way, more like a "hey dude, be careful how you're coming across here, as there may be things you don't understand." I read the above phrase as describing a mathematician's work as something a middle schooler should already know. But I take back what I said. I'm all good, everyone's good, I think there was just a misunderstanding here. In the same vein, I don't see how you could read my message as needlessly insulting, as I thought it was pretty softly worded. But I guess that's the nature of written communication. I think you should have given me the benefit of the doubt, just as I should have done for the original poster.
    - yesenadam 5y ago
      No, it wasn't softly worded. Now you take back what you said, although it was fine and I'm the one in the wrong to think it was insulting?! Etc. I don't think those are reasonable interpretations. Your comment was good without the last paragraph. Can't help sinking the boot in, eh? That's not a very nice habit. But anyway, I have things to do today! See ya.
- Sheneneh 5y ago
  > you are coming across as someone who is trivializing a potentially important piece of work. I doubt it. The parent is confused and hence the question obviously. But I get the impression that the parent would benefit from reading an elementary textbook on discrete math as the post is gibberish (as are a few other posts in this thread). I know it sounds rude, but I don't know how else to put it. It's not only the fact that the parent doesn't have a conceptual idea about equivalence relations and in particular equality, isomorphism, let alone homotopy, but is also very confused about what it means for a series to converge which is also very elementary. Before discussing the merits of Dostoevsky in Russian, one must learn and know the Russian alphabet at the very least or something.
linkdd 5y ago
In ZFC theory (fundamental maths), "A in B" means "there is a relation between A and B, and this relation is called 'in'". Replace 'in' by the correct math symbol or anything you want, it works the same. From this, we can define a new relation called "=" such as: for all x in A and for all y in B, x in B and y in A We don't care what A, B, x or y are. We don't care what "x in A" means. It's just logical statements that are useful, and we build the rest of maths upon it. For me "=" does not mean "equal", "equivalent", or anything. It means "there is a relation between 2 objects". For example: - in a programming language "a = 3" means that "a" is related to "3" - in a BNF grammar "rule := term term term" means that "rule" is related to "term term term" - in a math equation "y = x + 1" means there is a relation between "y" and "x + 1" - on some old calculator "A <- 1" means there is a relation between "A" and "1" In each of those domains, the relation is precisely defined. But it does not need to be the same relation (they are different math theories). Another example, "y = x + 1" could be interpreted as "there is a value for x for which I can replace x + 1 by y". You don't even have to care about what "x + 1" means.
macrolocal 5y ago
Two maybe helpful examples: - Objects are equal to themselves canonically, but they can be equivalent to themselves in many ways, often called "symmetries." - Bool is equivalent to a single bit in two ways, depending on whether 0 or 1 means True.
sharkbot 5y ago
You’ve hit upon one of the key insights in category theory. It’s been awhile, let me see if I can remember enough to describe the sketch… “Equality” is a tricky concept, and various branches of mathematics have slightly different ideas (or axioms) of equality. Simple arithmetic is based upon strict equality: two things are equal if and only if a sequence of logical steps are followed precisely and the final answer matches exactly. Other branches have looser (or just different) versions of equality: set theory may use a relation to induce an equivalence relation, topology may see things as equal based on structure preserving transformations, computer science has notions of program equivalence based on identical outputs given identical inputs, etc. Category theory is an attempt to identify and unify various similar concepts across mathematical branches, including “equality”. Category theorists are limited to talking about objects (which are opaque), and arrows between those objects. Using those (incredibly) abstract tools, how does one define “equality”? The answer is, one can’t, so what are the closest things possible that capture “equality”, and can be specialized back into more traditional notions as needed. Part of the confusion is that category theory is described from the “arrows and objects” perspective, when the really interesting stuff happens two layers higher (natural transformations and above). And another part of the confusion is that many mathematicians see category theory as needless nonsense :)
- User23 5y ago
  > “Equality” is a tricky concept, and various branches of mathematics have slightly different ideas (or axioms) of equality. Due to my own circumstances I’m drawn to notions of equality that have pragmatic value. One of my favorite is Leibniz’s rule x=y => f(x)=f(y) I use that rule so frequently and effectively when reasoning about programs that pragmatically I’m not interested in a model where it doesn’t hold. It looks very simple, but it’s practically foundational for reasoning about predicate transformers. Incidentally, I’d be really interested in a rigorous rendition of Dijkstra and Scholten’s work on program semantics in the language of category theory.
  - zozbot234 5y ago
    Leibniz's rule does hold under these generalized notions of isomorphism and equivalence. Each of these notions implicitly sets apart some class of functions `f` as "not evil", i.e. as respecting Leibniz's rule wrt. that equivalence. So as long as your predicate transformers are not "evil" in that sense, you'll be covered. And in practice, trying to work with possibly "evil" functions without a clear notion of what equivalences would render them "not evil" is generally a waste of effort and leads to results that are not semantically useful.
Sheneneh 5y ago
What you have up there is an equality. For example, x = y means x and y are the exact same thing. Equality is one example of equivalence relation of which there are a ton. Equivalence relation is a more general concept. A set is a bag of items. We usually call these items elements of a set. For example, {1, 2, 4} is a set containing elements 1, 2, 4. Ordered pairs are tuples written like so: (a, b) where (a, b) != (b, a). Relation is an association from one set to another. For example, a -> x, b -> &, c -> apple is a relation from {a, b, c} to {x, &, apple}. Let R stand for this relation, then we write R = {(a, x), (b, &), (c, apple)} where R associates a with x, b with & and c with apple. Consider the sets X = {1, 2, 4, 5} and Y = {6, 9, 1000, 5} with the following association R from X to Y: 1 -> 9, 2 -> 6, 4 -> 1000, 5 -> 5. This R looks like an ordering relation meaning this R is ≤. Let's see, 1 ≤ 9, 2 ≤ 6, 4 ≤ 1000, 5 ≤ 5. Then ≤ = {(1, 9), (2, 6), (4, 1000), (5, 5)}. Some relations are called functions if they meet certain criteria. If a relation R abides by the following rules it is called an equivalence relation. For any a, b, c in a set S: 1. (a, a) in R 2. If (a, b) in R, then (b, a) in R 3. If (a, b) and (b, c) in R, then (a, c) in R. For example, congruence modulo integer n is an equivalence relation as it abides by the three rules above which can be easily shown. Two integers a, b are congruent modulo n if n divides a - b. Equality is but one of many different equivalence relations. What I wrote above doesn't even come close to scratching the surface of this topic. However, any introductory textbook on abstract algebra, discrete math or elementary number theory will have this material well fleshed out. Also, every intro to proofs book dedicates significant number of pages to the topic of relations. But this stuff is very elementary and many steps removed from category theory and so you are missing some foundational background to understand the topic broached in the article. You want to have some experience with abstract algebra and general topology before approaching category theory. As for the equality you gave above, let X = 1 + x + x^2 + ... and Y = 1/(1 - x). Then X is a geometric series and X = Y only if |x| < 1. If |x| >= 1, then X diverges. When X = Y, you cannot talk about one side of the equality diverging and the other not as they both are the same object. This topic of geometric series (and many others) can be found in any textbook on elementary real analysis. Textbooks are great because they start from the beginning, don't leave out (or add) some random topics, give airtight definitions and the statements are given watertight proofs (like that one above about X = Y needs proof).
civilized 5y ago
Mathematician here. I understand why some people interpreted this post as dismissive of the article's premise. But I wish it could be okay, on a forum that putatively exists for founders and makers and challengers of the status quo, to say "this doesn't make sense when I think about it on a deeper level". Even if the reason it doesn't make sense to the speaker is because the speaker isn't an expert, and ultimately the thing does make sense. A challenge or contradiction doesn't have to be disparaging. We are all laymen sometimes, and sometimes we just want to scratch an itch. It usually comes from a place of curiosity, not arrogance. We want to understand how something that seems weird to us can actually make sense, even if our understanding of only limited and superficial. Why not let people express that in a direct way, without a bunch of deferential throat-clearing ("not an expert, just my thoughts here, this doesn't make sense to me...")? Who is hurt?
- yesenadam 5y ago
  Great comment, thank you. Also, bravely asking these obvious, "stupid", elephant-in-the-room, naive questions on HN is a great place for a discussion to start, and will attract people who can explain things in simple terms. The comments will be more useful reading to more people than ones on a high, technical level. 'Being wrong on the internet' attracts truth. It's not the experts who will object to such questions!
  - civilized 5y ago
    And as a complete non-expert in this subfield of math (or anything within a hundred miles of it) I would love to hear why people are saying stuff like "equality is a fundamental mistake of mathematics and this approach is fixing it" rather than "this approach is developing a more refined/general/flexible notion of equality". After a few minutes of deferential throat clearing, I'd like to say "in all seriousness, come on, equality isn't a mistake, and whatever brilliant insight your theory affords still isn't going to do away with it."
- galaxyLogic 5y ago
  Programs and logical proofs are "isomorphic" according to Curry-Howard. So logical theories like math in general are "programs". Two programs can be "equal" in the sense that same inputs produce the same outputs, yet their source-code can be very different. Therefore to explain a theory to a layman or anybody consider that your theory is a program, and therefore there can be any number of equal/equivalent but different programs, i.e. representations of that theory that are "equivalent" but have a different representation. Therefore, and this is the point I'm trying to make, (and maybe I'm wrong) any good explanation of a theory could also be presented in some other way, and possibly in a simpler way. Programmers know this intuitively: You can write the same program in a complicated way or in a much simpler way, sometimes. Therefore the fact that some math is difficult to understand may in fact not be the fault of the student, but of that "math" itself. And therefore it is useful that people come up with questions about what they find difficult to understand about a given theory. The "stupid" questions reveal something about the theory, they reveal what is difficult about it, what kind of mistakes people make when trying to understand it.
zozbot234 5y ago
> In case it wasn't clear, I'm hoping someone can explain how this notion of equivalence differs from what we've traditionally called equality since middle school, given that the latter doesn't appear to mean exactly the same either. The point is that what's called "equality" in current foundations of mathematics is not equality in the middle-school math sense, but something far more restrictive. There are older, property-based notions of "equivalence relation" that broaden this a bit, but not nearly enough for many uses. OP describes a logical formalism that might enable us to make rigorous, watertight inferences about something really, really close to what a middle-schooler would call "equality". It gets rid of a pervasive abuse of mathematical language and notation, a worrying "gap" in previous attempts to make mathematical reasoning rigorous.
charcircuit 5y ago
>even x / x = 1 They aren't equal if x is 0. The full statement would be x / x = 1, x ≠ 0. Or in English any number divided by itself except for 0 is 1.

harshreality 5y ago

tl;dr seems to be that some mathematicians think Jacob Lurie's work on infinity categories points to a better concept of equivalence than normal equivalence relations. Those mathematicians have been playing fast and loose with developing this theory, and now a few of them are trying to construct infinity categories of infinity categories that they think might fill holes in some of the less than rigorous work that's been going on. That sounds interesting, but unless higher category theory has any meaningful applications to non-mathematicians learning math in high school or undergraduate, saying that any of this will replace the equals sign or the standard notion of equivalence relations is overselling it.

Koshkin 5y ago
This page lists some applications outside mathematics: https://ncatlab.org/nlab/show/applications+of+%28higher%29+category+theory https://ncatlab.org/nlab/show/applications+of+%28higher%29+c...
stepchowfun 5y ago
> That sounds interesting, but unless higher category theory has any meaningful applications to non-mathematicians learning math in high school or undergraduate, saying that any of this will replace the equals sign or the standard notion of equivalence relations is overselling it. It's possible that our new understanding of equality as it appears in higher category theory and homotopy type theory will finally make working with proof assistants sufficiently practical for mathematicians, since it enables reasoning in a way that is closer to how mathematicians reason informally (treating isomorphic objects as equal, working with quotients, etc.). This area of research is obviously an active construction site, but we've seen incredible progress in the past two decades (e.g., cubical type theory). In high school, we often work informally with notions that have a more formal treatment as one progresses to university and graduate school. For example, in high school, one might be introduced to calculus by learning some rules for calculating derivatives and antiderivatives. Later, in university, those calculations are justified by real analysis. One could imagine a similar treatment of equality: in high school, we learn how to do equational reasoning by substitution, and then in university maybe we'd learn about (for example) how equality is defined as an inductive family and how substitution is justified by its corresponding induction principle. So, your comment seems a bit short-sighted or closed-minded to me, even if you're correct that this will not have any impact on high school mathematics. I just think that's a poor measuring stick for impact.

VirusNewbie 5y ago

Hopefully someone can explain here because I feel like equivalence fails in the same way equality does. Is 1 + 2 == 3? well, I understand they're equivalent, but they're not the same terms. Is (1+(1+1)) the same amount of equivalence to 3 as 1+2 is? I'd much prefer a notion that could look at how 'equivalent' terms are opposed to just looking at equality after β-reduction.

openfuture 5y ago
There is such a notion. You write a number on the equality sign saying essentially how many operations can be performed so 1+2 is equal to 3 if that number is larger than 0 (the special case of 0 is reflexivity, i.e. true equality). This is used a lot in some computer science stuff I've seen.
- VirusNewbie 5y ago
  thanks for letting me know, do you know if there's a term for that notation?
hither_shores 5y ago
That's the "infinity": ordinary (1-)categories have (1-)arrows between objects, 2-categories have 2-arrows between 1-arrows, 3-categories have 3-arrows between 2-arrows, and so on. Infinity-categories have (k+1)-arrows between k-arrows all the way up. (And a 0-category is just a set: objects, but no arrows) > Is (1+(1+1)) the same amount of equivalence to 3 as 1+2 is? I'd much prefer a notion that could look at how 'equivalent' terms are opposed to just looking at equality after β-reduction. "Amounts" of equivalence between terms isn't really the right notion here: there's not much you can do with "an equivalence exists", which is all that "X and Y are equivalent" really means. A 2-equivalence (which in this context I think is going to end up being something like a rewrite rule?) should be an equivalence between particular programs, not the whole space of programs implementing a given function.
edflsafoiewq 5y ago
In algebra, monads are used to reify the notion of an "explicit expression". So you have the integers, Z, and the monad m gives m(Z), the set of expressions (let's say sums) over Z. And then you have m(m(Z)) which is nested expressions and so on. An algebra for a monad evaluates an expression m(Z)->Z, and all the monad laws basically enforce the kind of equational reasoning ordinary notation takes for granted (eg sub-expressions can be replaced by their value, 1+(1+1)=1+2). So those would be related in this way join (1)+(1+1) : m(m(Z)) -----> 1+1+1 : m(Z) | | fmap(eval) | | eval v v 1+2 : m(Z) -----------> 3 : Z eval

stepchowfun 5y ago

To the folks in this thread who think they know better than researchers at the forefront of foundational mathematics: I encourage you to learn type theory, and especially homotopy type theory. In doing so, you'll be forced to confront the various notions of judgmental and propositional equality. You'll see why it's useful to have a formal justification for treating isomorphic objects as equal (this is called "univalence"), which is something you may have even been doing informally/subconsciously all along. In particular, homotopy type theory is a type theory, which means it looks like a programming language. So people here might find it a bit more familiar than, say, higher category theory. It'll be much easier if you know functional programming, so you may need to learn that first if you haven't already.

spekcular 5y ago
This is not "foundational mathematics." This is about the foundations of algebraic topology. The experts in the foundations of mathematics as a whole (set theorists, logicians, model theorists, etc.) don't care about homotopy type theory. It's sort of pointless for the study of the foundations of mathematics. That is, they really just care about ZF or ZFC, because those are already formulated so that they are maximally useful for foundational investigations. (And the e.g. reverse mathematics people who want to work outside of ZF/ZFC already have more direct ways of doing so.) Some idea of what people in foundations think about day-to-day can be gleaned by searching the Foundations of Math mailing list archive: https://cs.nyu.edu/pipermail/fom/ https://cs.nyu.edu/pipermail/fom/ In particular: don't confuse higher category theory (of interest to the algebraic topology community at large) with homotopy type theory (which is not). Jacob Lurie has a rather pointed conversation with Urs Schreiber about this, linked to here: https://mathematicswithoutapologies.wordpress.com/2015/05/18/jacob-lurie-explains-and-elaborates-on-his-no-comment/ https://mathematicswithoutapologies.wordpress.com/2015/05/18.... edit: I'd love to hear from the downvoters why they disagree with this take. It's pretty standard, afaik.
- zozbot234 5y ago
  > I'd love to hear from the downvoters why they disagree with this take. It's pretty standard, afaik. Because it's obtuse. There are well-known ways of phrasing all of this stuff in set theory (or rather, "legitimate" varieties of set theory) should anyone really care, replicating type-theoretical constructions by adding increasingly large "inaccessible cardinals" to one's pre-existing notion of set. But it's a pointless exercise when the type-theoretical description of these foundations is so much easier to work with. It's only useful if one believes that "set theory" is the only legitimate language for talking about anything foundational, which is again quite silly.

mark_l_watson 5y ago

I bought a book on Category Theory by Emily Riehl that I find myself unable to get through. I both find her talks on YouTube to be more digestible, and I also wish I was better at mathematics.

kevinventullo 5y ago
I learned a lot from The Catsters on YouTube, way back in 2007 or so.
Koshkin 5y ago
Yeah, in the continuum of texts on category theory, Riehl’s book is somewhere on the advanced side…
- throwoutway 5y ago
  What exists in the most elementary side?
  - Koshkin 5y ago
    On a reasonably elementary level, I like Perrone's Notes (with examples from basic math) and Barr's book "for computer scientists." Books for a more general audience I know of are Conceptual Mathematics by Lawvere and Schanuel, and one "for the sciences" by Spivak.

hamiltonians 5y ago

imagine if this guy became a trader. He would crush it, like james simmons. i wish there was more research into mathamatical finance, but if anyone had something good they would use it to make money, not publish it.

jmeister 5y ago
Quanta is funded by Jim Simons, so it seems JS himself disagrees with you on the value of academic research.
- hamiltonians 5y ago
  what are the odds james would divulge his highly profitable trading secrets for the sake of knowledge.

rocqua 5y ago

One thing I did not find in thr article is what the improvement here is. If I read it (and some of the comments here) correctly the idea is to replace equality from ZFC (so isomorphic sets) with equality in categories (so isomorphic objects in a k-category). The article says something about better describing all the isomorphisms, but doesn't explain why that is better. A comment here suggested to me that this system might make it easier to rigorously 'compose' different types of equivalence relationships. Something like "this field extension has a galois group 'equivalent' to A. And field extensions of A have this other property so this field extensions must also have this property". Am I on the right track as to what improvements this system offers?

Twisol 5y ago
As a relative layperson alongside you, I'm not sure what precise deficit Lurie is addressing. But having spent some deep time in a proof assistant (Agda) lately, I think there is a related issue. Formally, equality can be "intensional" or "extensional". An intensional theory equality says that things are the same only when they are defined the same way. So, for instance, "the set of even primes" and "the set of primes less than 3" are not intensionally the same. In contrast, an extensional theory says that things are the same when they behave the same. Both sets answer the same membership questions the same way -- 2 is the only element of either -- so they are the same set. ZFC is fundamentally extensional -- one of its axioms is literally called the axiom of extensionality, defining equality in terms of membership. In deeply identifying the above sets, we lose some of the ability to distinguish them formally and model the way in which they are equivalent. That's one guess. Another, less specific guess is that it's much like how the dual of a vector space is isomorphic to the original vector space, but in a way that depends on certain arbitrary choices. Meanwhile, the dual of the dual is naturally isomorphic to the original vector space. Thus, there are qualities of equivalence that we're interested in. (But this example is perfectly well captured by linear algebra as it stands.)
mattalex 5y ago
In standard mathmatics you cannot identify isomorphic objects without the use of an informal argument or abuse of notation: The issue is that the two equivalent objects aren't actually identical, they just behave the same in some way. This becomes necessary if you look at more complex objects than the ones equality was originally designed to tackle: a permutationsort and a quicksort are not the same, therefore you can't (at least in the original sense of equality) write permutationsort=quicksort. Of course you can invoke the notion of Leibniz equality and say that ∀x. permutationsort(x) = quicksort(x), therefore they are the same. However, you can't generally replace every occurrence of "quicksort" in your program with "permutationsort" because most likely your program is not going to finish before the heat-death of the universe. So for your program, you need to be able to express the notion of "they two algorithms have to be the same wrt. their (input,output) pairs and asymptotic runtime". However, if you ask your friend, the pure mathematician, you will notice he is quite fine with either one of them, because for the soundness of his new algorithm he just needs _some_ sorting algorithm: In fact, he wants that every sorting algorithm works, not just the specific one he chose to prove his algorithm with. The third person you go to is your old computational-complexity theory professor: From his point of view, permutationsort and quicksort aren't the same at all, but quicksort and matrix-multiplicationa are: after all, they are both P-TIME algorithms. Meanwhile your, at this point very confused, mathematics student comes up to you and asks "if we take a vector space with basis {(1,0),(0,1)} and transform it into a new vectorspace {(1,2),(0,1)}, are they still the same?" and simultaneously two mathmaticians stand up, one saying "yes of course, both describe the ℝ²" and the second will say "no they are not: clearly one is an orthogonal basis, while the other isn't". Depending on the proof you want to do, both can be right. Importantly here is that all of these aren't only considered "equivalent" they are considered "equal", just like you would consider the same algorithm written in Java and C++ as the same, even though they clearly aren't. Therefore, what you want to do is extend the notion of equality such that these notions of equivalence are covered by it. For that, you need a more fine-grained notion of equality, which leads to the equality to be "indexed" by its proof (after all, you need to know which "equality" you were talking about). This will very quickly lead you to the notion of "paths as equalities" and the univalence axiom. So you get rid of the uniqueness of identity axiom, and instead build different notions of equality on different "levels" to have all these notions of equality (and many more) in your system natively.