• A
  • A
  • A
  • АБВ
  • АБВ
  • АБВ
  • А
  • А
  • А
  • А
  • А
Обычная версия сайта

Мероприятия

Формальная философия-48: доклад Андрея Родина

Мероприятие завершено

24 октября в 18.30 состоится 48-е заседание научно-теоретического семинара  «Формальная философия».

Андрей Вячеславович Родин

старший научный сотрудник 
Международной лаборатории логики, лингвистики
 и формальной философии (ЛогЛинФФ) НИУ ВШЭ



выступит с докладом:

«Geometrical Logic versus Logical Geometry: the Case of Univalent Foundations»

Abstract:
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. 

 Bibliography:

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

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 reader.