Место и время: Институт Философии РАН (Москва, Волхонка 14), сектор логики, четверг 14 марта в 3 часа
Название: Генетический аксиоматический метод, изоморфизм Карри-Ховарда и “унивалентные основания” Воеводского.
Абстракт:
В.А. Смирнов вслед за Гильбертом и Бернайсом указывает на тот факт, что формальный аксиоматический метод сам по себе является недостаточным для построения научных теорий (и соответствующих мета-теорий) и должен быть дополнен более традиционным генетическим методом. В своем докладе я сначала демонстрирую понятие генетического метода на примере “Начал” Евклида, а затем обсуждаю современные версии генетического метода: конструктивную теорию типов Мартина-Лёфа, ее связь с изоморфизмом Карри-Ховарда, гомотопическую модель этой теории (использующую язык теории категорий) и, наконец, “унивалентные основания математики” Воеводского, в которых эта гомотопическая модель используется в качестве содержательного основания всей математики.
Мой тезис состоит в том, что современное понятие генетического метода следует отождествить с понятием аксиоматического метода как такового, а гильбертово понятие “формального” или “экзистенциального” аксиоматического метода нужно рассматривать только в качестве специального приема (который, как мы сейчас знаем, далеко не так эффективен, как в свое время думал Гильберт). Формулирую это утверждение в виде слогана: Вперед к Евклиду!