Матлогика, вывод формулы из теории ZF

[SDMF]

Дано:формула,

$$$ \forall X(\exists v(v \in X) \to \exists !Y\forall z(z \in Y \rightleftarrows \forall u(u \in X \to z \in u))) $$$

Требуется доказать, что это - теорема Цермело-Френкеля, как я понимаю, это означает что нужно её вывести из аксиом.

Первые шаги решения:
Я понял буквальный смысл этой формулы: X - множество, состоящее из множеств, Y - некое множество, в которое входят элементы, содержащиеся во всех элементах из X. То есть, Y - объединение всех элементов X.

Дальше - единственная идея, что нужно составить некую функцию,$$$ \varphi (z) $$ $ которая выдаваёт истину, если элемент z находится во всех множествах из X, и работать с аксиомой подстановки.

[Ираклий]

SDMF в сообщении #274086 писал(а):

Я понял буквальный смысл этой формулы: X - множество, состоящее из множеств, Y - некое множество, в которое входят элементы, содержащиеся во всех элементах из X. То есть, Y - объединение всех элементов X.

Только не объединение, а пересечение. Доказывается эта формула с использованием аксиомы объединения и аксиомы выделения.

[SDMF]

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

Хорошо, попробую, как Вы сказали.

[SDMF]

Нет, не получается что-то, всё время квантор при

$$ (u \in X \to z \in u) $$

получается существования

[Ираклий]

Если Вам нужен вывод формулы $ \forall X(\exists v(v \in X) \to \exists !Y\forall z(z \in Y \rightleftarrows \forall u(u \in X \to z \in u))) $ в непосредственном смысле этого слова (т.е. цепочка формул, каждая из которых либо аксиома, либо получается из предыдущих по правилам вывода), то я не готов взять на себя труд выписывания подобного вывода. Могу рассказать доказательство на неформальном уровне (которое, я верю, можно превратить в вывод при наличии времени и усердия).

1) Пусть Х - произвольное множество, такое, что $\exists v(v \in X)$.
2) По аксиоме объединения, существует такое множество Z, что $\forall z(z \in Z \rightleftarrows \exists u(u \in X \& z \in u)))$.
3) Применим к этому множеству аксиому выделения для формулы $\forall u(u \in X \to z \in u)$. (Аксиома выделения - это на самом деле схема аксиом, она зависит от формулы.)
4) Получим множество Y, такое, что $\forall z(z \in Y \rightleftarrows (z \in Z \& \forall u(u \in X \to z \in u)))$.
5) Покажем, что это множество удовлетворяет желаемому нами условию: $\forall z(z \in Y \rightleftarrows \forall u(u \in X \to z \in u))$. Для этого достаточно проверить, что $\forall u(u \in X \to z \in u) \to z \in Z$.
6) Последнее легко усматривается из того, что $\exists v(v \in X)$.
7) Единственность Y следует из аксиомы экстенсиональности.

Вот как-то так. Форумчане, проверьте, не наврал ли где в формулах.

[SDMF]

спасибо, вроде выглядит без ошибок. Я постоянно ошибался при переходе от аксиомы объединения к выделения

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

Ираклий в сообщении #274105 писал(а):

Только не объединение, а пересечение. Доказывается эта формула с использованием аксиомы объединения и аксиомы выделения.

А зачем аксиома объединения? Разве просто выделения недостаточно?

[Ираклий]

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

Разве просто выделения недостаточно?

ммм... Пожалуй, Вы правы! Можно выделять не из объединения, а из какого-нибудь элемента семейства X.