andrei rodin Andrei Rodin's blog about History and Philosophy of Mathematics

Contributed talk at the 25th International Conference on Types for Proofs and Programs, June 11-14, 2019, Oslo, Norway

Abstract

Slides

Related paper

Book of Abstracts indexed by Program

Invited talk at the 3d International Workshop “Formal Concept Analysis for Knowledge Discovery” (jww Serge Kovalyov)

When: Friday June 7, 2019

Where: Department of Computer Science, Higher School of Economics (Moscow, 3 Kochnovsky Proezd)

Abstract

Paper

Slides

14 мая 2019 года в Институте философии РАН в рамках проекта «Философская мастерская» состоялся круглый стол
“А.С. Есенин-Вольпин о верховенстве закона в логике, математике и общественной жизни” .

ВИДЕО:

Страница события на сайте РАН

Участники: Р.Г. Апресян, д.ф.н., главный научный сотрудник, руководитель сектора этики Института философии РАН; В.А. Лекторский, академик РАН, д.ф.н., главный научный сотрудник сектора теории познания Института философии РАН; Г.Б. Шабат, д.физ.-мат.н., профессор кафедры математики, логики и интеллектуальных систем в гуманитарной сфере РГГУ.

Модератор к.ф.н. А.В. Родин, со-модератор проф. РАН, д.ф.н. Ю.В. Синеокая.

Speaker: Andrei Rodin, Russian Academy of Sciences

When: Wednesday April 24, 2019, 7:00 – 8:30 PM.

Where: Graduate Centre CUNY, (365 5th Ave, New York, NY 10016), room 6417

Abstract:

Directed Homotopy Type theory (DHTT) is a generalization of Homotopy Type theory (HoTT) where fundamental groupoids of spaces are replaced by more general (higher) categories. Along with type formers for identity types which admit the standard HoTT interpretation in terms of invertible paths and their homotopies, DHTT comprises type formers for non-invertable homomorphisms of all levels which admit an interpreation in terms of non-invertable paths in appropriate spaces. The choice between DHTT and HoTT as foundational formal frameworks for building mathematical theories has an epistemological dimension, which concerns the epistemic significance of the invertibility condition. While HoTT and the related notion of Univalent Foundations support Mathematical Structuralism DHTT supports a more dynamic conception of Mathematics, which I shall outline in my talk. 

slides

Coming out soon in Springer with my piece on Univalent Foundations.  More details here.

ProductFlyer

 

Extra-logical proof-theoretic semantics in HoTT (abstract)

Conference Proof Theoretic Semantics: Assessments and Future Perspectives : Tübingen,  March 27-30, 2019

 

Логическая и экстра-логическая теоретико-доказательная семантика в гомотопической теории типов (slides)

Теоретический семинар Кафедры Логики СПбГУ , 7 марта 2019, начало 17:20, ауд. 167

 

 

E pluribus unum в логике и математике (abstract)

 Когда: 24 ноября 2018,начало в 11 утра

Конференция «Горизонты логического плюрализма» к юбилею Владимира Леонидовича Васюкова

Где: ВШЭ (Москва) Мясницкая 11, ауд. 508

 

 

Конструктивный аксиоматический метод и унивалентные основания математики (abstract)

Когда: 26 ноября 2018, 14:00

Где: ПОМИ (Петербургское отделение математического института им. В.А. Стеклова РАН), городской логический семинар (объявление).

Смерть Владимира Воеводского на пике его профессиональной карьеры это трагическая и невосполнимая потеря для всей мировой науки.  Начиная по крайней мере с 2006 года, когда Владимир распространил в Интернете короткую заметку с интригующим названием “О гомотопическом лямбда-исчислении” (1) его основные интеллектуальные усилия были сфокусированы на задаче построения новых оснований математики, которые Владимир предложил называть Унивалентными Основаниями. Интерес Владимира к математической логике и основаниям математики не был случайным. Опираясь на свой личный опыт  исследований на переднем крае математики, которые в 2002 году мировое математическое  сообщество оценило  высшей возможной в виде медали Филдса, Владимир видел угрозу в том, что новые математические доказательства теряют прозрачность и оказываются доступными для понимания и, тем более, для проверки лишь очень небольшому числу экспертов в той узкой области математики, к которой относится данная теорема.

То, что в такая экспертиза является ненадежной, Владимир знал на примере собственных публикаций: в частности, спустя пятнадцать лет после публикации своей совместной статьи с Михаилом Капрановым, он обнаружил в ней ошибку.  Унивалентные Основания позволяют записывать сложные математические доказательства в виде программного кода и затем проверять корректность этого кода с помощью компьютера, освобождая интеллект исследователя для решения более творческих задач. Значение Унивалентных Оснований не ограничивается решением этой прагматической задачи. Как и всякий крупный проект в области оснований математики проект построения Унивалентных Оснований ставит целый ряд логических, эпистемологических и чисто математических проблем, над которыми Владимир продолжал работать до последнего дня вместе с группой сотрудников из разных стран и университетов. Эта работа, безусловно, продолжится, и я уверен, что влияние идей Владимира в математике и вообще в науке будет только возрастать в ближайшие годы, несмотря на преждевременную смерть их автора.

