Не zf(c)шные подходы к математике

[EminentVictorians]

Какие существуют подходы строить математику, чтобы не ZF(C)? Лучше даже вообще не теоретико-множественные. Варианты лямбда исчислений, теорий типов, конструктивизм, категорные подходы (ETCC)... Вот что-то такое интересно. В принципе, про теории множеств тоже можно поговорить, но не про ZFC-like (т.е. всякие MK, NBG и подобные - фтопку). Если уж и теории множеств, то интересны только такие, в которых в сигнатуре есть не только $\in$. Например, IST (там в сигнатуре есть одноместный предикат St - предикат стандартности). Такие теории множеств - нормально, можно обсудить. Вообще, хочется чего-то менее выразительного чем теории множеств, но с какими-нибудь хорошими свойствами.

[dgwuqtj]

Из «хардкордных» вариантов есть $\mathrm{PA}$, арифметика второго порядка $\mathrm Z_2$, а также их более слабые варианты. В арифметике второго порядка уже можно развивать математический анализ, ну и есть арифметики третьего и т.д. порядков.

Подходы с теорией типов — это те, что используются в системах компьютерных доказательств, то есть $\mathrm{CoC}$, $\mathrm{HoTT}$ и всякое в этом духе. Это даже не теории первого порядка. А ETCC — это теоретико-множественный подход, просто на другом языке.

В плане выразительности теории типов и множеств примерно эквивалентны, они отличаются только наличием больших кардиналов и аксиом степени/преобразования/выбора. Без понятия, как такие понятия выразить в теории типов. Арифметика менее мощная, скажем, PA — это примерно теория множеств без аксиомы бесконечности.

Вы бы взяли что-то в духе доказательства бесконечности множества простых чисел в этих системах и сравнили. А потом ещё основную теорему алгебры.

[EminentVictorians]

dgwuqtj в сообщении #1682995 писал(а):

Из «хардкордных» вариантов есть $\mathrm{PA}$, арифметика второго порядка $\mathrm Z_2$, а также их более слабые варианты. В арифметике второго порядка уже можно развивать математический анализ, ну и есть арифметики третьего и т.д. порядков.

Я вчера как раз прочитал на ncatlab, что даже в EFA (elementary function arithmetic) строится огромный кусок математики, хотя она слабее PA. Я понимаю так, что все эти системы - для неверующих. Т.е. для тех, кто сильно озабочен противоречивостью, хочет ограничивать себя в средствах, чтобы гарантированно использовать только самые надежные. Это не мой случай, я даже в теорию множеств верю. Да и противоречивость меня не сильно заботит. Теория множеств мне не нравится из-за других причин. Она какая-то слишком "жесткая". Мы можем взять любое множество, выкинуть из него, можно сказать, любой элемент и получим в итоге тоже множество. Я тут поймал себя на мысли, что мне даже аксиома экстенсиональности не нравится, хочу её ослабить. Хочется, чтобы математика была какая-то более "мягкая", чтобы было не вот это жесткое теоретико-множественное $=$, а равно в смысле какой-нибудь эвивалентности. Чтобы не требовалось совпадение буквально всех элементов.

dgwuqtj в сообщении #1682995 писал(а):

Подходы с теорией типов — это те, что используются в системах компьютерных доказательств, то есть $\mathrm{CoC}$, $\mathrm{HoTT}$ и всякое в этом духе. Это даже не теории первого порядка.

И хорошо, что не теории первого порядка. Бестиповое лямбда исчисление тоже не является теорией первого порядка, а сколько всего там можно смоделировать.

[dgwuqtj]

EminentVictorians в сообщении #1683007 писал(а):

Хочется, чтобы математика была какая-то более "мягкая", чтобы было не вот это жесткое теоретико-множественное $=$, а равно в смысле какой-нибудь эвивалентности. Чтобы не требовалось совпадение буквально всех элементов.

Тогда читайте книжку Homotopy type theory, как раз что-то такое и будет. Только в реальной математической деятельности это почти всегда неудобно.

[EminentVictorians]

Я просто вот как рассуждаю. Почему вообще математика так эффективна? Потому что она дает язык для построения очень длинных цепочек рассуждений, которые словами было бы тяжело (практически - невозможно) проговорить. Т.е. эффективность - в самой возможности заменять одни выражения другими, делать преобразования. Но если мы строим математику на фрэймворке теории множеств, получается такая ситуация, что у нас часто возникают очень похожие, но формально не равные объекты. Перейти от одного из них к другому (т.е. просто заменить один из них другим) в выкладках не получится, т.к. они не равны. Частично спасают различные связки типа $\sim$, $\approx$, и т.д. Но базово мы все равно почти всегда переходим от одного предмета к другому с помощью $=$. А когда $=$ слишком жесткое, встраивать длинные цепочки становится слишком трудно (т.к. мельчайшее несовпадение объектов сразу обрубает цепочку равенств). Именно поэтому в теории множеств приходится делать все эти выкрутасы с эквивалентностью, вложениями, фактормножествами и прочее.

[dgwuqtj]

Вы на свой собственный опыт опираетесь или на какую-то статистику? Это зависит от раздела математики. Там, где куча изоморфных объектов, приходится следить за коммутативностью всяких диаграмм, и теоретико-множественный язык с добавлением струнных диаграмм и подобных формализмов с этим справляется (в геометрии и топологии вообще картинки рисуют, и ничего). А теории типов люди мало используют, их больше для компьютеров продвигают. Видимо, не очень удобные.

[Ende]

