Еще раз об аксиоме выбора

[EminentVictorians]

epros в сообщении #1617205 писал(а):

Слово "модель" в этом смысле плохо тем, что обычно этот смысл подразумевает наличие в реальности моделируемого объекта.

Не сказал бы. По мне абсолютно нормально моделировать одни воображаемые объекты другими воображаемыми (но в некотором смысле более простыми) объектами.

epros в сообщении #1617205 писал(а):

Поэтому не удивителен интерес к тому, что было бы, если бы мы так и остались с одним сложением.

Да, тут согласен полностью.

epros в сообщении #1617205 писал(а):

И это очень интересный объект в том смысле, что достаточно слабый язык его определения позволяет реально получить ответ "да" или "нет" на любой вопрос, заданный на этом языке.

Ну да, она разрешимая. Вот только "объект" здесь - арифметика Пресбургера, а не натуральные числа.

epros в сообщении #1617205 писал(а):

Чем по-Вашему определяется "реальное" натуральное число?

Достаточно сильной теорией, годной для формализации всей (или почти всей) математики. Типа теории множеств или теории категорий.

epros в сообщении #1617205 писал(а):

А у меня есть хороший ответ: "Настоящих" нет, есть только придуманные.

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

epros в сообщении #1617205 писал(а):

Чем Вам далась эта ZFC?

Тем, что мое повседневное оперирование множествами очень похоже на то, что позволяет делать ZFC. У меня есть небольшая личная история, связанная с этим. Если лет 5 назад я еще делить столбиком толком не умел, то года 4 назад я уже пытался что-то учить математического и, разумеется, я не мог пройти мимо типичных экскурсов в наивную теорию множеств, которые встречаются в разных начальных курсах типа алгебры и анализа. Я тогда еще не знал ни про какую ZFC, но я очень хорошо помню, что у меня возник вопрос: допустим у нас есть множество $X$; с чего мы взяли, что существует $2^X$? Я даже пытался это как-то доказать По итогу, я пришел к выводу, что сам этот факт настолько базовый, что он сам по себе внушает доверие больше, чем любое его доказательство, каким бы оно ни была. Так что да, я официально переоткрыл одну аксиому ZFC .

epros в сообщении #1617205 писал(а):

Конечно же известны утверждения, не формализуемые иначе, чем в логике второго порядка.

А можно пример?

[epros]

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

По мне абсолютно нормально моделировать одни воображаемые объекты другими воображаемыми (но в некотором смысле более простыми) объектами.

Если Вы в состоянии вообразить сложный объект, то какой смысл его моделировать, упрощая?
Может, конечно, вычислительных ресурсов жалко. Но это уже какой-то отдельный разговор из области прикладных технических применений.

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

Вот только "объект" здесь - арифметика Пресбургера, а не натуральные числа.

Арифметика Пресбургера - это определение натуральных чисел со сложением.

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

epros в сообщении #1617205 писал(а):

Чем по-Вашему определяется "реальное" натуральное число?

Достаточно сильной теорией, годной для формализации всей (или почти всей) математики. Типа теории множеств или теории категорий.

Какая сила теории "достаточна"?

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

epros в сообщении #1617205 писал(а):

А у меня есть хороший ответ: "Настоящих" нет, есть только придуманные.

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

Не понимаю Вашего определения "настоящего". Что угодно можно "выделить" и в смысле этого выделения объявить "единственным".

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

epros в сообщении #1617205 писал(а):

Чем Вам далась эта ZFC?

Тем, что мое повседневное оперирование множествами очень похоже на то, что позволяет делать ZFC.

Это очень странное заявление. Прямо точно ничего не хочется добавить или убавить? Вариантов для этого - море. Просто ZFC как-то оказалась распиаренной в массовом математическом сознании как не слишком сложная, но достаточная "почти для всего" аксиоматика. Но в сущности в ней нет ничего особенного, своего рода математический ширпотреб.

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

epros в сообщении #1617205 писал(а):

Конечно же известны утверждения, не формализуемые иначе, чем в логике второго порядка.

А можно пример?

