Alexander Kuklev (akuklev) wrote,
Alexander Kuklev
akuklev

Categories:

Теоретико-множественные основания теорката

На протяжении 20-го века основным языком классической математики была система NBG (von Neumann-Gödel-Bernays). Теоретико-множественная часть системы NBG называется теорией множеств Цермело-Френкеля с аксиомой выбора (ZFC), разница между ними в том, что на языке ZFC можно говорить только о множествах, и нету грамматического оборота, позволяющего сказать, например, "для всех групп G". А вот NBG это система, где можно определять классы, например всех множеств Set, всех групп Grp, всех колец Rng, при этом она является консервативным расширением ZFC, т.е. все вещи, которые в ней можно доказать "для всех групп Grp" это в точности те же вещи, которые можно доказать про группы в ZFC. Конечно же на языке NBG можно говорить и о таких алгебраических структурах как категории, о классе Cat множеств со структурой категории.

Однако в Cat не входит "категория всех групп", т.к. Grp не множество, я в Cat входят только множества со структурой категории. Зато мы можем отдельно рассматривать два разных понятия,
1) конкретные категории: Классы со структурой категории: Grp, Rng,..
2) малые категории: элементы Cat

На практике от этого получается большая беда, для малых категорий мы можем доказывать общие результаты, скажем "для всякой категории С верно то-то" и производить общие построения, "для всякой категории C мы можем построить Скелет C, Нерв C" и т.д. Но применить эти результаты к большим конкретным категориям навроде Grp мы вообще говоря не можем.

В поисках решения этого вопроса Гротендик придумал понятие иерархии вселенных. Вселенная (Гротендика) это такое множество U, очень похожее на класс всех множеств Set (похожесть выражается в замкнутости относительно базовых тайп-формеров, см. http://en.wikipedia.org/wiki/Grothendieck_universe), но без требования что все другие множества в него входят, в частности U ∉ U. Вместо этого требуется, чтобы для каждого множества s ∈ Set существовала какая-нибудь вселенная U ∋ с. В частности, это означает, что для начиная с любой вселенной U можно построить иерархию U ∈ U' ∈ U'' ∈ ···.
Дальше вместо того чтобы что-то доказывать для (больших) конкретных категорий Grp, Rng и т.п., проводят доказательства для их "усечённых до U" подкатегорий GrpU, RngU. Жить так безусловно можно. Но таскать за собой индексы U в каждой формуле, а впереди каждого высказывания писать "для любой достаточно большой вселенной U" муторно и неэлегантно. (Хотя в Agda так сейчас и живут!)

Решение этого вопроса предлагает теория множеств (strong) ZFC/s Соломона Фефермана: это обычная ZFC/NBG, дополненная постулатом о существовании как минимум одной вселенной Гротендика и схемой генерализации: если мы доказали высказывание pU усечённое до той или иной вселенной U, причём U входит в высказывание только на уровне типов (т.е. связывает свободные переменные), но не термов (это называется proof irrelevance), то автоматически вернен неусечённый вариант p. Отметим, что отдельно постулировать иерархию вселенных не нужно, из определения вселенной и схемы генерализации автоматически следует, что для каждого s ∈ Set существует какая-нибудь вселенная U ∋ с.

Не смотря на то, что сам Феферман недоволен результатом и последние сорок лет периодически возвращается к вопросу о том, как бы вообще обойтись без понятия вселенной при формализации теорката, сами категорные теоретики вполне довольны этим подходом, см. https://golem.ph.utexas.edu/category/2009/11/feferman_set_theory.html, а вопрос детальной работы со вселенными Гротендика, как выяснилось, имеет полезные прикладные стороны как в логике (в отросли интуиционистских теорий типов), так и за её пределами (inter-universal Teichmüller Theory).

Мне же этот вопрос интересен в смысле того, как обращаться со вселенными в функциональных языках программирования и Theorem Prover'ах на базе теорий типов. Думается мне, что будущее за подходом Фефермана, а не за постулированием иерархий вселенных в явном виде.
Tags: fprog
Subscribe

  • (no subject)

    Встретил фотографию толпы футбольных фанатов, и она меня скорее напугала, у меня уж точно нет желания быть там среди них. Но внезапно я понял, что…

  • Прогресс

    Десять дней назад, вторая ступень SpaceX'овского корабля Starship своим ходом слетала своим ходом на десять километров вверх, и усмепшно приземлилась…

  • О водосбережении

    Как известно, питьевая вода во многих странах дефицитный ресурс. И даже в дождливой Германии летом иногда случаются засухи, в результате которых она…

  • Post a new comment

    Error

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 8 comments