Выводимы ли в ZF аксиомы Пеано ?

[alex_dorin]

Выводимы ли в ZF аксиомы Пеано ?

[Xaositect]

Да (если зафиксировать какое-нибудь определение множества натуральных чисел)

[alex_dorin]

Xaositect -

В какой литературе это есть ? Какие аксиомы ZF(C) необходимы для этого, нужна ли аксиома индукции ?

[arseniiv]

В ZF нет аксиомы индукции.

-- Пн дек 30, 2013 18:00:53 --

Аксиома бесконечности ZF(C) вводит множество $\omega$, которое содержит $\varnothing$, и для каждого $a\in\omega$, $a\cup\{a\}\in\omega$.

Чтобы выразить аксиомы Пеано в теории множеств, нам нужно выразить сначала константу 0 и одноместный функциональный символ $S$, ну или как он может обозначаться у вас.

Если выбрать за множество натуральных чисел $\omega$, то 0 переводят как $\varnothing$, а $S(t)$ переводят как $t\cup\{t\}$.

Аксиома $\forall a\mathbin. S(a)\ne0$, например, переводится таким образом как $\forall a\mathbin. a\in\omega \to a\cup\{a\}\ne\varnothing$. Выводя эту формулу в ZF, вы сами без труда определите, какие аксиомы для этого вывода нужны.

[alex_dorin]

В ZF(C) ,конечно, нет аксиомы индукции. Я ее привел в вопросе из-за того , что она вполне выразима только в логике
второго порядка.

[Xaositect]

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

В какой литературе это есть ? Какие аксиомы ZF(C) необходимы для этого, нужна ли аксиома индукции ?

Литературу не припомню. Можете посмотреть http://us.metamath.org/mpegif/mmtheorems42.html#mm4133s и http://us.metamath.org/mpegif/mmtheorems56.html#mm5555s

-- Пн дек 30, 2013 16:12:48 --

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

В ZF(C) ,конечно, нет аксиомы индукции. Я ее привел в вопросе из-за того , что она вполне выразима только в логике второго порядка.

В аксиома индукции подмножества будут пониматься в смысле ZFC. Но можно доказать и схему аксиом индукции как метатеорему: http://us.metamath.org/mpegif/findes.html

[alex_dorin]

Очень не обычное изложение - много свободных переменных.
Я задал этот вопрос из-за того, что ни один пруверов за приемлемое время не смог доказать формулу
$(a + b) \cdot c = a \cdot c + b \cdot c$

[arseniiv]

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

Я ее привел в вопросе из-за того , что она вполне выразима только в логике второго порядка.

Схема аксиом индукции вполне выразима и в логике первого порядка. Ну и что что их бесконечное число. По идее, можно показать, что они все выводятся в теории множеств.

[alex_dorin]

Для представлении в ZF натуральніх чисел я принял -
натуральное число - конечное множество
арифметическая сумма 2- х натуральных чисел -- объединение 2-х непересекающихся множеств
арифметическое произведение 2-х натуральных чисел -- декартово произведение 2-х множеств
равенство 2-х натуральных чисел -- равномощнсть 2-х множеств

[arseniiv]

Боюсь, это не очень удобные «определения» для того чтобы доказать дистрибутивность.

Как вы перевели их в ZF?

[alex_dorin]

эти формулы в ZF длинны и меня тут заставляют использовать латекс, я за это тут не берусь

[Joker_vD]

alex_dorin
$S(x)=x\cup\{x\},\;0=\varnothing$

\begin{array}{l}1=S(0)=0\cup\{0\}=\{0\}\\ 2=S(1)=1\cup\{1\}=\{0\}\cup\{1\}=\{0,1\}\\ 3=S(2)=2\cup\{2\}=\{0,1\}\cup\{2\}=\{0,1,2\}\end{array}
ну и т.д.

[Xaositect]

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

равенство 2-х натуральных чисел -- равномощнсть 2-х множеств

Тут может быть проблема для прувера, доказательство равномощности - это доказательство существования. Пруверу придется как-то строить биекцию.

[Deggial]

Тема перемещена из форума «Помогите решить / разобраться (М)» в форум «Карантин»
Причина переноса: формулы не оформлены $\TeX$ом

alex_dorin
Наберите все формулы и термы $\TeX$ом.
Инструкции по оформлению формул здесь или здесь (или в этом видеоролике).
После исправлений сообщите в теме Сообщение в карантине исправлено, и тогда тема будет возвращена.

[Deggial]

Тема перемещена из форума «Карантин» в форум «Помогите решить / разобраться (М)»
Вернул. Наведите мышкой на формулу и увидите её код. Тег math почти всегда ставить не нужно, ставьте доллары - и шрифт приятнее.