Самое известное - невыразимость в логике первого порядка аксиомы индукции. Схема индукции её не заменяет, поскольку она только для предикатов, выразимых формулами. В итоге - неоднозначность понятия натурального числа. Это не решается и теорией множеств первого порядка, поскольку как ни доказывай в теории множеств, что минимальное индуктивное множество единственно, у самой теории множеств обнаруживаются разные модели.

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

Ещё есть что-то про существование точной верхней грани, не помню, можете поискать.

Из простых утверждений на естественном языке известно такое: "Некоторые критики восхищаются только друг другом" (придумал его, насколько я помню, Булос). Невыразимость его языком первого порядка изящно доказывается построением модели критиков как раз на натуральных числах, которые могут оказаться и нестандартными.

В общем, примеров довольно много.

[mihaild]

epros в сообщении #1617218 писал(а):

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

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

[EminentVictorians]

epros в сообщении #1617218 писал(а):

Если Вы в состоянии вообразить сложный объект, то какой смысл его моделировать, упрощая?

Возьмем $n$-мерное векторное пространство $V(K)$ над полем $K$. Рассмотрим $GL_n(V)$ - группу обратимых линейных операторов вида $V \to V$. Могу я "вообразить" этот объект? Да запросто. Следует ли из этого, что его никогда не понадобиться ничем моделировать? Нет, не следует. Например, я могу выбрать базис в пространстве $V(K)$ и тем самым построить изоморфизм между $GL_n(V)$ и $GL_n(K)$ (последняя - группа невырожденных матриц размера $n \times n$), поставив в соответствие каждому оператору его матрицу в выбранном базисе. Тем самым, я моделирую "сложный" объект (группу операторов) "простым" объектом (группой матриц). Понятно, что сложный/простой - это понятия относительные и зависят от контекста. Так я и группу матриц в случае чего могу моделировать группой операторов, если последние окажутся проще для некоторой задачи. В общем, оба объекта - вымышленные. Оба же обозримые. Но это не мешает один объект моделировать другим.

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

epros в сообщении #1617218 писал(а):

Какая сила теории "достаточна"?

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

epros в сообщении #1617218 писал(а):

Прямо точно ничего не хочется добавить или убавить? Вариантов для этого - море.

Типа аксиому выбора на аксиому детерминированности? Нет, это точно не хочется. Вроде все устраивает. А какие есть варианты? Может мне что-то понравится.

epros в сообщении #1617218 писал(а):

Самое известное - невыразимость в логике первого порядка аксиомы индукции.

Почему "в логике первого порядка"? В арифметике Пеано же, а не во всей логике первого порядка. В ZFC аксиома индукции - это же обычная теорема про подмножества натуральных чисел. Разве нет?

epros в сообщении #1617218 писал(а):

В аксиоматике действительных чисел как непрерывного упорядоченного поля аксиома непрерывности - второго порядка.

Аналогично. Формализуется в ZFC.

epros в сообщении #1617218 писал(а):

но содержание при этом теряется.

Например, какое? Мне как-то не очевидно.

[mihaild]

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

В ZFC аксиома индукции - это же обычная теорема про подмножества натуральных чисел. Разве нет?

С точки зрения логики второго порядка (и "настоящей" семантики) эта теорема существенно слабее "настоящей" индукции - она (как и любая другая теорема ZFC) что-то утверждает только про те подмножества, что попали в нашу модель ZFC, а не про "все". Если натуральные числа нестандартные, то с точки зрения моделирующей теории, принцип индукции не выполнен, а вот теорема внутри модели - выполнена, разница из-за того, что внутри модели забыли положить некоторые подмножества.

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

А какие есть варианты?

https://en.wikipedia.org/wiki/List_of_statements_independent_of_ZFC
Например континуум-гипотеза. Или существование недостижимых кардиналов. Или элементарно непротиворечивость ZFC.

[epros]

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

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

