Конечные множества, ZF

[Xaositect]

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

Формулу, утверждающую предложение "все множества - конечные"
могу написать, но не в latex.
Нужно ввести не мало вспомогательных аксиом для вспомогательных предикатов.

Хотя бы скажите, Вы пользовались определением по Дедекинду (множество конечно, если не существует собственного подмножества, равномощного всему множеству)?

-- Вт июн 03, 2014 20:02:50 --

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

Мостовский А. Конструктивные множества и их приложения. М.: Мир, 19730 http://eqworld.ipmnet.ru/ru/library/boo ... 973ru.djvu

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

[alex_dorin]

Да , конечное множество - по Дедекинду.
Аксиома выделения выводима из аксиомы подстановки ( по памяти, доказательство в Френкель, Бар-Хиллел Основания теории множеств).
Если Вы считаете, что для нахождения противоречия в ZF c присоединенной новой аксиомой - "все множества конечны" нужна аксиома подстановки, то укажите ее схематический вид в логике первого порядка, хотя бы не формально, а интуитивно понятно.

А. Дорин

[arseniiv]

Надо заметить, что есть и альтернативные формулировки ZF, и что некоторые формулировки прекрасно переносятся в некоторые системы автоматического/автоматизированного доказательства целиком (это насчёт неиспользования вами аксиомы подстановки). Есть, например, такая штука как Metamath.

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

могу написать, но не в latex

У вас есть столько времени, сколько вам нужно, но как-нибудь освойте то маленькое подмножество латеха, которое нужно для таких формул. На этом форуме это для записи формул обязательно.

Аксиома бесконечности из указанной вами книги имеет вид

$$\exists x\exists y\left( y\in x\wedge\forall z\left( z\in x\to \exists t \left( t\in x\wedge t\ne z\wedge\forall s\left( s\in z\to s\in t \right) \right) \right) \right).$$

Видно, что эта аксиома $A_1$ постулирует существование множества, которое содержит какой-то элемент и вместе с каждым элементом содержит его собственное надмножество. Приведённая мной аксиома $A_2$ — просто более конкретизированный вариант $A_1$, она определяет единственный объект, в отличие от $A_1$. «Форма» у неё, однако, похожа настолько, что построить биекцию с собственным подмножеством можно так же, просто нужно сначала уметь определить минимальный по включению элемент $\mathsf Ia$ множества $a$, что ZF позволяет, и определить подмножество $x\mathsf Sa$ элементов, являющихся собственными надмножествами $x$, из множества $a$, что она тоже позволяет. После этого биекцией между $\omega$ и $\omega\setminus\{\mathsf I\omega\}$ будет функция, сопоставляющая $x$ значение $\mathsf I(x\mathsf S\omega)$.

[alex_dorin]

Наверное, для того, чтобы уметь определить минимальный по включению элемент множества , что ZF позволяет - как Вы пишите , без аксимы выбора не обойтись ?
Прувер Metamath я так и не понял, используются формулы со свободными переменными и формулы содержательно еще и с ошибками , имхо.
Есть пруверы для логики 2-го порядка , где полно можно выразить ZF, но там, как известно, со
стратегией поиска доказательства совсем плохо.

А. Дорин

[Xaositect]

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

Аксиома выделения выводима из аксиомы подстановки ( по памяти, доказательство в Френкель, Бар-Хиллел Основания теории множеств).
Если Вы считаете, что для нахождения противоречия в ZF c присоединенной новой аксиомой - "все множества конечны" нужна аксиома подстановки, то укажите ее схематический вид в логике первого порядка, хотя бы не формально, а интуитивно понятно.

Именно, без выделения в ZF нельзя сделать почти ничего, а без подстановки из используемой Вами системы она не выводится.
Для схемы аксиом выделения не нужна логика второго порядка, она формулируется не для любого свойства, а для любой формулы. Соответственно, для того, чтобы выразить аксиому выделения или подстановки в языке первого порядка, можно сделать два сорта термов - множества и формулы aka классы.

[alex_dorin]

Наверное, Вы имеете в виду теорию множеств NBG. Однако, у NBG есть первородный грех - невыразимость принципа математической индукции , это цена за конечную аксиоматизируемость теории множеств.

А. Дорин

[arseniiv]

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

Прувер Metamath я так и не понял, используются формулы со свободными переменными и формулы содержательно еще и с ошибками , имхо.

Что именно вы не поняли? Не совсем ясно из стиля изложения.

Ошибок там нет, иначе это было бы замечено давно. (А если вы настаиваете — то отстоите своё мнение, показав конкретные места, и в чём именно там ошибки.)

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

Наверное, для того, чтобы уметь определить минимальный по включению элемент множества , что ZF позволяет - как Вы пишите , без аксимы выбора не обойтись ?

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

[alex_dorin]

