Одновалентные фундаменты
Унивалентные основы — это подход к основам математики , при котором математические структуры строятся из объектов, называемых типами . Типы в однолистных основаниях не соответствуют в точности ничему в теоретико-множественных основаниях, но их можно рассматривать как пространства с одинаковыми типами, соответствующими гомотопически эквивалентным пространствам, и с равными элементами типа, соответствующими точкам пространства, соединенным путем. . Однозначные основания вдохновлены как старыми платоническими идеями Германа Грассмана и Георга Кантора , так и « категорической » математикой в стиле Александра Гротендика . Унивалентные основы отходят от использования классической логики предикатов в качестве базовой формальной системы вывода (хотя также совместимы с ней) , заменяя ее на данный момент версией теории типов Мартина-Лёфа . Разработка однолистных оснований тесно связана с развитием теории гомотопических типов .
Однозначные основания совместимы со структурализмом , если принято соответствующее (т. е. категориальное) понятие математической структуры. [1]
История [ править ]
Основные идеи одновалентных оснований были сформулированы Владимиром Воеводским в период с 2006 по 2009 год. Единственным источником информации о философских связях между одновалентными основаниями и более ранними идеями являются лекции Воеводского Бернейса 2014 года. [2] Название «однолистность» принадлежит Воеводскому. [3] [4] Более подробное обсуждение истории некоторых идей, которые способствуют нынешнему состоянию унивалентных оснований, можно найти на странице теории гомотопических типов ( HoTT ).
Фундаментальной характеристикой однолистных оснований является то, что они — в сочетании с теорией типов Мартина-Лёфа ( MLTT ) — обеспечивают практическую систему формализации современной математики. Значительный объем математических вычислений был формализован с использованием этой системы и современных помощников по доказательству, таких как Coq и Agda . Первую такую библиотеку под названием «Фундаменты» создал Владимир Воеводский в 2010 году. [5] Теперь Foundations является частью более крупной разработки нескольких авторов под названием UniMath . [6] Фонды также вдохновили другие библиотеки формализованной математики, такие как библиотека HoTT Coq. [7] и библиотека HoTT Agda, [8] которые развивали одновалентные идеи в новых направлениях.
Важной вехой для универсальных фондов стало на семинаре Бурбаки. выступление Тьерри Коканда [9] в июне 2014 года.
Основные понятия [ править ]
Унивалентные основания возникли в результате некоторых попыток создания оснований математики на основе теории высших категорий . Ближе всего к одновалентным основаниям из ранних идей были идеи, которые Майкл Маккай называет « логикой первого порядка с зависимыми сортами» (FOLDS). [10] Основное различие между однолистными основаниями и основаниями, представленными Маккаем, заключается в признании того, что «аналоги множеств более высоких измерений» соответствуют бесконечным группоидам и что категории следует рассматривать как аналоги частично упорядоченных множеств более высоких измерений .
Первоначально одновалентные основы были разработаны Владимиром Воеводским с целью дать возможность тем, кто работает в области классической чистой математики, использовать компьютеры для проверки своих теорем и построений. Тот факт, что унивалентные основания по своей сути конструктивны, был обнаружен в процессе написания библиотеки Foundations (теперь часть UniMath). В настоящее время в однолистных основаниях классическая математика рассматривается как «ретракт» конструктивной математики , т. е. классическая математика является одновременно подмножеством конструктивной математики, состоящим из тех теорем и конструкций, которые используют закон исключенного третьего в качестве своего предположения и «частное» конструктивной математики по отношению эквивалентности по модулю аксиомы исключенного третьего.
В системе формализации однолистных оснований, основанной на теории типов Мартина-Лёфа и ее потомках, таких как исчисление индуктивных конструкций , аналоги множеств более высоких размерностей представлены типами. Коллекция типов стратифицируется понятием h-уровня (или уровня гомотопии ). [11]
Типы h-уровня 0 соответствуют одноточечному типу. Их еще называют сжимаемыми типами.
Типы h-уровня 1 — это те, в которых любые два элемента равны. Такие типы называются «предложениями» в однолистных основаниях. [11] Определение пропозиций в терминах h-уровня согласуется с определением, предложенным ранее Аводи и Бауэром. [12] Итак, хотя все предложения являются типами, не все типы являются предложениями. Быть предложением — это свойство типа, требующее доказательства. Например, первая фундаментальная конструкция в однолистных фундаментах называется iscontr . Это функция от типа к типу. Если X — тип, то iscontr X — это тип, который имеет объект тогда и только тогда, когда X сжимаем. Это теорема (которая в библиотеке UniMath называется isapropiscontr ), что для любого X тип iscontr X имеет h-уровень 1 и, следовательно, быть сжимаемым типом является свойством. Это различие между свойствами, которые засвидетельствованы объектами типов h-уровня 1, и структурами, которые засвидетельствованы объектами типов более высоких h-уровней, очень важно в унивалентных основаниях.
Типы h-уровня 2 называются множествами. [11] Это теорема о том, что тип натуральных чисел имеет h-уровень 2 ( isasetnat в UniMath). Создатели однолистных основ утверждают, что однолистная формализация множеств в теории типов Мартина-Лёфа является лучшей доступной в настоящее время средой для формальных рассуждений обо всех аспектах теоретико-множественной математики, как конструктивной, так и классической. [13]
Категории определяются (см. библиотеку RezkCompletion в UniMath) как типы h-уровня 3 с дополнительной структурой, которая очень похожа на структуру типов h-уровня 2, определяющую частично упорядоченные множества. Теория категорий в однолистных основаниях несколько отличается и богаче, чем теория категорий в теоретико-множественном мире, причем ключевым новым различием является различие между предкатегориями и категориями. [14]
Изложение основных идей одновалентных оснований и их связи с конструктивной математикой можно найти в учебнике Тьерри Коканда. [а] Презентацию основных идей с точки зрения классической математики можно найти в обзоре Альваро Пелайо и Майкла Уоррена за 2014 год. [17] а также во введении [18] Дэниел Грейсон. См. также: Владимир Воеводский (2014). [19]
Текущие события [ править ]
Отчет о построении Воеводским одновалентной модели теории типов Мартина-Лёфа со значениями в симплициальных множествах Кана можно найти в статье Криса Капулькина, Питера ЛеФану Ламсдейна и Владимира Воеводского. [20] Однолистные модели со значениями в категориях обратных диаграмм симплициальных множеств были построены Майклом Шульманом . [21] Эти модели показали, что аксиома однолистности независима от аксиомы исключенной средней для высказываний.
Модель Воеводского считается неконструктивной, поскольку она использует аксиому выбора неустранимым образом .
Проблема поиска конструктивной интерпретации правил теории типов Мартина-Лёфа, дополнительно удовлетворяющей аксиоме однолистности. [б] и каноничность натуральных чисел остается открытой. Частичное решение изложено в статье Марка Безема , Тьерри Коканда и Саймона Хубера. [23] при этом ключевой остающейся проблемой являются вычислительные свойства элиминатора для типов идентичности. Идеи данной статьи в настоящее время развиваются в нескольких направлениях, включая развитие теории кубического типа. [24]
Новые направления [ править ]
Большая часть работ по формализации математики в рамках унивалентных оснований ведется с использованием различных подсистем и расширений Исчисления индуктивных конструкций (ИСК).
Существуют три стандартные задачи, решение которых, несмотря на множество попыток, не удалось построить с помощью CIC:
- Определить типы полусимплициальных типов, H-типов или структур (infty,1)-категорий типов.
- Расширить CIC системой управления юниверсами, которая позволит реализовать правила изменения размера.
- Разработать конструктивный вариант аксиомы одновалентности. [25]
Эти нерешенные проблемы указывают на то, что, хотя CIC является хорошей системой для начальной фазы разработки унивалентных основ, переход к использованию компьютерных помощников в работе над более сложными ее аспектами потребует разработки нового поколения формальной дедукции. и вычислительные системы.
См. также [ править ]
Примечания [ править ]
Ссылки [ править ]
- ^ Аводи, Стив (2014). «Структурализм, инвариантность и одновалентность» (PDF) . Философия Математика . 22 (1): 1–11. CiteSeerX 10.1.1.691.8113 . дои : 10.1093/philmat/nkt030 .
- ^ Воеводский Владимир (9–10 сентября 2014 г.). «Основы математики — их прошлое, настоящее и будущее». Лекции Пола Бернейса 2014 года . ETH Цюрих. См. пункт 11 на «Воеводских лекциях».
- ^ аксиома однолистности в nLab
- ^ Мартин Хетцель Эскардо (18 октября 2018 г.) Самостоятельная, краткая и полная формулировка аксиомы одновалентности Воеводского.
- ^ Библиотеку Foundations см. https://github.com/vladimirias/Foundations.
- ^ Библиотека UniMath, см. https://github.com/UniMath/UniMath.
- ^ Библиотеку HoTT Coq, см. https://github.com/HoTT/HoTT.
- ^ Библиотека HoTT Agda, см. https://github.com/HoTT/HoTT-Agda.
- ^ Коканда Бурбаки Лекционный материал и видео
- ^ Маккай, М. (1995). «Логика первого порядка с зависимыми видами с приложениями к теории категорий» (PDF) . СКЛАДКИ .
- ↑ Перейти обратно: Перейти обратно: а б с См. Пелайо и Уоррен 2014 , стр. 611
- ^ Аводи, Стивен; Бауэр, Андрей (2004). «Предложения как [типы]» . Дж. Лог. Вычислить . 14 (4): 447–471. дои : 10.1093/logcom/14.4.447 .
- ↑ Воеводский 2014 , Лекция 3, слайд 11.
- ^ См. Аренс, Бенедикт; Капулькин, Крис; Шульман, Майкл (2015). «Одновалентные категории и пополнение Резка». Математические структуры в информатике . 25 (5): 1010–1039. arXiv : 1303.0584 . дои : 10.1017/S0960129514000486 . S2CID 1135785 .
- ^ Кулинария (2014), часть 1.
- ^ Кулинария (2014), часть 2.
- ^ Пелайо, Альваро; Уоррен, Майкл А. (2014). «Теория гомотопических типов и однолистные основания Воеводского» . Бюллетень Американского математического общества . 51 (4): 597–648. arXiv : 1210.5658 . дои : 10.1090/S0273-0979-2014-01456-9 .
- ^ Грейсон, Дэниел Р. (2018). «Введение в однолистные основания для математиков» . Бюллетень Американского математического общества . 55 (4): 427–450. arXiv : 1711.01477 . дои : 10.1090/bull/1616 . S2CID 32293255 .
- ^ Владимир Воеводский (2014) Экспериментальная библиотека однолистной формализации математики
- ^ Капулькин, Крис; Ламсдейн, Питер ЛеФану; Воеводский, Владимир (2012). «Симплициальная модель одновалентных оснований». arXiv : 1211.2851 [ math.LO ].
- ^ Шульман, Майкл (2015). «Онивалентность обратных диаграмм и гомотопическая каноничность». Математические структуры в информатике . 25 (5): 1203–1277. arXiv : 1203.3253 . дои : 10.1017/S0960129514000565 . S2CID 13595170 .
- ^ Мартин Хетцель Эскардо (18 октября 2018 г.) Самостоятельная, краткая и полная формулировка аксиомы одновалентности Воеводского.
- ^ Безем, М.; Коканд, Т.; Хубер, С. «Модель теории типов в кубических множествах» (PDF) .
- ^ Альтенкирх, Торстен ; Капоши, Амбрус, Синтаксис теории кубических типов (PDF)
- ^ В. Воеводский, Проект Uniвалентных фондов (модифицированная версия заявки на грант ННФ), с. 9
Внешние ссылки [ править ]
Словарное определение слова «унивалент» в Викисловаре
- Библиотеки формализованной математики