Мало того, что скучный, так ещё и не о том. Матрицы - не проще операторов, ибо они и есть операторы, да ещё и записанные в конкретных координатах. "Моделировать" (в Вашем смысле) сложное простым, это, например, заменить понятие натуральных чисел, определённое арифметикой второго порядка ($Z_2$), понятием, определённым примитивно рекурсивной арифметикой ($PRA$), которая не может доказать даже всюду определённость функции Аккермана, не говоря уже о более сложных вещах.

Если у Вас нет каких-то специальных целей, то что может заставить Вас, знающего (и принимащего) такие вещи, как ВТФ или теорема Гудстейна, отказаться от них, ограничившись более простой "моделью"?

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

epros в сообщении #1617218 писал(а):

Какая сила теории "достаточна"?

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

Разумеется смысл словосочетания "обычная математика" нельзя принять без уточнений. Математика слишком обширна. Кому-то не хватит и теории, в которой принята гипотеза континуума, а кому-то достаточно и такой теории, в которой недоказуемо существование бесконечных множеств.

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

epros в сообщении #1617218 писал(а):

Прямо точно ничего не хочется добавить или убавить? Вариантов для этого - море.

Типа аксиому выбора на аксиому детерминированности? Нет, это точно не хочется. Вроде все устраивает. А какие есть варианты? Может мне что-то понравится.

Узко мыслите. Я вижу, что ZFC Вам "понравилась" настолько, что Вы практически убедили себя в том, что именно её-то Вы всегда и имели в виду чуть ли не с рождения. Или, по крайней мере, с того момента, как впервые услышали слово "множество". А чем Вам, скажем, NBG не нравится? Это почти то же самое, только плюс понятие "класса", которого в ZFC нет. Или почему не теория типов? Не теория категорий? Почему не мереология?

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

epros в сообщении #1617218 писал(а):

Самое известное - невыразимость в логике первого порядка аксиомы индукции.

Почему "в логике первого порядка"? В арифметике Пеано же, а не во всей логике первого порядка. В ZFC аксиома индукции - это же обычная теорема про подмножества натуральных чисел. Разве нет?

Нет, именно в логике первого порядка. Теория множеств первого порядка даёт иллюзию доказуемости аксиомы индукции, однако суть остаётся та же самая - индукция осуществляется только по формулам языка, а должна осуществлятся и по всем предикатам, невыразимым формулами.

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

[mihaild]

epros в сообщении #1617241 писал(а):

А чем Вам, скажем, NBG не нравится?

Я думаю что для любого содержательного математического разница между NBG и ZF неважна.
Если кому-то нужна гипотеза континуума, то её легко можно дописать в условия. А если кому-то хватает небольшого семейства множеств, то соответствующий результат опять же можно сформулировать и доказать в ZF - "для любого множества, моделирующего что нужно, выполнено что нужно".

epros в сообщении #1617241 писал(а):

индукция осуществляется только по формулам языка, а должна осуществлятся и по всем предикатам, невыразимым формулами

Вроде бы всё же по подмножествам.
Формулировка индукции в ZF: $\forall P: (0 \in P \wedge (\forall x: x \in P \rightarrow x + 1 \in P)) \rightarrow \mathbb (N \subseteq P)$. Где тут формулы?
Формулы появятся только дальше, когда мы будем применять индукцию к конкретному $P$, заданному конкретной формулой.

[epros]

mihaild в сообщении #1617244 писал(а):

Я думаю что для любого содержательного математического разница между NBG и ZF неважна.

Ну так несобственных классов нет, уже некоторое неудобство. Есть за что невзлюбить эту аксиоматику.

mihaild в сообщении #1617244 писал(а):

Вроде бы всё же по подмножествам.
Формулировка индукции в ZF: $\forall P: (0 \in P \wedge (\forall x: x \in P \rightarrow x + 1 \in P)) \rightarrow \mathbb (N \subseteq P)$. Где тут формулы?

Это понятно, что по "множествам", но множества-то всё равно могут быть только такие, существование которых доказуемо в аксиоматике. Вот построим счётную модель ZFC и окажется, что только по множествам этой модели разрешена индукция. Теорема Лёвенхейма-Сколема ведь опирается именно на то, что теория сформулирована на языке логики первого порядка.

