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

[mihaild]

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

Например, теорему Гудстейна позволяет доказать

Теорема Гудстейна доказывается в ZF.

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

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

Не очень понял - Вы утверждаете, что её даже сформулировать не получится? $x\uparrow y$ вообще примитивно рекурсивная, утверждение $x \uparrow y = z$ записывается $\Sigma_1$-формулой в PA.

[epros]

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

Теорема Гудстейна доказывается в ZF.

Известно, что в $Z_2$ тоже доказывается. Это к вопросу о том, что нового позволяет логика второго порядка в смысле вывода.

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

Не очень понял - Вы утверждаете, что её даже сформулировать не получится? $x\uparrow y$ вообще примитивно рекурсивная, утверждение $x \uparrow y = z$ записывается $\Sigma_1$-формулой в PA.

Не именно её. Насколько я знаю, теорема Гудстейна доказывается трансфинитной индукцией до ординала $\varepsilon_0$. Поэтому вопрос заключается в том, почему в языке первого порядка эту трансфинитную индукцию нельзя свести к математической, а в языке второго порядка можно. Получается, что для индукции до любого ординала $\omega\uparrow n$ этот переход к математической индукции выражается конечной формулой, а для индукции до $\omega\uparrow\omega$ - уже нет.

-- Сб ноя 11, 2023 12:21:25 --

Похожая проблема в $PRA$ с доказательством всюду определённости функции Аккермана. Язык без кванторов позволяет свести индукцию до любого ординала $\omega^n$ к математической, но попытка проделать то же самое до ординала $\omega^\omega$ приводит к бесконечной формуле (или к цепочке вывода бесконечной длины).

-- Сб ноя 11, 2023 13:02:05 --

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

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

Вот к чему все эти умствования? Просто сравните действительнозначную матрицу $5 \times 5$ и линейный оператор на 5-мерном векторном пространстве над полем $\mathbb R$.

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

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

Так выбор базиса - и есть запись в координатах этого базиса. Вы погрязли в формализмах словообразования.

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

Можно внутри одной теории моделировать одну структуру другой.

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

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

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

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

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

Т.е. несобственные классы Вы не признаёте?

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

Короче, вообще ничего не понял.

Понятно, незнакомство с темой не породило к ней "любви, прослеживаемой с рождения", как это произошло с ZFC.

[mihaild]

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

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

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

[EminentVictorians]

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

Вот к чему все эти умствования?

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

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

Просто сравните действительнозначную матрицу $5 \times 5$ и линейный оператор на 5-мерном векторном пространстве над полем $\mathbb R$.

Для меня это разные объекты.

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

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

Да нет же. Не синоним слова "теория". Когда простая абстракция ухватывает нужные нам свойства какой-то сложной абстракции, то эту простую абстракцию и называют моделью сложной абстракции. Теориями они быть не обязаны (но могут). Можно совсем простой пример привести. Когда Вы аппроксимируете какую-нибудь сложную функцию каким-нибудь сплайном, по мне это уже моделирование.

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

Т.е. несобственные классы Вы не признаёте?

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

[epros]

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

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

Я понял. Просто теория множеств второго порядка - слишком сложная штука для обсуждения. Хотя очевидно, что там тоже возникают какие-то новые возможности говорить о невыразимых языком предикатах. Привести пример формулы, невыводимой в теории множеств первого порядка, но выводимой в теории множеств второго порядка, будет затруднительно, поскольку proof-theoretic ординал для ZFC неизвестен.

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

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

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