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

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

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

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

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

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

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

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