Тема перемещена из форума «Беседы на околонаучные темы» в форум «Математика (общие вопросы)»
Причина переноса: в профильный раздел.

[EminentVictorians]

dgwuqtj в сообщении #1683035 писал(а):

Вы на свой собственный опыт опираетесь или на какую-то статистику?

На свой опыт, никакой статистики у меня нету.

dgwuqtj в сообщении #1683035 писал(а):

теоретико-множественный язык с добавлением струнных диаграмм и подобных формализмов с этим справляется

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

[dgwuqtj]

Возьмём конкретное утверждение, например, "все сопряжённые слева функторы к данному естественно изоморфны, притом единственным образом". Оно обычно доказывается на естественном языке, например, русском или английском. При желании это легко формализовать в теории множеств, там все утверждения легко записать через логику первого порядка с равенством. Для удобства можно использовать струнные диаграммы, ровно для конструкций нужных естественных преобразований и доказательства их равенства. При формализации в теории типов вместо формул первого порядка будут некие термы, но всё равно доказываться будут всякие равенства (т.е. будут строиться экземпляры типов для равенств), просто это будет ещё менее похоже на естественный язык.

[EminentVictorians]

Кстати, еще насчет HoTT хотел бы спросить. Правильно ли я понимаю, что она по большей части ориентирована на алгебраических топологов? Т.е. если я, например, алгебраический тополог, и мне не нравится теория множеств, то я - как раз целевая аудитория для HoTT. А если я не алгебраический тополог? Там есть какая-то фундаментаьная идея, не привязанная ко всем этим гомологиям и гомотопиям?

[dgwuqtj]

Насколько я понимаю, HoTT — это язык для $\infty$-группоидов. То есть её можно использовать ещё в алгебраической геометрии, гомологической алгебре, алгебраической $\mathrm K$-теории, логике, собственно в теории категорий, в задачах автоматического доказательства, в придумывании языков программирования... Но обычно алгебраические топологи не используют формальную теорию множеств, им ZFC знать не обязательно, достаточно английского и алгебраической топологии.

[EminentVictorians]

dgwuqtj в сообщении #1683059 писал(а):

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

Но неформализованную теорию множеств используют же. Да, они не рисуют деревья с формальными аксиомами и правилами вывода, но когда хотят доказать, что $A = B$, вполне себе доказывают $A \subset B$ и $B \subset A$, т.е. пользуются неформализованной аксиомой экстенсиональности. Топология у них - это все равно подмножество булеана. Функция у них - это подмножество декартова произведения. Т.е. да, они не отслеживают номера аксиом и не пишут явно правила вывода, которыми пользуются, но по полной программе используют неформальную ZFC или что-то типа неё (может неформальную NBG). Не выглядит так, что достаточно английского и алгебраической топологии.

То есть я веду к тому, что хоть практически никто из математиков явно не использует формализованную ZFC, их обычная математическая деятельность все равно во многом обусловлена (или "инспирирована", не знаю какое тут слово подобрать) теорией множеств, пусть и не формализованной.

[dgwuqtj]

EminentVictorians в сообщении #1683060 писал(а):

Но неформализованную теорию множеств используют же.

Они используют неформальные математические рассуждения. Да, там есть множества, а ещё есть типы (они даже не пытаются доказывать $A \subset B$, если $A$ и $B$ — это гомоморфизмы между группами гомологий), арифметика, вещественные числа как первичная сущность и т.д. Причём они обычно работают не в категории всех топологических пространств, а в чём-то в духе $\mathbf{CGWH}$, категории клеточных пространств или вообще в категории симплициальных множеств. Вряд ли они часто задумываются над вопросами оснований.

Вы почему-то думаете, что если переписать всю математику на HoTT, то всё должно кардинально поменяться, включая математическую интуицию. А я думаю, что вообще почти ничего не изменится, только книги по основаниям математики надо переделать и раздуть в несколько раз. Причём ту же классическую логику придётся оставить (переписав теорию моделей на язык топосов), она нужна не только для оснований.

Во всяком случае, классический анализ, теория групп, комплексный анализ, комбинаторика, синтетическая геометрия и элементарная теория чисел были придуманы задолго до возникновения теории множеств.

[EminentVictorians]

dgwuqtj в сообщении #1683066 писал(а):

Вы почему-то думаете, что если переписать всю математику на HoTT, то всё должно кардинально поменяться, включая математическую интуицию.

Тут половина - да, половина - нет. Я действительно думаю что интуиция может поменяться. Более того, такой пример есть. У меня довольно разная интуиция понятия функции в рамках теории множеств и в рамках лямбда исчисления. Вот буквально разные ощущения (от лямбда исчисления приятнее). У меня было так, что я сначала познакомился с самим (бестиповым) лямбда исчислением, и только потом узнал про его интерпретацию в теории множеств. И мне с самого начала казалось, что функций в лямбда исчислении меньше, и они какие-то более гладкие, что ли... Не настолько жесткие как в теории множеств.

Но на самом деле смена интуиции - это не цель. Цель в том, чтобы выкладки стали более разнообразными. Чтобы можно было не различать больше объектов, конструировать какие-нибудь странные операции, не очевидные на базе теории множеств (потому что теоретико-множественный язык очень плох в "подсказывании", в отличие от, например, категорного языка).

[dgwuqtj]

Вот я что-то не видел примеров математических текстов, где «не теоретико-множественный подход» был бы выигрышным. Кроме тех, где речь идёт про соответствующие абстрактные объекты, и то обычно это топосы (или что-то послабее), в которых логика первого порядка.