О прувере Metamath -

здесь приведена Axiom of Infinity with no distinct variable conditions
http://us.metamath.org/mpegif/mmzfcnd.html
содержит свободные переменные y, z - те , которые в начале формулы;
она явно отличается от приведеной выше, даже если как-то пытаться навешивать кванторы, чтобы получить
замкнутую формулу.
Может Вы как-то кратко на интуитивном уровне проясните наличие в формулах свободных переменных, т.к. вообще
это получаются некие непоименованые предикаты, например в случае Axiom of Infinity with no distinct variable conditions -
это предикат арности 2. Как он может называться аксиомой ?

А. Дорин

[arseniiv]

Аксиома из Мостовского:

$$\exists x\exists y\left( y\in x\wedge\forall z\left( z\in x\to \exists t \left( t\in x\wedge t\ne z\wedge\forall s\left( s\in z\to s\in t \right) \right) \right) \right).\eqno{(1)}$$

Приведённая вами аксиома из Metamath:

$$\exists x\left(y\in z\to\left(y\in x\wedge\forall y\left(y\in x\to\exists z\left(y\in z\wedge z\in x\right)\right)\right)\right).\eqno{(2)}$$

На самом деле она там теорема, а за аксиому берётся

$$\exists y\left(x\in y\wedge\forall z\left(z\in y\to\exists w\left(z\in w\wedge w\in y\right)\right)\right),\eqno{(3)}$$

где любая пара переменных из $x,y,z,w$ не может быть заменена на одну и ту же переменную. А предыдущая доказывается как теорема (и на этой странице перечисляется ещё куча альтернативных аксиом, все доказанные из этой).

Так вот, (3) утверждает существование множества $y$ такого, что ему принадлежит хотя бы один элемент, и что для каждого элемента $y$ существует содержащий этот элемент элемент $y$ (а не собственное надмножество этого элемента, как в (1)). Т. е. если $z\in y$, то и какое-то $\{z,\ldots\}\in y$ — в (1) же если $z\in y$, то и $\exists t\,t\notin z\wedge z\cup\{t,\ldots\}\in y$ — в этом вся разница. В (3) нет необходимости говорить что-то про неравенство, потому что аксиома регулярности гарантирует $a\ne\{a,\ldots\}$.

Любое из множеств, существующих из-за (3), также приводит к противоречию с «все множества конечны по Дедекинду», потому что и там строится биекция, только теперь там в нужных местах вместо включения принадлежность.

Теперь о выводимости (1) из (3). Из (3) выводится упоминавшаяся мной аксиома (4) существования ординала $\omega$; в короткой форме такая — ср. с

arseniiv в сообщении #871127 писал(а):

$\exists \omega\left( \varnothing\in\omega\wedge\forall x\left( x\in\omega\to x\cup\{x\}\in\omega \right\right)$

А из (4) выводится (1), потому что $x\subsetneq x\cup\{x\}$.

Что касается несвязанных переменных, они связываются при желании с помощью стандартного для исчисления предикатов правила вывода $\varphi\vdash \forall x\,\varphi$, выполненного в Metamath в виде аксиомы ax-gen.

-- Ср июн 04, 2014 14:08:34 --

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

она явно отличается от приведеной выше

Да, знаете ли, если $\Gamma,\varphi\vdash\psi$ и $\Gamma,\psi\vdash\varphi$, $\varphi$ и $\psi$ не обязаны даже содержать хоть один общий предикатный или функциональный символ. Зачем писать «явно отличается», коль это вообще ни при чём?

[alex_dorin]

arseniiv -
Большое спасибо за Ваш труд.
C уважением
А. Дорин

[arseniiv]

Благодарностью мне будет, когда вы разберёте, что не так в вашем доказательстве непротиворечивости ZF + «все множества конечны по Дедекинду» (а вы его даже не представили!).

[alex_dorin]

Здравствуйте !
Создан логический прувер, который позволяет доказывать или опровергать теоремы значительно более сложные, чем существующие пруверы. Действительно, присоединение к ZF аксиомы "все множества - конечны" делает систему аксиом противоречивой.
arseniiv, спасибо.

C уважением
Александр А. Дорин
г Полтава

[Someone]

Вообще-то, насколько я знаю, определить понятие "конечное множество" нельзя никаким набором аксиом. Поскольку где-то мне встречалась такая теорема: если теория имеет конечную модель со сколь угодно большим числом элементов, то она имеет и бесконечную модель. (По умолчанию речь идёт о логике первого порядка.)

В ZFC сначала определяются натуральные числа, а потом конечные множества определяются как множества, равномощные натуральным числам.

[alex_dorin]

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

[Someone]

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

Все просто - конечное множество - это множество , не являющееся бесконечным.

Ага. А бесконечное множество — это такое, которое не является конечным. Замечательное определение.