Независимость и невыводимость

[Unx]

Аксиомы Пеано:
1 $0 \in \mathbb{N}$
2 $x \in \mathbb{N} \rightarrow Sx \in \mathbb{N}$
3 $x \in \mathbb{N} \rightarrow Sx \neq 0$
4 $x \in \mathbb{N} \land y \in \mathbb{N} \land Sx = Sy \rightarrow x=y$
5 $0 \in M \land \forall x (x \in M \rightarrow Sx \in M) \rightarrow N \subseteq M$
Я пытаюсь доказать независимость первой аксиомы от остальных. Для этого можно в качестве $\mathbb{N}$ взять пустое множество (можно я его буду называть моделью?) Для пустого множества выполняются все аксиомы кроме первой, следовательно, если первая аксиома доказывается (как теорема) с помощью четырех остальных, то для данной модели мы получили бы противоречие с теорией множеств. Таким образом вопрос независимости сводится к вопросу непротиворечивости теории множеств + аксиомы Пеано 2-5. Правильно ли я рассуждаю? И как мне закончить решение?
Другой вопрос о том, как показать невыводимость первой аксиомы из остальных и влечет ли она независимость? Или может наоборот из независимости следует невыводимость?

[Sonic86]

Вам надо просто прочитать определение независимости аксиомы от остальных и привести 2 таких модели, в каждой из которых выполняются остальные аксиомы, но 1-я аксиома выполняется только в одной модели и не выполняется в другой. Из этого следует независимость по определению, она же невыводимость аксиомы и невыводимость ее отрицания.
Одну модель Вы уже придумали, осталось придумать вторую.
Метатеорию и используемую для рассуждения теорию считайте непротиворечивыми по умолчанию.

[Unx]

Sonic86 в сообщении #1084110 писал(а):

Одну модель Вы уже придумали, осталось придумать вторую.

Придумать вторую в той же самой метатеории? Или это не обязательно?
Ну вот есть готовая теоретико-множественная модель, где $\mathbb{N}$ определяется как объединение всех множеств, содержащих пустое, и замкнутое относительно операции $S$. Операция $S$ определяется рекуррентным способом:
$0=\varnothing $
$1=S(0)=\{0\}$
$2=S(1)=\{0,1\}$
...
Первая аксиома выполняется в силу существования пустого множества. Вторая - в силу замкнутости операции. Третья - из определения операции $S$ и так далее...

Sonic86 в сообщении #1084110 писал(а):

Из этого следует независимость по определению, она же невыводимость аксиомы и невыводимость ее отрицания.

Объясните как все это взаимосвязано. Как из независимости получается невыводимость?

[Unx]

Нет, что-то у меня здесь не то написано.

Цитата:

The set $\mathbb{N}$ of natural numbers is defined as the smallest set containing $0$ and closed under the successor function $S$ defined by $S(n) = n \cup \{n\}$.

[Sonic86]

Unx в сообщении #1084196 писал(а):

Ну вот есть готовая теоретико-множественная модель, где $\mathbb{N}$ определяется как объединение всех множеств, содержащих пустое, и замкнутое относительно операции $S$. Операция $S$ определяется рекуррентным способом:
$0=\varnothing $
$1=S(0)=\{0\}$
$2=S(1)=\{0,1\}$
...
Первая аксиома выполняется в силу существования пустого множества. Вторая - в силу замкнутости операции. Третья - из определения операции $S$ и так далее...

Ну вот и все: это и есть 2-я модель.

Unx в сообщении #1084196 писал(а):

Объясните как все это взаимосвязано. Как из независимости получается невыводимость?

Потому что из истинных посылок нельзя вывести то, что в некоторых случаях (в некоторых моделях) является ложным.