Alexander Kuklev (akuklev) wrote,
Alexander Kuklev
akuklev

Categories:

Снова про теорию множеств

Извините, убрал прошлые несколько постов про теорию множеств под глаз; я просто сказать несколько не то хотел. Если начинать с длинных введений и исторических экскурсов, легко случайно уйти не туда. Так что давайте сразу для тех, кто в теме.

Стандартную теорию множеств можно аксиоматизировать очень разными способами. Аксиоматика Цермело-Френкеля — прагматичный вариант аксиоматики: прямолинейный, бесхитросный, операционный, комбинаторный. Никаких туманных философий, просто методы конструирования множеств: пустое множество, пара, индуктивное порождение, фильтрация и замена, множество всех подмножеств, объединение. Сверх того только аксиома, определяющая что такое равенство, схема индукции (= аксиома о фундированности), да аксиома выбора опцинально. Такой прагматичный подход удобен для анализа самой теории: можно доказать независимость аксиом друг от друга, а потом убирать аксиомы по одной или заменять более слабые, и смотреть стала ли теория слабее, и, если да, не эквивалентна какой-нибудь другой симпатичной теории.

Так можно, например, выяснить, что ZFC (с аксиомой выбора), ZF (без аксиомы выбора, но с исключённым третьим) и IZF (без исключённого третьего) эквиконсистентны. Т.е. слабейшая из них (IZF) непротиворечива, то непротиворечива и сильнейшая (ZFC). Можно выделить конструктивную версию CZF, которая при добавлении исключённого третьего или аксиомы выбора немедленно превращается в ZF или ZFC соответственно, однако если ничего не добавлять — конструктивная теория, непротиворечивость которой можно обосновать вычислительной интерпретацией и комбинаторно. А слегка усиленный вариант этой теории, минимальный пригодный для рассуждений о вещественных числах (CZF + Full Separation) оказывается эквиконсистентен арифметике второго порядка, и соответственно его непротиворечивость можно обосновать вычислительной интерпретацией (System F). С другой стороны, такие теории удобно усиливать для нужд теорий, не вписывающихся в рамки ZF(C): теории категорий и категорной алгебраической геометрии. Наиболее распространённые расширения — теория множеств TG Тарского-Гротендика и ещё более сильная (и гораздо более элегантная!) теория ZMC/S Фефермана-Шульмана ("ZFC с сильной рефлексией"), которой достаточно для всех известных на данный момент человечеству нужд теории категорий и всей остальной содержательной математики.

Слабой стороной прагматичного подхода как с точки зрения практического удобства, так и с онтологической точки зрения, является то, что всякие штуковины вроде "категории всех множеств", "категории всех групп" и т.д. существуют только “на словах”, вне самой теории множеств, на метатеоретическом уровне, если угодно. На языке теории мы можем записать высказывание “x — группа” и “y — гомоморфизм групп”, но мы не можем из этих гаджетов собрать внутритеоретический объект “категория всех групп”. В теориях с рефлексией, навроде ZMC/S, мы можем собрать внутритеоретический объект, который ведёт себя по построению неотличимо от категории всех групп, но _не саму категорию всех групп_.

Однако есть и другой подход к аксиоматизации — не прагматичный, а философский, когда имеющиеся методы формирования множеств выводятся из каких-то принципов “максимальной свободы, ещё не приводящей к парадоксам”. Тут есть два подхода:
— более распространённый «Limitation of Size» Кантора-фон Неймана-Гёделя (“всё то множество, что неравномощно универсуму”), симпатичный тем, что там из элегантного принципа следует аксиома выбора (в очень сильной форме) и все остальные способы конструирования множеств ZFC, кроме пары, множества всех подмножеств и индуктивного порождения, и
— более интересный «Bottom-up generation» Аккерманна, из которого следуют вообще все способы порождения множеств ZF, но не следует аксиома выбора.

Обе эти теории очень хороши ещё и тем, что в соответствующих теориях можно говорить не только о множествах, но и о "больших" классах навроде категории всех множеств; в частности один из вариантов теории Аккермана, ARC (см. F.A. Muller, “Sets, classes, and categories” и ревью этой статьи MR1851712 за авторством Andreas Blass) эквиконсистентен ZFC и консервативен над нею (т.е. в отношении множеств в них верны одни и те же высказывания) позволяет говорить не только о таких классах, как "категория всех групп“, но и о функторах между такими категориями, естественных преобразованиях между такими функторами и проч. И это при том, что в теории всего четыре очень естественных аксиомы, и не постулируется вообще никаких бесконечных множеств, операций индуктивного порождения, множеств всех подмножеств, объединений и замен. Всё бесплатно следует из общих принципов. Кроме аксиомы выбора.

Очень хочется выработать консервативное расширение ZMC/S в стиле теории множеств Аккерманна, т.е. чтобы там всё работало так же как в ZMC/S, только о больших категориях можно было бы говорить на языке самой теории, а не только снаружи, и аксиомы были элегантные и минималистичные. Пока этого никто не сделал, и сделать это крайне непросто (а может быть, и вообще невозможно). Но прежде чем перейти в XXI-й век и начать использовать в качестве языка математики HoTT — внутренний язык (т.е. "наименьший общий знаменатель") элементарных высших топосов, нужно закончить век XX-ый: элегантно кодифицировать вариант теории множеств, необходимый и достаточный для математики XX-го века.

P.S. В комментариях к предыдущим постам про теорию множеств меня спрашивали, нет ли какого формального языка навроде языков программирования, только для теории множеств, чтобы было точно понятно, что можно делать, а что нельзя. Разумеется, есть: https://en.wikipedia.org/wiki/Mizar_system, система записи и автоматической проверки доказательств на базе теории множеств TG (Тарского-Гротендика), при желании можно оставаться в рамках ZFC или ZFC. Но там внутре не только чистая теория множеств, но и специальный хитрый синтаксический сахар, чтобы можно было говорить о классах, категориях и прочем. Если бы Мизар (и //metamath.org) делали сейчас, а не 40 лет назад, наверное бы использовали ZMC/S вместо TG.
Subscribe

  • Прогресс

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

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

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

  • 36

    Традиционный деньрожденный пост. Год выдался необычный. :)

  • 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.
  • 24 comments

  • Прогресс

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

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

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

  • 36

    Традиционный деньрожденный пост. Год выдался необычный. :)