Непротиворечивость теории категорий

[maximk]

Является ли теория категорий непротиворечивой? Если этот факт доказан, то где можно найти его доказательство?

[Lia]

Тема перемещена из форума «Математика (общие вопросы)» в форум «Помогите решить / разобраться (М)»

[arseniiv]

maximk
А вы ведь знаете, что конкретно надо понимать под непротиворечивостью теории категорий? Просто вдруг ответ напишут — а зря.

[maximk]

Нет, я не знаю, что нужно понимать под этим. До этого момента считал, что невыводимость в этой теории утверждения и его отрицания, разве нет?

[arseniiv]

А с точностью до матлогики? Подобные спрашиваемому вами доказательства будут на её языке написаны.

[ИСН]

Повернём другим боком. maximk, а какие, например, теории (ну, из более-менее известных) вообще являются непротиворечивыми?

[kp9r4d]

Мне больше интересен вопрос с третьей стороны: разве теория категорий является теорией в логическом смысле этого слова? Если у нас есть какая-нибудь $ZFC$ то мы можем определить "категорию" как объект, удовлетворяющий такому-то списку аксиом, но сама по себе она разве теория? Даже в Маклейне этого сильно не касаются, говорят что-то типа того, что если у нас есть теория $ZFC+\{\text{для каждого множества существует универсум Гротендика содержащий его}\}$ то всё что придумывается более-менее в ней формулируется (по крайней мере в "малых" версиях категорий). Я слышал что-то о таких вещах, как топосы, высшие категории и логические основания категорий, но, как я понял, это всё вещи неустоявшиеся - достижения последних 50-70 лет, и спросив об этом специалистов получим три мнения на двух человек.

[maximk]

ИСН, теория групп.
kp9r4d, то есть ответ на вопрос зависит от непротиворечивости $ZFC$?

[kp9r4d]

maximk в сообщении #1058728 писал(а):

kp9r4d, то есть ответ на вопрос зависит от непротиворечивости $ZFC$?

Может быть, я этого не говорил.
Разумеется теорию "абстрактной категории" сделать можно, достаточно ввести пару предикатов типа "х - стрелка", "х - объект" и выписать все аксиомы категории (коих 3 штуки). И такая теория будет, как минимум, непротиворечива относительно $ZFC$ (из $Con(ZFC)$ будет выводится $Con(CT)$) как минимум потому, что она имеет модель.
Но существа живущие внутри этой теории - ничего о категориях не знают, они знают только об объектах и о стрелках, то есть даже "функтор" - сущность вне их мира, а под "теорией категорий" хотелось бы понимать нечто очень универсальное, вроде теории множеств, позволяющее работать сразу с несколькими категориями и определять новые. И вот для этого второго случая адекватной общепринятой аксиоматики (вроде бы) пока ещё нет, поэтому вопрос бессмысленен без соответствующих уточнений.
С другой же стороны, мне кажется что такие понятия как "теория" и "непротиворечивость" вы понимаете ещё превратнее, чем я :3 Вот например

maximk в сообщении #1058728 писал(а):

ИСН, теория групп.

А почему она непротиворечива?

[maximk]

kp9r4d, признаюсь, что не владею информацией. Буду вам благодарен, если вы мне это и объясните и поправите меня

[kp9r4d]

maximk
Ну, чтобы объяснить всё по науке нужен семестровый курс логики, в одном сообщении я его вряд ли напишу :3 Однако если по рабоче-крестьянски, то, как я понимаю, ситуация такая (если что, знающие люди поправят). Под "теорией групп" понимают, опять же, теорию "абстрактной группы" - то есть там мы можем говорить об элементах группы, но не можем говорить о группах вообще. И разумеется, из непротиворечивости $ZFC$ следует и непротиворечивость теории групп. Непротиворечивость - это свойство почти всегда относительное, мы не можем говорить о "непротиворечивости вообще", а можем говорить только, что "из непротиворечивости А выводится непротиворечивость В". Однако бывают случаи, когда, на самом деле, можем, это очень редкие случаи - когда из аксиом выводится (чисто синтаксически) любое утверждение, либо его отрицание, такие теории называются "полными" и вот теория групп - она не такая.
То есть говорить о том, что "теория групп (сама по себе) непротиворечива" - неаккуратно как минимум, а как максимум, неправильно. Таки дела вот.

[maximk]

kp9r4d, спасибо. Но есть вопросик, почему вы поставили тире в предложении, где речь шла о непротиворечивости и полноте, ведь полнота не влечет непротиворечивость? Или вы к тому, что для некоторых теория есть процедура, которая для каждого утверждения теории дает значение истинности или ложности и таким образом выясняя, что нет двух противоречащих утверждений?
А как вы думаете, оправдан ли метод доказательства непротиворечивости теории путем построеня модели? Это оправдывается тем, что если бы модель была противоречива, то и теория была бы таковой же? Нет ли у вас сомнений в этом принципе?

[kp9r4d]

maximk в сообщении #1058806 писал(а):

Но есть вопросик, почему вы поставили тире в предложении, где речь шла о непротиворечивости и полноте, ведь полнота не влечет непротиворечивость?

Имелась в виду "непротиворечивая полнота". Вообще тут есть некоторая проблема с терминпологией. "Полнота", "непротиворечивость" и "теория" - не слишком фиксированные термины, и меняются от учебника к учебнику, см. например [1].

maximk в сообщении #1058806 писал(а):

Или вы к тому, что для некоторых теория есть процедура, которая для каждого утверждения теории дает значение истинности или ложности и таким образом выясняя, что нет двух противоречащих утверждений?

Нет, я точно не к этому.

maximk в сообщении #1058806 писал(а):

А как вы думаете, оправдан ли метод доказательства непротиворечивости теории путем построеня модели? Это оправдывается тем, что если бы модель была противоречива, то и теория была бы таковой же? Нет ли у вас сомнений в этом принципе?

Это оправдывается основной теоремой теории моделей - любая теория либо противоречива, либо имеет модель, что такое "противоречивая модель" не понятно, модель - это просто множесто, как множество может быть противоречивым? Этот результат верен настолько же, насколько мы верим в аксиомы теории множеств (что не очень приятно, так как средства не финитные и, вроде бы, финитным языком не формализуются) и в правила вывода.

[Olivka]

(Оффтоп)

kp9r4d в сообщении #1058916 писал(а):

модель - это просто множество

Множество чего? Вот мне нигде не попадалось простое, понятное объяснение, что такое модель.

[arseniiv]

Множество чего-нибудь. Вместе с определёнными на нём операциями и отношениями, поставленными в соответствие функциональным и предикатным символам данного языка первого порядка, что даёт находить истинностные значения замкнутых формул этого языка. Такое хорошее множество зовётся интерпретацией*. Если все формулы теории первого порядка истинны в данной интерпретации, последняя зовётся моделью [теории]. Теория здесь — это множество формул данного языка, замкнутое относительно выводимости.

* Соответствие символов операциям/отношениям можно выкинуть, считая те соответствующими, если они идут в одинаковом порядке. Тогда интерпретация — это просто алгебраическая система.

Вообще, чтение литературы устраняет пробелы такого толка, т. к. это уровень определений. Как сказал kp9r4d, в названиях и смысле терминов бывают небольшие отличия, но наборы из разных источников переводятся друг в друга с полпинка. Если не переводятся, стоит задуматься о какой-нибудь другой области математики.