Исследовательская группа

Лаборатория языковых инструментов

Введение в Metamath

October 14

Основная идея проекта Metamath - построить формализованное здание математики, которое с одной стороны может быть проверено автоматически на компьютере, а с другой стороны "вручную" разобрано человеком в привычной ему нотации. В определенном смысле это Principia Mathematica. Какие идеи стоят за Metamath?

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

Далее будем постепенно отходить от основ и двигаться в сторону все более абстрактных конструкций: отношений, функций, ординалов, "обычных" чисел, структур. Напоследок покажем, как Metamath "справляется" с теорией категорий.


Докладчик: Кирилл Смирнов.