Когда мы говорим про использование теории категорий в качестве оснований математики, мы имеем в веду не аксиоматическую теорию первого порядка, моделями которой являются категории, а нечто другое. Как аксоиматическая теория групп почти не позволяет никак работать с этими самыми группами (её язык слишко скуден, в нём нет выражения “пара элементов группы”, “список элементов группы”, “конечное подмножество элементов группы”, нет арифметики и соответственно возможности сказать “n элементов группы”), так и теория “одной категории” в качестве основания математики ни на что не годна.
То что понимается под standalone categorical foundations - это несколько размазанное понятие, тут есть две идеи. Либо это аксиоматическая теория категории всех категорий Cat, либо это аксоиматическая теория категории всех множеств Set. В обоих случаях аксиомы гарантируют, что внутри Cat/внутри Set живёт арифметика и внутренние категории моделей всевозможных других теорий - категория всех групп, категория всех колец ну и т.д.
Подход с аксиоматической теорией категории всех категорий пока недоразвит, т.к. категория всех (локально малых) категорий вообще-то нормально описывается как 2-категория, а не как категория, ну и там двойкой не ограничешься, надо для всех `n`. Короче, это ещё long way to go.
Подход с аксиоматической теорией категории множеств довольно развит. Это не поверх теории множеств, это альтернатива теории множеств, реально существующая. https://ncatlab.org/nlab/show/fully+formal+ETCS
Мы берём ту самую аксиоматическую теорию категорий и добавляем в неё аксиомы о существовании всех конечных пределов и классификатора подобъектов. Такая категория называется элементарным топосом. Это очень хороший класс категорий. Такая структура необходима, чтобы можно было проинтерпретировать всякую теорию высшего порядка (т.е. не только теорию групп, но и теорию топологических пространств), и достаточна для того чтобы истинность во всех моделях совпадала с доказуемостью (Awodey, Butz “Topological Completeness for Higher-Order Logic”, 2000). Затем добавляют аксиому, гарантирующую существование объекта натуральных чисел (вместе с ним забесплатно приходят кортежи, списки, деревья и конечные множества). Такие штуковины (W-топосы) всё ещё дают адекватную семантику для всевозможных теорий первого и высших порядков, и арифметику вместе с комбинаторными объектами.
Хорошо бы на этом и остановиться, но к сожалению структуры топоса недостаточно, чтобы заниматься математикой полноценно, и поэтому приходится вводить дополнительные требования - well-pointedness и тот или иной вариант аксиомы выбора. И это плохо, потому что получающийся класс категорий уже не обладает потребной универсальностью. [...]
Когда мы говорим про использование теории категорий в качестве оснований математики, мы имеем в веду не аксиоматическую теорию первого порядка, моделями которой являются категории, а нечто другое. Как аксоиматическая теория групп почти не позволяет никак работать с этими самыми группами (её язык слишко скуден, в нём нет выражения “пара элементов группы”, “список элементов группы”, “конечное подмножество элементов группы”, нет арифметики и соответственно возможности сказать “n элементов группы”), так и теория “одной категории” в качестве основания математики ни на что не годна.
То что понимается под standalone categorical foundations - это несколько размазанное понятие, тут есть две идеи. Либо это аксиоматическая теория категории всех категорий Cat, либо это аксоиматическая теория категории всех множеств Set. В обоих случаях аксиомы гарантируют, что внутри Cat/внутри Set живёт арифметика и внутренние категории моделей всевозможных других теорий - категория всех групп, категория всех колец ну и т.д.
Подход с аксиоматической теорией категории всех категорий пока недоразвит, т.к. категория всех (локально малых) категорий вообще-то нормально описывается как 2-категория, а не как категория, ну и там двойкой не ограничешься, надо для всех `n`. Короче, это ещё long way to go.
Подход с аксиоматической теорией категории множеств довольно развит. Это не поверх теории множеств, это альтернатива теории множеств, реально существующая. https://ncatlab.org/nlab/show/fully+formal+ETCS
Мы берём ту самую аксиоматическую теорию категорий и добавляем в неё аксиомы о существовании всех конечных пределов и классификатора подобъектов. Такая категория называется элементарным топосом. Это очень хороший класс категорий. Такая структура необходима, чтобы можно было проинтерпретировать всякую теорию высшего порядка (т.е. не только теорию групп, но и теорию топологических пространств), и достаточна для того чтобы истинность во всех моделях совпадала с доказуемостью (Awodey, Butz “Topological Completeness for Higher-Order Logic”, 2000). Затем добавляют аксиому, гарантирующую существование объекта натуральных чисел (вместе с ним забесплатно приходят кортежи, списки, деревья и конечные множества). Такие штуковины (W-топосы) всё ещё дают адекватную семантику для всевозможных теорий первого и высших порядков, и арифметику вместе с комбинаторными объектами.
Хорошо бы на этом и остановиться, но к сожалению структуры топоса недостаточно, чтобы заниматься математикой полноценно, и поэтому приходится вводить дополнительные требования - well-pointedness и тот или иной вариант аксиомы выбора. И это плохо, потому что получающийся класс категорий уже не обладает потребной универсальностью. [...]
Reply
Leave a comment