15
$\begingroup$

This article from The New York Times is an obituary of the recently deceased Dr. Voevodsky. It explained that he was deeply involved in developing computer proof verification, and to do so "changed the meaning of the equal sign" and "reformulated mathematics from its very foundation".

As the article is targeted to a general audience, it does not go into details.

Can someone explain the meaning of these two quotes from the New York Times?

(I believe they are related)

$\endgroup$
11
  • 1
    $\begingroup$ Here's a video by Dr. Voevodsky which should help clarify $$$$ $\qquad$youtube.com/watch?v=oRqOVQXxQI4 $$$$ $\endgroup$
    – quasi
    Oct 7, 2017 at 13:28
  • 1
    $\begingroup$ Not confident enough to provide a full answer - but in some type-based foundations of mathematics, such as variants of Martin-Loef type theory used in Coq or Agda (especially Coq for this topic, as Agda tends to assume the "$K$ axiom" by default which destroys homotopy type theory): each proposition is in fact a type itself ("a proposition is the type of proofs of that proposition"). So, if you have x, y : A and two proofs e1, e2 : x = y then it makes sense to ask whether e1 = e2 and it's surprisingly not provable. Then for e3, e4 : e1 = e2 you can ask whether e3 = e4, etc. $\endgroup$
    – Daniel Schepler
    Oct 12, 2017 at 19:08
  • $\begingroup$ That starts to look somewhat like an $\infty$-category, and specifically has analogies to homotopies, homotopies between homotopies, etc. $\endgroup$
    – Daniel Schepler
    Oct 12, 2017 at 19:09
  • $\begingroup$ So, for a possible interpretation of this fact in terms of homotopies, say $A = S^1$ and you interpret x = y as the set of paths from $x$ to $y$. Then for e1, e2 : x = y, interpret e1 = e2 as the set of homotopies from path $e_1$ to path $e_2$, and in particular as a proposition e1 = e2 corresponds to the two paths being homotopic to each other. $\endgroup$
    – Daniel Schepler
    Oct 12, 2017 at 19:12
  • $\begingroup$ What I'm not so confident about: I've only seen some of the discussions of HoTT briefly from the outside, so I'm not sure whether my interpretation is in line with the HoTT project, or if my interpretation diverges somewhat from their development and/or focus. $\endgroup$
    – Daniel Schepler
    Oct 12, 2017 at 19:20

1 Answer 1

Reset to default
4
$\begingroup$

The paradigm shift here — which didn't originate with Voevodsky — is that equivalence is generally a more important notion than equality. There is a quirk that makes achieving the shift difficult: equivalence is often more complex than simply a yes/no proposition.

For example, in group theory, it's much more important to talk about whether two groups are isomorphic than whether they are equal. In fact, it's rather uncommon to do the latter.

As an example of the added complexity, consider the first isomorphism theorem of groups. The main conclusion is often stated as

If $\varphi : G \to H$ is a group homomorphism, then $G/\ker(\varphi)$ is isomorphic to $\mathrm{im}(\varphi)$

but that's only part of what it says: the first isomorphism isn't merely saying "there is an isomorphism", but that the specific function $\overline{x} \mapsto \varphi(x)$ is said isomorphism. (where $\overline{x}$ denotes the congruence class of $x$)

Talk of "changing the meaning of the equals sign" is, IMO, somewhat hyperbolic. Really, it's just describing the fact that if you have a way to reason and calculate in a way where equivalence really is the primary notion, it's useful to repurpose the symbol "=" to mean equivalence. (and if you really need the notion of equality, to find some other way to express it)

A great answer should mention homotopy type theory and/or the univalence axiom. It should also mutter something about the development of $\infty$-category theory and the search for internal languages, and also about the semantics of identity types in intensional type theory. I'm not ambitious enough to try and write a great answer, so I'll just mention the terms here to give hints for further reading.

$\endgroup$
5
  • $\begingroup$ Note I can't really speak as to what Voevodsky's contributions were. $\endgroup$
    – user14972
    Oct 12, 2017 at 20:14
  • $\begingroup$ It sounds like a good deal of this answer involves a shift from $\mathbf{Sets}$ (with Leibniz equality) to $\mathbf{Setoids}$. (Another example often given: in classical mathematics we have functional extensionality: $(\forall x, f(x) = g(x)) \rightarrow f = g$. While this is a natural equivalence to consider on function spaces, in computer science we're often concerned with algorithmic complexity of the implementations of $f$ and $g$ which isn't well-defined with respect to the "extensionally equal" equivalence.) I'm not sure how much that has to do with homotopy type theory, though... $\endgroup$
    – Daniel Schepler
    Oct 12, 2017 at 20:51
  • $\begingroup$ which as I understand it was in large part what Voevodsky's contributions were focused in. (Not that I'm at all opposed to the shift from $\mathbf{Sets}$ to $\mathbf{Setoids}$ myself.) $\endgroup$
    – Daniel Schepler
    Oct 12, 2017 at 20:52
  • $\begingroup$ So there is no answer. $\endgroup$
    – beroal
    Oct 18, 2017 at 16:47
  • $\begingroup$ @DanielSchepler: Setoids are still "equivalence as a yes/no proposition". The example of groups up to isomorphism is already beyond that: the core of Grp is a groupoid that is not a setoid. $\endgroup$
    – user14972
    Oct 18, 2017 at 18:33

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .