# Are Univalent Foundations of mathematics a modern version of logicism?

As I understand it (and mine is just basic understanding) the Univalent Foundations program is an attempt to reduce mathematics to an interpretation of Martin-Löf type theory by using homotopy theory. Is this not a revamped version of the logicist program (using type theory instead of FOL and homotopy theory as the semantics) and, consequently, doesn't it face the objections logicism faced? By the logicist program I mean the (Fregean) attempt of reducing mathematics to logic.

• Comment : the Fregeam project was "revamped" by W&R Principia with the Theory of Types that addressed the contradictions due to the original (Fregean) version of Logicism. The onjection to TT as a foundational theory a mainly "philosophical" : some axioms (like Infinity and Reducibility) are not "in the spirit" of pure logicism. From this point of view, the issues with any foundational project are two : ... 1/2 Commented Sep 28, 2015 at 8:48
• 1) its capability to give a complete and consisten "reconstruction" of existsing mathematics (or the part of it considered relevant), and 2) its "plausibility" form a philosophical point of view. Axiomatic set theory, for example, as done 1) in a (quite) perfect way. About 2), the current approach is a sort of "formalism" trying to skip this issue. 2/2 Commented Sep 28, 2015 at 8:50
• @Caro Lori Probably you like to check a related post from math.stackexchange: math.stackexchange.com/questions/361986/… Commented Sep 28, 2015 at 10:34

If anything, univalent foundations share more with constructivism and formalism than with logicism, and even with them it shares technical apparatus more than motivations. Logicism was an ambitious project to ground all of mathematics in the self-evident laws of thought. Russell's paradox brought the realization that "laws of thought" were not as self-evident as they seemed, and Principia demonstrated that devices needed to avoid paradoxes and recover all of mathematics (like types and reducibility) are contrived and go beyond any plausible conception of logic. On the other hand, Wittgenstein's Tractatus showed what is forthcoming from plausibly logical means, iteration and substitution. That would be primitive recursive arithmetic, not even all of arithmetic, let alone all of mathematics. The last version of logicism, relativized to "linguistic frameworks" by Carnap, had a great deal of Hilbert's formalism mixed in, and was undermined along with it by Gödel's results.

Univalent programme, a.k.a. homotopy type theory (HoTT), is very young (key ideas emerged in 2005-2014) and far more pragmatic, The name "univalent" is meant in the sense of "faithful":

"Voevodsky explained his choice of the term “univalent” in [62]: it comes from a Russian translation of the Boardman and Vogt's book Homotopy Ivariant Algebraic Structures on Topological Spaces, here the term “faithful functor” is translated as “univalent functor”. He also said, “Indeed these foundations seem to be faithful to the way in which I think about mathematical objects in my head.”"

The idea is not to give mathematics a new philosophical justification, but to reconstruct most of it from a new point of view that is particularly friendly to constructive methods and automated proof verification.

"Part of the reason that Martin-Löf type theory employed in the univalent setting is that this theory has good computational properties. In technical terms, type checking in this theory is decidable. Consequently, it is possible to implement the theory on a computer. This is essentially what has been done in the case of the proof assistants Coq and Agda."

Other exciting features are that the new model of type theory (constructivist logic) found by Voevodsky in 2009 naturally interprets some of its "oddities", and is unexpectedly and non-trivially connected to more traditional areas of mathematics. Logic is modeled using topological notions, specifically homotopy theory, e.g. identity is treated as a homotopy equivalence. This allows to formalize in a principled way one of mathematicians' favorite tricks, identifying isomorphic structures. Which in turn links univalent foundations to the category theory, also well known for its intuitionistic models (elementary topoi), but with a richer and more flexible structure.

However, there is no contention that types and homotopy are more fundamental than sets, categories or other mathematical notions. Univalent foundations are meant to be a particular mathematical theory, albeit widely applicable, one foundation among many, geared to a pragmatic purpose (proof checking in Coq is even likened to typing in Latex). In this sense it is like one of Carnap's "linguistic frameworks", but without Fregean or Hilbertian ambitions.

For a brief survey I recommend first two sections of Pelayo-Warren's Homotopy Type Theory and Voevodsky's Univalent Foundations, which are more lucid than Wikipedia's articles on both subjects. The most recent review is Grayson's Introduction to univalent foundations for mathematicians.

• Thats really helpful thanks. Just to clarify something: from your description it seems as though the UF program is geared towards offering a different pov for mathematics. But then, why consider it a new foundation? - I cam across it advertised as a new foundation of mathematics that will hopefully supplant set theory etc. Commented Sep 29, 2015 at 16:10
• @Carlo Lori The view of set theory as foundations of mathematics also changed in the pragmatic direction since the days of Cantor and Hilbert. It is foundations in the sense that mathematics can be axiomatically reconstructed starting from basic properties of sets and inclusion, not that these properties are necessarily self-evident or philosophically compelling. Constructivism and category theory gave alternative foundations of this sort. In a sense, univalent program offers a synthesis of the latter two, which is structurally more attractive and broadly useful than each. Commented Sep 29, 2015 at 17:57