2 x 2 = 4

[AGu]

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

1) Любое истинное арифметическое равенство доказуемо в IA.
2) В IA доказуемы только истинные арифметические равенства.
3) У IA есть одноэлементная модель, в связи с чем ни одно арифметическое неравенство (типа $\ulcorner 2 \urcorner \neq \ulcorner 3 \urcorner$) в IA не доказуемо.
4) Если к IA добавить аксиомы $0 \neq 0'$ и $(x' = y') \rightarrow (x=y)$, то в IA будут доказуемы в точности истинные арифметические неравенства.

Со всем согласен. (Сначала можно индукцией доказать, что для любых $n,m\in\mathbb N$ в ${\rm IA}$ доказуемы равенства $\ulcorner n\urcorner+\ulcorner m\urcorner=\ulcorner n+m\urcorner$ и $\ulcorner n\urcorner\times\ulcorner m\urcorner=\ulcorner n\times m\urcorner$, после чего рекурсией по сложности термов легко доказывается гипотеза 1.)

Обозначим через ${\rm BA}$ (Baby Arithmetic) результат добавления к ${\rm IA}$ аксиом $0\ne0'$ и $(x'=y')\rightarrow(x=y)$.

Несложно показать, что для любых $n,m\in\mathbb N$ из $n\ne m$ следует ${\rm BA}\vdash\bigl(\ulcorner n\urcorner\ne\ulcorner m\urcorner\bigr)$, откуда вытекает 4).

Выходит, что теория ${\rm BA}$ является полной для бескванторных предложений: для любого такого предложения $\varphi$ мы имеем ${\rm BA}\vdash\varphi$ или ${\rm BA}\vdash\neg\varphi$, причем ${\rm BA}\vdash\varphi$ равносильно $\mathbb N\vDash\varphi$.

Позволю себе еще чуток порезвиться в этой песочнице.

О полноте ${\rm BA}$ (для любых предложений, включая кванторные), разумеется, речи быть не может. Достаточно вспомнить Гёделя. Тем не менее неполноту ${\rm BA}$ можно установить и «без Гёделя». Предлагаю поразмышлять над следующей гипотезой (которую я, как мне кажется, могу доказать, чего и вам желаю).

Гипотеза 2.
${\rm BA}\nvdash(\forall\,x)(0+x=x)$

