Омега минус один

[Munuvonaza]

В традиционных ординалах фон Неймана, определяемых из аксиомы бесконечности ZF, операция вроде $\omega - 1$ является неопределенной, поскольку $\omega$ есть предельный ординал и операция декремента к нему не применима
Если рассматривать вопрос формально, то это означает, что в ZF должна быть опровержима формула, определяющая существование множества Y, которое в объединении с одноэлементным множеством $\{Y\}$ равно множеству, представляющему ординал $\omega$, или чуть более точно
$\exists X \exists Y [[(\emptyset \in X)\wedge \forall w(w\in X\implies (w\cup \{w\})\in X ) ]\wedge [(Y\cup \{Y\}) = X]]$
Хотя из-за шорткатов вида $\emptyset$, $A \cup B$, $A=B$ и $\{S\}$ это не совсем строгая ZF-формула, понятно что имеется в виду - если эта формула неопровержима из стандартных ZF-аксиом, то множество $Y$ существует, а это как раз то самое $\omega - 1$ по определению
Собственно вопрос - как опровергать такую формулу, т.е. выводить ее отрицание или вступать в противоречение с аксиомами?

И еще дополнительный вопрос - может ли быть, что существование $\omega - 1$ независимо от стандартных ZF-аксиом? То есть в традиционном ZF множество $\omega - 1$ не существует, но можно добавить независимую аксиому, по аналогии как это делается с аксиомой выбора, и существование множества $\omega - 1$ не будет ничему противоречить?

P.S. Интересует именно строгая формально-логическая сторона вопроса. Пожалуйста, не надо ответов в духе $\omega$ есть предельный ординал и поэтому $\omega - 1$ не существует. Интересует именно доказательство от аксиом и совместимость/несовместиомсть тех или иных объектов с конкретными аксиомами
Спасибо!

[mihaild]

Раз $Y \cup \{Y\} = \omega$, то $Y \in \omega$. А дальше индукцией по $x$ показываем, что $\forall x \in \omega: x \cup \{x\} \neq \omega$.

[dgwuqtj]

Давайте заведём предикат $\mathrm{ind}(X) \Leftrightarrow \varnothing \in X \wedge \forall x \in X \enskip x \cup \{x\} \in X$. По определению, $\omega$ — это наименьшее множество по включению, удовлетворяющее $\mathrm{ind}$. И словами вы написали, что хотите доказать $\neg \exists Y \enskip Y \cup \{Y\} = \omega$. А формула у вас говорит $\forall X \enskip \mathrm{ind}(X) \Rightarrow \neg \exists Y \enskip Y \cup \{Y\} = X$, это более сильное утверждение.

Даже для более сильного утверждения, возьмём такое индуктивное $X$ (удовлетворяющее $\mathrm{ind}$) и предположим, что $X = Y \cup \{Y\}$ для некоторого $Y$. Тогда $Y \in X$, так что из индуктивности следует $Y \cup \{Y\} \in X$. Другими словами, $X \in X$. А это противоречит аксиоме регулярности.

Аксиома выбора, аксиома объединения и схема аксиом преобразования не используются. Аксиома бесконечности тоже формально не используется, она нужна только для существования индуктивных множеств. Аксиома регулярности для утверждения конкретно про $\omega$ вроде тоже не нужна, но тут надо думать.

[mihaild]

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

Аксиома регулярности для утверждения конкретно про $\omega$ вроде тоже не нужна, но тут надо думать.

Не нужна, для элементов $\omega$ она выполнена автоматически (множество всех фундированных элементов индуктивного множества само индуктивно ).

[Munuvonaza]

Спасибо огромное за ответы, четко и по существу!
Пользуясь случаем, еще один вопрос по смежной теме - существует ли версия аксиомы детерминированности, которая есть мягкая замена для аксиомы выбора, в виде какой-то разумной формулы логики первого порядка?
Везде много объяснений на примере теории игр, и суть аксиомы детерминированности в принципе ясна, но совсем не понятно, как такое словесное описание, включающее нетривиальные и довольное неформальные по меркам FOL конструкции, описать в FOL-терминах, ну или хотя бы словесным наброском

[dgwuqtj]

Возьмите описание на языке теории игр и переведите всё на язык теории множеств. То есть для любого подмножества $A \subseteq \omega^\omega$ либо существует стратегия для первого игрока (последовательность функций $f_k \colon \omega^{2 k} \to \omega$ для всех $k \in \omega$) такая, что любая последовательность ходов $x \colon \omega \to \omega$, когда первый игрок ходит согласно стратегии (то есть $f_k(x_0, \ldots, x_{2 k - 1}) = x_{2 k}$), принадлежит $A$, либо существует аналогичная стратегия для второго игрока.

А в каком смысле это замена аксиомы выбора? Для приложений обычно хватает счётной аксиомы выбора (ну или аксиомы зависимого выбора).