Аксиома бесконечности

[Профессор Снэйп]

Стандартная формулировка аксиомы бесконечности в ZFC следующая:

$$ \exists x (\varnothing \in x \mathop{\&} \forall y(y \in x \rightarrow y \cup \{ y \} \in x)) $$

Через ZFC' обозначим систему аксиом, полученную из ZFC заменой аксиомы бесконечности на аксиому

$$ \exists x (\varnothing \in x \mathop{\&} \forall y(y \in x \rightarrow \{ y \} \in x)) $$

Показать, что ZFC и ZFC' эквивалентны.

P. S. Не уверен, что задаче место в олимпиадном разделе, но в "помогите решить/разобраться" она тоже как-то не смотрится.

[Профессор Снэйп]

Прошло полдня, AGu пока молчит. Удивительно!

[AGu]

Профессор Снэйп в сообщении #258299 писал(а):

Прошло полдня, AGu пока молчит. Удивительно!

Приятно, что я могу кого-то удивлять.
Еще приятнее, что я могу это делать, ничего не делая.
Откровенно говоря, я бы предпочел так же удивлять и дальше,
поскольку красивое решение у меня не наклевывается.
(Если есть что-то симпатичное, поделитесь, пожалуйста!)
Для очистки совести я набросаю то, что наклевывается.
Еще раз предупреждаю: будут только наброски,
причем до красоты им весьма далеко.

Пусть ${\rm I}$ — «стандартная» аксиома бесконечности (по фон Нейману),
${\rm I}'$ — «нестандартная» аксиома бесконечности (по Цермело),
${\rm ZFC}$ — «стандартная» совокупность аксиом теории множеств,
${\rm ZFC}'=({\rm ZFC}\backslash\{{\rm I}\})\cup\{{\rm I}'\}$.
Насколько я понимаю, достаточно показать, что ${\rm ZFC}\vdash{\rm I}'$ и ${\rm ZFC}'\vdash{\rm I}$.
Первое, в общем-то, хорошо известно: ${\rm I}'$ можно вывести в ${\rm ZFC}$
с помощью принципа рекурсии, который, в свою очередь,
доказывается с помощью принципа выделения и схемы подстановки.
Я не придумал ничего лучше, кроме как наметить тот же путь
для доказательства ${\rm I}$ в ${\rm ZFC}'$.

Итак, рассуждаем в ${\rm ZFC}'$.
Введем обозначения $0:=\varnothing$ и $n+1:=\{n\}$.
Множество $N$ назовем индуктивным, если $0\in N$ и $(\forall\,n\in N)\ n+1\in N$.
Как и в стандартном случае, с помощью принципа выделения можно

доказать, что существует наименьшее индуктивное множество $\omega'$
и что для него работает принцип индукции.

Для $n\in\omega'$ определим $[0,n)$ как объединение всех таких

подмножеств $S\subseteq\omega'$, что $(\forall\,m\in\omega')(m+1\in S\Rightarrow m\in S)$ и $n\notin S$
(возможно, тут можно придумать что-то попроще и поудобнее).

Теперь рассмотрим следующую формулу $\varphi(n,x)$:

$n\in\omega'$\ \land$
$\bigl(\exists\,f:[0,n+1)\to\mathbb V\bigr)$

$\bigl[f(0)=0\ \land\ \bigl(\forall\,m\in[0,n)\bigr)\bigl(\,f(m+1)=f(m)\cup\{f(m)\}\,\bigr)\ \land\ f(n)=x\bigr]$.

Индукцией по $n$ показываем, что $(\forall\,n\in\omega')(\exists!\,x)\,\varphi(n,x)$.
Применяем подстановку для $\omega'$ и $\varphi(n,x)$,

получаем $\omega:=\{x:(\exists\,n\in\omega')\,\varphi(n,x)\}$
и показываем, что $\omega$ удовлетворяет ${\rm I}$.

Не факт, что тут нет ляпов. В любом случае все это очень муторно.
Хочу красивое решение!