[dgwuqtj]

epros в сообщении #1617246 писал(а):

Вот построим счётную модель ZFC и окажется, что только по множествам этой модели разрешена индукция.

Их всё равно намного больше, чем формул, а счётность -- это просто некоторое свойство в метатеории.

[mihaild]

epros в сообщении #1617246 писал(а):

Ну так несобственных классов нет, уже некоторое неудобство

Неудобство, но переводить туда-сюда можно.

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

Их всё равно намного больше, чем формул

Можно построить модель ZF, в которой любое множество будет задаваться некоторой формулой. Естественно сама модель об этом знать не будет.

[dgwuqtj]

mihaild в сообщении #1617250 писал(а):

Можно построить модель ZF, в которой любое множество будет задаваться некоторой формулой.

Вы про конструктивный универсум? Там множества на уровне $\alpha$ задаются через множества на предыдущих уровнях. Это не лучше, чем наивная запись через $\{\ldots\}$, всё равно почти ничего не получится полностью определить конечными наборами формул, изначально имея только аксиомы. Ну и надо заранее иметь все ординалы.

[mihaild]

Я про pointwise definable модель. Для каждого её элемента существует формула с одной свободной переменной, которая в этой модели выполнена в точности на этом элементе.

[dgwuqtj]

Интересно. Спасибо за ссылку!

[epros]

Вот это я пропустил:

mihaild в сообщении #1617222 писал(а):

А где на практике используются рассуждения, требующие "настоящую" индукцию, которые не формализуются в теории множеств первого порядка?

Например, теорему Гудстейна позволяет доказать. Я так понимаю, что рассуждения про конструкции вида $x^{x^{\cdot^{x}}}$ с конечным количеством степеней записываются формулами конечной длины, но нет одной формулы конечной длины, которая бы сказала нечто нам нужное про подобную конструкцию с произвольным количеством степеней. Наверное, в некотором смысле можно сказать, что подобная "бесконечная формула" и должна выражать тот предикат, индукция по которому позволяет доказать теорему Гудстейна.

mihaild в сообщении #1617222 писал(а):

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

Мне тоже. Я вообще не понимаю, что такое "стандартная семантика". Фразы типа: "Квантор всеобщности на переменной второго порядка означает, что имеются в виду действительно все подмножества универсума", - меня совершенно не вдохновляют.

[EminentVictorians]

epros в сообщении #1617241 писал(а):

Матрицы - не проще операторов, ибо они и есть операторы

Ну уж нет. Матрица из элементов, принадлежащих множеству $M$, - это функция из декартова произведения частично упорядоченных множеств в некоторое множество $M$. Обычно в качестве частично упорядоченных множеств берут начальные отрезки $\mathbb N$ с порядком, наследованным с канонического порядка на $\mathbb N$, а декартово произведение берут двух таких начальных отрезков. Так что матрица - это функция с вполне конкретной областью определения. Линейный оператор - это тоже функция, но уже из носителя векторного пространства. Так что эти объекты точно нельзя отождествлять.

epros в сообщении #1617241 писал(а):

операторы, да ещё и записанные в конкретных координатах

Мне неизвестно понятие "оператор, записанный в некоторых координатах". Я могу доказать теорему, что выбор базиса в $V(K)$ индуцирует изоморфизм между пространством операторов и пространством матриц. Тем самым, оператору присваивается некоторая матрица. Но он сам нигде не записывается.

epros в сообщении #1617241 писал(а):

"Моделировать" (в Вашем смысле) сложное простым, это, например, заменить понятие натуральных чисел, определённое арифметикой второго порядка ($Z_2$), понятием, определённым примитивно рекурсивной арифметикой ($PRA$), которая не может доказать даже всюду определённость функции Аккермана, не говоря уже о более сложных вещах.

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

epros в сообщении #1617241 писал(а):

А чем Вам, скажем, NBG не нравится?

Тем, что я множества строю, а не просто рассматриваю какие-то совокупности.

epros в сообщении #1617241 писал(а):

Почему не мереология?

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