Иными словами, существует система $(X,{}',{+},{\times},0)$, которая удовлетворяет всем аксиомам ${\rm BA}$, но в которой $0+x\ne x$ для некоторого $x\in X$.

Это может показаться любопытным, ведь из установленного выше следует, что в ${\rm BA}$ доказуемо равенство $0+\ulcorner n\urcorner=\ulcorner n\urcorner$ для всех $n\in\mathbb N$. (В частности, в ${\rm BA}$ не работает так называемое $\omega$-правило.)

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

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

AGu в сообщении #334912 писал(а):

Не сомневаюсь, что логиками эта песочница уже многократно перекопана...

Угу. Каждый год на семинарах по матлогике с второкурсниками копаем В том числе и гипотезу 2...

AGu в сообщении #334912 писал(а):

но почему бы в ней не повозиться и нам, младенцам-любителям?

Всё, ухожу. Извините...

[neo66]

AGu в сообщении #334912 писал(а):

Гипотеза 2.
${\rm BA}\nvdash(\forall\,x)(0+x=x)$

Иными словами, существует система $(X,{}',{+},{\times},0)$, которая удовлетворяет всем аксиомам ${\rm BA}$, но в которой $0+x\ne x$ для некоторого $x\in X$.

Ну, как-то так?
Пусть $X$ состоит из "натуральных чисел" $\{0,1,2,3 \dots\}$ и "дубля" $\{\tilde 0,\tilde 1,\tilde 2,\tilde 3 \dots\}$ и правил
1. $m\times \tilde n = \tilde {(m\times n)}$
2. $\tilde m\times n = {(m\times n)}$
3. $m + \tilde n = \tilde {(m + n)}$
4. $\tilde m + n = {(m + n)}$

6. $\tilde m\times \tilde n = \tilde {(m\times n)}$
7. $\tilde m + \tilde n = \tilde {(m + n)}$
8. $m + n = {(m + n)}$
9. $m + n = {(m + n)}$

10. $ \tilde m'= \tilde {(m+1)}$
11. $m'=(m+1)$

Тогда, если не ошибаюсь, все тут непротиворечиво и $0 + \tilde0=\tilde0$.

[AGu]

neo66 в сообщении #335377 писал(а):

$0 + \tilde0=\tilde0$.

Ага. А нам надо $0+x\ne x$.

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

AGu в сообщении #334912 писал(а):

Со всем согласен...

А зря, поскольку $\mathbb{Z}_2 \models \mathrm{BA}$ Я там немного облажался

К BA надо ещё добавить что-то вроде $\exists z(x = y + z) \rightarrow \forall z (y \neq x + z)$. Вечером будет время, отпишусь подробнее.

[AGu]

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

$\mathbb{Z}_2 \models \mathrm{BA}$

Ага. Я сослепу принял $0\ne0'$ за $0\ne x'$.
Предлагаю отныне считать ${\rm BA}$ теорией именно с этой аксиомой. Иначе таки да, фигня.
Итак, аксиомы ${\rm BA}$:

$x' \ne 0$
$x'=y'\ \to\ x=y$
$x+0 = x$
$x+y' = (x+y)'$
$x\times 0 = 0$
$x\times y' = (x\times y)+x$

[neo66]

AGu в сообщении #335384 писал(а):

neo66 в сообщении #335377 писал(а):

$0 + \tilde0=\tilde0$.

Ага. А нам надо $0+x\ne x$.

Угу, ну это ничего. Полепим еще куличики. Чуть подправим.

Пусть $X$ состоит из "натуральных чисел" $\{0,1,2,3 \dots\}$ и "дубля" $\{\tilde 0,\tilde 1,\tilde 2,\tilde 3 \dots\}$ и правил:

1. $m\times \tilde n = \tilde {(m\times n)}$
2. $\tilde m\times n = {(m\times n)}$
3. $m + \tilde n = {(m + n)}$
4. $\tilde m + n = \tilde {(m + n)}$

6. $\tilde m\times \tilde n = \tilde {(m\times n)}$
7. $\tilde m + \tilde n = \tilde {(m + n)}$
8. $m + n = {(m + n)}$
9. $m + n = {(m + n)}$

10. $ \tilde m'= \tilde {(m+1)}$
11. $m'=(m+1)$

Тогда, аксиомы $\rm BA$ выполняются и $0 + \tilde0=0$.

[AGu]

Этот пример, кажись, можно «оптимизировать».
Если добавить к $\mathbb N$ два новых элемента $x$ и $y$
и доопределить сложение следующим образом

\begin{tabular}{|c|ccc|}\hline $+$ & $n$ & $x$ & $y$ \\ \hline $m$ & $m+n$ & $y$ & $x$ \\ $x$ & $x$ & $y$ & $x$ \\ $y$ & $y$ & $y$ & $x$ \\ \hline \end{tabular}

то аксиомы сложения будут выполняться, но $0+x=y\ne x$.
Думаю, и умножение можно доопределить, но лень.

Профессор, а Вы в песочнице какую контрмодель откапываете?

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

Мне песочница вот какая вспоминается...

Я историю плохо знаю, и оригинальную формулировку Курта Гёделя его теоремы о неполноте не помню. То, что сейчас проходят в НГУ на втором курсе --- это так называемая теорема Гёделя-Россера. Она утверждает, что любое эффективно (часто говорят "рекурсивно") перечислимое непротиворечивое расширение теории $\mathrm{PA}^-$ неполно. А что за теория $\mathrm{PA}^-$? Тут есть несколько вариантов. Приведу пару из книжек, имеющихся под рукой.

Вариант 1.

$$\def\lwedge{\mathop{\&}} \begin{array}{ll} 1.&x \leqslant x \\ 2.&x \leqslant y \lwedge y \leqslant z \rightarrow x \leqslant z \\ 3.&x \leqslant y \lwedge y \leqslant x \rightarrow x = y \\ 4.&x \leqslant y \vee y \leqslant x \\ 5.&0 \leqslant x \\ 6.&x \leqslant s(x) \lwedge \neg(x = s(x)) \\ 7.&x \leqslant y \lwedge \neg(x = y) \rightarrow s(x) \leqslant y \\ 8.&x + 0 = x \\ 9.&x + s(y) = s(x + y) \\ 10.&x \cdot 0 = 0 \\ 11.&x \cdot s(y) = x \cdot y + x \end{array} $$

Вариант 2.

$$\def\lwedge{\mathop{\&}} \begin{array}{ll} 1.&\neg (x = 0) \leftrightarrow \exists y (x = s(y)) \\ 2.&s(x) = s(y) \rightarrow x = y \\ 3.&x + 0 = 0 \\ 4.&x + s(y) = s(x + y) \\ 5.&x \cdot 0 = 0 \\ 6.&x \cdot s(y) = x \cdot y + x \\ 7.&x \leqslant y \leftrightarrow \exists z(x + z = y) \\ 8.&0 \leqslant x \\ 9.&x \leqslant x \\ 10.&x \leqslant y \lwedge y \leqslant z \rightarrow x \leqslant z \\ 11.&x \leqslant y \lwedge y \leqslant x \rightarrow x = y \\ 12.&x \leqslant y \vee y \leqslant x \end{array} $$

Возможны и другие варианты. Строятся они исходя из следующих соображений. Пусть $\mathfrak{M}$ и $\mathfrak{N}$ --- модели некоторой сигнатуры, в которую входит бинарное отношение $\leqslant$, являющееся на обоих моделях линейным порядком. Тогда $\mathfrak{M}$ называется концевым расширением $\mathfrak{N}$, если $\mathfrak{N}$ --- подмодель модели $\mathfrak{M}$, являющаяся начальным сегментом (то есть для любых $a \in \mathfrak{N}$ и $b \in \mathfrak{M}$ из $b \leqslant a$ следует $b \in \mathfrak{N}$). Ну и единственное, по сути, требование, исходя из которого строятся варианты теории $\mathrm{PA}^-$, заключается в следующем: каждая модель $\mathrm{PA}^-$ обязана являться концевым расширением стандартной модели арифметики $\mathbb{N}$.

В сигнатуру, как видите, включаем отношение $\leqslant$, функцию следования $s$ (то, что выше в теме обозначается штрихом), сложение, умножение и константу $0$. Функция $s$ плюс константа $0$ дают нумералы. В аксиомы, как несложно заметить, включаем теорию $\mathrm{IA}$, аксиомы линейного порядка плюс кое-что ещё...

А с второкурсниками мы каждый год копаем следующее: в $\mathrm{PA}^-$ (в обоих из приведённых выше вариантов) недоказуемы коммутативности, ассоциативности обоих операций, их дистрибутивность, равенство $0 + x = x$, неравенство $x \leqslant x^2$ и прочие подобные вещи. Типа очень слабая такая теория, если разобраться.

Естественно, раз равенство $0 + x = x$ недоказумо в $\mathrm{PA}^-$, то оно недоказуемо и в $\mathrm{IA}$, и в $\mathrm{BA}$ тоже...

[AGu]

Сасибо, Профессор.
Теперь я, пожалуй, спрячу голову в песок.

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

Вот несколько типичных задач с зачёта (подчёркивания обозначают нумералы):

Первый вариант теории:

1) $\mathrm{PA}^- \vdash (x+y=s(x)) \rightarrow (\underline{1} \leqslant y)$.
2) $\mathrm{PA}^- \vdash (x \cdot y = 0) \rightarrow (y=0 \vee \underline{2} \leqslant y \vee x=0)$.
3) $\mathrm{PA}^- \not\vdash (x \cdot y = 0) \rightarrow (x=0 \vee y=0)$.
4) $\mathrm{PA}^- \vdash (x \cdot s(y) = 0) \rightarrow (x = 0 \vee \underline{3} \leqslant x)$.
5) $\mathrm{PA}^- \not\vdash x \leqslant x \cdot x$.