Помимо чисто математической работы Владимир серьезно интересовался историей и философией своей дисциплины. Его философские взгляды на основания математики значительно отличались от современного мэйнстрима, и Владимир не делал систематических попыток их защищать за пределами математического сообщества.
Я, тем не менее, очень надеюсь, что эта важная часть наследия Воеводского также не останется в забвении и получит дальнейшее развитие.

Владимир был не только гениальным ученым, но и очень внимательным товарищем. Мы познакомились в 2012 году в Любляне и все последующие годы очень плодотворно общались – как по переписке, так и лично, когда была такая возможность. По приглашению Владимира я в начале 2015 года посещал его в Принстонском Институте: мне запомнился эпизод, когда после обеда в столовой Института, мы вдруг обнаружили, что уже час разговариваем где-то на кампусе, держа в руках подносы с грязной посудой, которые после обеда мы оба забыли поставить на нужное место.

Мне кажется, что в своих занятиях основаниями математики Владимир искал и какую-то личную точку опоры, которая могла бы позволить ему как-то совладать с тем необычным интеллектом, которым он обладал, и лучше приспособить себя к условиям и условностям человеческого общества. Переживая сегодня горе, связанное с уходом нашего гениального товарища, мы должны быть благодарны ему за все то, что он смог для нас сделать, пока оставался с нами. Прощай, Володя.

(1)  https://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/Hlambda_short_current.pdf

In addition to being a mathematician of genius Vladimir had a genuine interest to the history and philosophy of his discipline; I owe Vladimir hours of extremely tensed discussions on Euclid (Vladimir read both the Elements and the Proclus’ Commentary very carefully), Grassmann (whose writings he studied perhaps more than any other historical source). Our last short exchange in LQ in Stockholm was on Aristotle: Vladimir told me that he had big plans of studying the history of logic. Vladimir had a fantastic capacity of understanding another person’s ideas immediately following only some hints – or at least this is my personal experience with Vladimir.

We were not close friends but all our meetings and talks were always very friendly; in 2015 he was my extremely attentive host in IAS. I lost an important person in my life with Vladimir’s unexpected death. Good buy Volodya.

Пленарный доклад на конференции “Философия науки и техники в России: вызовы информационных технологий”, Вологда 2-3 июня 2017, организованная при участии РОИФН (abstract)(slides)(video – с 42й минуты и до конца записи)

Приглашенный доклад на заседании Ученого Совета Санкт-Петербургского филиала Института Истории Естествознания и Техники РАН   23 мая 2017 (презентация)(аудио)(видео)

Конструктивное знание-3: формализация теорий

NEW: Full Video

Когда: пятница 12 мая 2017 с 10 утра

Где: ИФ РАН, комната 416 (4-й этаж)

 

Описание:

Этот воркшоп – третий в серии воркшопов, организованных в рамках проекта “Логические и эпистемологические аспекты конструктивного знания” (см. первый и второй воркшопы). В этот раз фокус будет сделан на анализе различных подходов к формализации теорий. Эта проблема будет рассмотрена как с технической, так и с эпистемологической точек зрения.

 

Программа:

10:00 – 10:40

ВЛАДИМИР ШАЛАК (ИФ РАН)

Логическая компонента научных теорий

(аннотация)

 

10:40 – 11:10

СЕРГЕЙ КОВАЛЁВ (ИПУ РАН)

Представление инженерных знаний в электронно-цифровом макете сложного технического изделия

(аннотация)

 

КОФЕ

 

11:30 – 12:10

ВЛАДИМИР КРУПСКИЙ

О моделировании уверенности и знания в социальных сетях

(аннотация)

 

12:10 – 12:50

АНДРЕЙ РОДИН (ИФ РАН)

Правила или аксиомы? О двух стилях аксиоматизации.

(аннотация)

 

12:50 – 13:30

АЛЕКСАНДР ЖОЖИКАШВИЛИ (ИППИ РАН)

Теоретико-категорная формализация продукционных систем представления знаний

(аннотация)

 

 

13:30 – 15:00 – ОБЕД

 

15:00 – 15:40

ВЛАДИМИР ВАСЮКОВ (ИФ РАН)

Трансцендентальные модальности

(аннотация)

 

 

15:40 – 16:10

КОНСТАНТИН ШИШОВ (МГУ)

Семантики квантовой логики

(аннотация)

 

КОФЕ

 

16:30 – 17:10

ДАНЯ РОГОЗИН (МГУ)

Соответствие Карри-Говарда и колмогоровская сложность

(аннотация)

 

17:10 – 17:50

СЕРГЕЙ ТИТОВ (ИФРАН)

 Объяснительная сила информационно-емких исследований

(аннотация)

 

17:50 – 18:30

ЗАЛЮЧИТЕЛЬНОЕ ОБСУЖДЕНИЕ