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

[alex_dorin]

Здравствуйте !
Как выглядит аксиома бесконечности средствами ZFC, т.е. с использованием единственного двуместного предиката "элемент' ,
или подскажите литературу, где она выписана явно?
С уважением
А. Дорин

[Nemiroff]

https://en.wikipedia.org/wiki/Axiom_of_infinity

[Someone]

$$\exists a(((\forall x\neg(x\in p))\Rightarrow(p\in a))\wedge\forall x((x\in a)\Rightarrow\exists y((y\in a)\wedge\forall z((z\in y)\Leftrightarrow((z\in x)\vee\forall t((t\in z)\Leftrightarrow(t\in x)))))))$$

Надеюсь, не наврал.

[Nemiroff]

$p$ замкните.

[Someone]

Не понял. В начале написать $\forall p$? По умолчанию свободные переменные предполагают квантор всеобщности. Но если хочется, можно его написать явно.

-- Вт июл 21, 2015 22:41:50 --

$\exists a(\forall p((\forall x\neg(x\in p))\Rightarrow(p\in a))\wedge\forall x((x\in a)\Rightarrow\exists y((y\in a)\wedge\forall z((z\in y)\Leftrightarrow((z\in x)\vee\forall t((t\in z)\Leftrightarrow(t\in x)))))))$

Теперь возражений нет?

[Nemiroff]

Someone в сообщении #1039287 писал(а):

По умолчанию свободные переменные предполагают квантор всеобщности.

Да? ОК.

Someone в сообщении #1039287 писал(а):

Теперь возражений нет?

Вроде бы нет.
А так сойдёт?
$\exists y (\forall p((\forall x\neg(x\in p))\Rightarrow(p\in y)) \wedge \forall z (z \in y \Rightarrow \exists t (z \in t \wedge t \in y )))$

[Someone]

$\exists a(\forall p((\forall x\neg(x\in p))\Rightarrow(p\in a))\wedge\forall x((x\in a)\Rightarrow\exists y((y\in a)\wedge\forall z((z\in y)\Leftrightarrow((z\in x)\vee\forall t((t\in z)\Leftrightarrow(t\in x)))))))$

Фрагмент $\forall t((t\in z)\Leftrightarrow(t\in x))$ означает, что $z=x$, а фрагмент $\forall z((z\in y)\Leftrightarrow((z\in x)\vee(z=x)))$ означает, что $y=x\cup\{x\}$. Разумеется, $\forall x\neg(x\in p)$ означает, что $p=\varnothing$, поэтому начальный фрагмент (от $\forall p$ до первого $\wedge$) означает, что $\varnothing\in a$. С учётом этих сокращений у меня получается

$$\exists a((\varnothing\in a)\wedge\forall x((x\in a)\Rightarrow(x\cup\{x\}\in a))).$$

А у Вас, по-моему, что-то другое.

[mihaild]

Nemiroff в сообщении #1039296 писал(а):

$\exists y (\forall p((\forall x\neg(x\in p))\Rightarrow(p\in y)) \wedge \forall z (z \in y \Rightarrow \exists t (z \in t \wedge t \in y )))$

Под такую аксиому подходит, например, $\{0, 2, 3, 4, \ldots\}$ (и вообще любое бесконечное подмножество натуральных чисел, содержащее 0), а исходная аксиома требовала, чтобы множество содержало все натуральные числа.

[Nemiroff]

Someone в сообщении #1039308 писал(а):

С учётом этих сокращений у меня получается

Это понятно, вопросов нет.
У меня написано нечто вида $\exists y (\varnothing \in y \wedge y \subset \bigcup y)$
Наверное, это разные вещи.

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

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

При чём тут числа?

[mihaild]

Nemiroff в сообщении #1039327 писал(а):

При чём тут числа?

$0 = \emptyset, n + 1 = n + \{n\}$
Исходная аксиома утверждает существование множества, содержащего $0$ и для каждого $x$ из множества содержащее $x+1$.

А у Вас, в том числе, подходит $\{\emptyset, \{\emptyset\}, \{\{\emptyset\}\}, \ldots\}$.

[Someone]

mihaild, Вы забегаете вперёд. Аксиома бесконечности утверждает лишь существование индуктивного множества. Чтобы получить из этого модель натурального ряда, надо ещё проделать определённую работу. И не столь уж малую.

-- Ср июл 22, 2015 02:43:47 --

Nemiroff в сообщении #1039327 писал(а):

У меня написано нечто вида $\exists y (\varnothing \in y \wedge y \subset \bigcup y)$
Наверное, это разные вещи.

Это, безусловно, не совпадает со стандартной формулировкой аксиомы бесконечности. Но, скорее всего, она равносильна стандартной формулировке.

[alex_dorin]

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

Nemiroff в сообщении #1039296
писал(а):
$\exists y (\forall p((\forall x\neg(x\in p))\Rightarrow(p\in y)) \wedge \forall z (z \in y \Rightarrow \exists t (z \in t \wedge t \in y )))$

Где можно прочитать о такой форме ?

[Nemiroff]

alex_dorin в сообщении #1039419 писал(а):

Где можно прочитать о такой форме ?

Не знаю. Я когда писал, мне пришло в голову, что это то же самое, что и обычная формулировка. Потом пришло в голову, что это не то же самое.

Someone в сообщении #1039346 писал(а):

Но, скорее всего, она равносильна стандартной формулировке.

Metamath с вами согласен. http://us.metamath.org/mpegif/infeq5.html

[alex_dorin]

Nemiroff в сообщении #1039453 писал(а):

Someone в сообщении #1039346
писал(а):
Но, скорее всего, она равносильна стандартной формулировке. Metamath с вами согласен. http://us.metamath.org/mpegif/infeq5.html

Верно ли я понял, что прувером Metamath была доказана равносильность обеих форм аксиом бесконечности ?

[alex_dorin]

Аксиома бесконечности, предложенная Nemiroff
выводима из классической аксиомы бесконечности , изложенной Someone
я проверил это прувером Vampire 4.0
Обратное доказать пруверами SPASS, Vampire, Metis не удалось за обозримое время.
Наверное, классическая форма аксиомы бесконечности сильнее.