Второй вариант теории:

1) $\mathrm{PA}^- \vdash s(x) \leqslant s(y) \rightarrow x \leqslant y$.
2) $\mathrm{PA}^- \vdash \forall z(z \leqslant x \vee s(x) \leqslant z)$.
3) $\mathrm{PA}^- \vdash x \leqslant y \rightarrow s(x) \leqslant s(y)$.
4) $\mathrm{PA}^- \vdash \exists y(y \neq 0 \mathop{\&} x=x+y) \rightarrow x=s(x)$.
5) $\mathrm{PA}^- \vdash x \cdot y = 0 \rightarrow x = 0 \vee y = 0$.
6) $\mathrm{PA}^- \vdash \neg \exists x(x \cdot \underline{2} = \underline{1})$.
7) $\mathrm{PA}^- \vdash \neg \exists x(\underline{2} \cdot x = \underline{1})$.
8) $\mathrm{PA}^- \vdash \forall x(x \neq s(x) \rightarrow x + \underline{1} \neq x + \underline{2})$.
9) $\mathrm{PA}^- \vdash \forall x(\underline{2} \leqslant x \rightarrow \exists y(x = y + \underline{2}))$.
10) $\mathrm{PA}^- \vdash \forall x(x \neq 0 \mathop{\&} x \neq s(x) \rightarrow \exists y(x = s(y) \mathop{\&} x \neq y))$.
11) $\mathrm{PA}^- \not\vdash (x+y=x) \rightarrow (y=0)$.
12) $\mathrm{PA}^- \not\vdash (x \cdot \underline{3} = x) \rightarrow (x = 0)$.

AGu в сообщении #337038 писал(а):

Сасибо, Профессор.
Теперь я, пожалуй, спрячу голову в песок.

Не прячьте, пожалуйста. Там ведь всё довольно просто, если разобраться