• A
  • A
  • A
  • ABC
  • ABC
  • ABC
  • А
  • А
  • А
  • А
  • А
Regular version of the site

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


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

3) 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