Понедельник, 26 ноября, ПОМИ РАН, ауд. 106. Начало в 14:00.
Докладчик: А.В. Родин (Институт философии РАН).
Тема: Конструктивный аксиоматический метод и унивалентные основания математики.
Abstract
Современное понятие аксиоматического метода восходит к работам Давида Гильберта по основаниям математики в первой половине 20-го века. Свою новую версию аксиоматического метода Гильберт называл «экзистенциальным» аксиоматическим методом и отличал её от более традиционного метода построения математических теорий, который он называл «генетическим» или «конструктивным». Отличие конструктивного метода от экзистенциального состоит в том, что в первом случае используются правила для конструирования непропозициональных объектов из данных примитивных объектов, тогда как во втором случае в каждой интерпретации формальной теории объекты предполагаются фиксированными, и теория содержит только логические правила, с помощью которых из одних пропозиций выводятся другие пропозиции. Унивалентные основания математики представляют собой основанную на теории типов формальную схему для генетического конструирования математических теорий, в рамках которой логические правила вывода оказываются частным случаем более общих правил, которые применяются также и к непропозициональным объектам. Такой новый подход в основаниях математики эффективно решает задачу компьютерной проверки нетривиальных математических доказательств, а также устанавливает более тесную связь между логическими и внелогическими элементами математического рассуждения, чем стандартный подход.
Приложение
