Multiple Concepts of Equality in the New Foundations of Mathematics by Vladimir Voevodsky

Talk at: FOMUS 2016, for all Talks and more information see: fomus.weebly.com/
Multiple Concepts of Equality in the New Foundations of Mathematics by Vladimir Voevodsky (Institute for Advanced Study, Princeton, USA)
Abstract: One of the most confusing aspects of the Univalence Axiom (UF) is that it seems to assert that, which mathematical students learn early in their education to be a mistake - that isomorphic objects are equal. The source of the confusion is in the failure of the earlier attempts to explain UF to emphasize the existence of two classes of equalities in the theories used to formalize it - substitutional equalities and transportational equalities. The concept of transportational equality is the adaptation to the precise requirements of a formal theory of the philosophical equality principle going back to Leibniz. The concept of the substitutional equality is the one that we all learn at school. In the original formal system used for the Univalent Foundations there was one transportational and one substitutional equality. In the more complex formal systems that are being studied now there can be several equalities of each class.
This workshop was organised with the generous support of the Association for Symbolic Logic (ASL), the Association of German Mathematicians (DMV), the Berlin Mathematical School (BMS), the Center of Interdisciplinary Research (ZiF), the Deutsche Vereinigung für Mathematische Logik und für Grundlagenforschung der Exakten Wissenschaften (DVMLG), the German Academic Merit Foundation (Stipendiaten machen Programm), the Fachbereich Grundlagen der Informatik of the German Informatics Society (GI) and the German Society for Analytic Philosophy (GAP).

[@scin3759]

Pity the community of mathematicians having to deal with this man who thinks SOOOOOOOOOOOOOO outside the box. His project will probably have to wait. Sad he left us so soon.

[@shouqie844]

Yes, indeed- like Grassmann's ideas. On the other hand, it seems that computers will verify proofs of ever increasing length, which is certainly disconcerting to those who work with paper and pen.

[@JoelHealy]

@Calum Tatum Once pen and paper mathematicians figure out how to express their ideas using definitions and structures that are precise enough to be investigated/verified by a computer (a.k.a "virtual graduate student"), I think the status quo will change fairly rapidly. At least I hope so.

[@kamilziemian995]

Voevodsky was very self-conscious men, that think outside the big box, I admire him very much.

[@fbkintanar]

@@JoelHealy Perhaps many of the pen and paper mathematicians will never change, and never get a hang of using a proof assistant. But if they are open-minded, they can play a role like system analysts working with coders. They will have grad students who grew up coding proofs into a proof assistant, they are digital natives. The transition will be difficult for many mathematicians and departments, but it can be made smoother. User friendly interfaces to the next generation of proof assistants, or even Lean if they bring back HoTT compability in some (cubical?) version, would be a great help.

[@kamilziemian995]

This talk was from time to time hard to understand, but it is such mind expanding that is thing that you must watch. Requiesciat in pace Voevodsky, you were a great mathematician.

[@StephenPaulKing]

Great Mathematicians are immortal, they live on in us.

[@kamilziemian995]

@@StephenPaulKing I hope we will worth of their legacy.

[@qrator2982]

well he is not native

[@buraianmath]

This is guy a fin genius... and this is the first time I've commented such a thing!

[@kamilziemian995]

1:32:00 "There is not mathematical definition what stupid means." :D

[@peterwaksman9179]

This is the new mathematics of foundations. Not new foundations.