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


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

24 октября 2018 г. состоялось сорок восьмое заседание семинара «Формальная философия». А. В. Родин (старший научный сотрудник Международной лаборатории логики, лингвистики и формальной философии НИУ ВШЭ) выступил с докладом "Geometrical Logic versus Logical Geometry: the Case of Univalent Foundations".

"Геометрическая логика vs логическая геометрия: случай унивалентных оснований"

В докладе были представлены различия между геометрической логикой илогической геометрией в исторической перспективе и в современныхисследованиях оснований математики. Доклад начался с представления логической геометрии. Логическаягеометрия является геометрической теорией, построенной на эксплицитно заданных логических основаниях. В качестве примеров логической геометрии были рассмотрены исследование аксиоматического метода Евклида Д. Гильбертом в "Основаниях геометрии"; статья "What iselementary geometry" и книга "Введение в методологию дедуктивных наук"
А. Тарского. Далее последовало обращение к работам, посвященным геометрической логике. Геометрическая логика в широком смысле понимается как работа с логическими теориями и системами на основании геометрии. В докладе были упомянуты такие примеры геометрической логики, как топологическая семантика для модальной логики, формализация топологии, теория топосов, модальная логика пространства. В заключении доклада был представлен современный подход к проблемам связи математического и логического знания, границ логики. Этот подход к решению проблемы оснований математики, разработке систем проверки доказательств теорем, называемый унивалентные основания,основывается на теории гомотопий, теории типов Мартина-Лёфа и теории категорий.


"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