Formal Philosophy – 48: «Geometrical Logic versus Logical Geometry: the Case of Univalent Foundations»
On the 24th of October Andrei Rodin, Senior Research Fellow of the International Laboratory for Logic, Linguistics and Formal Philosophy, made a report “Geometrical Logic versus Logical Geometry: the Case of Univalent Foundations” on the 48th session of theoretical seminar “Formal Philosophy”.
"By Logical Geometry I mean a geometrical theory built on explicit logical grounds such as the theory of Hilbert’s epoch-making Grundlagen der Geometrie first published in 1899 and its multiple
heirs. The term “Geometric Logic” is presently used in a technical sense for referring to a class of geometrically motivated logical calculi. I use here the term “Geometrical Logic” more broadly for
referring to any system and theory of Logic where Geometry, broadly conceived, is used as a principal motivation or as a foundation. I shall briefly review the history of complicated relationships between
Logic and Geometry, touch upon the widely discussed issue of bounds of Logic in this context, and finally focus on the Univalent Foundations as a current episode of this continuing story."
1) I did not yet complete a paper that exactly corresponds to this talk but this earlier paper of mine (recently published in L&A) can be helpful: https://arxiv.org/abs/1408.3591v3
2) For a gentle and concise mathematical intro to the Univalent Foundations see https://arxiv.org/abs/1711.01477
(The example of formal rendering of torsors in Section 5, which requires a stronger mathematical background, can be omitted without much affecting the rest. )
3) In this http://philsci-archive.pitt.edu/12116/ paper (published in the IfCoLog Journal of Logic and Its Application) you find my attempt to use UF for resolving the Venus problem posed by Frege. The paper
shows a way of thinking about UF intuitively (but covers only pedestrian intuitions of a layman, not highly refined intuitions of workers in the Algebraic Geometry, which actually motivated the subject).
4) For a more systematic and more detailed intro into UF download the HoTT Book: https://homotopytypetheory.org/book/
There is no explicit Philosophy in the Book but it has nevertheless elements of an underlying philosophical agenda, which, in my view, should not be taken for granted by any critical philosophical