July 1st, 2017

ДР Цертуса 2011

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

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

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

Так можно, например, выяснить, что 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.