2 x 2 = 4

[AGu]

Сомневался, стоит ли постить. Решил, сюда. (А куда еще?)
Итак, фрагмент сегодняшнего ICQ-диалога (с друганом-айтишником)...

— Это очевидно как $2\times2=4$.
— Нифига не очевидно.
— Фига, очевидно.
— Докажи.
— Что доказать?
— Что очевидно.
— Что что очевидно?
— Что $2\times2=4$.
— Это очевидно.
— Очевидно то, что легко доказать.
— Ну да.
— Вот и докажи.
— Доказать, что $2\times2=4$?
— Ага.
— В какой теории?
— В любой.
— Тогда я выбираю аксиому $2\times2=4$. Доказывать?
— Нет такой аксиомы.
— Ты же сказал, что в любой теории.
— В любой известной.
— Их много, известных.
— Ну вот тебе аксиомы (из тырнета):

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

— Не густо. Там наверняка еще и другие аксиомы есть.
— Тебе аксиомы $2\times2=4$ не хватает?
— Не, я серьезно. Хотя... Щас, минутку...
— Прошла твоя минутка.

[neo66]

$2+2=2+1'=(2+1)'=(2+0')'=(2+0)''=2''=4$
$2 \times 1 = 2 \times 0'=(2 \times 0) + 2 = 2$
$2 \times 2 = 2 \times 1'= (2 \times 1) +2 = 2 + 2=4$

[Mathusic]

del/ не та теория

[AGu]

Мелочь, конечно, но...

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

$(2 \times 0) + 2 = 2$

не доказано.

[Kitozavr]

Говорят два программиста:
- Скажи, чем программист отличается от простого смертного?
- Например, он может ответить на вопрос в котором уже заложен ответ
- Это как?
- Чему равно $2\times2= 4$?
- Ну конечно True!

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

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

Мелочь, конечно, но...

не доказано.

Ага, кусочек пропущен

$$ (2 \times 0) + 2 = 0 + 2 = 0 + 1' = (0+1)' = (0 + 0')' = (0+0)'' = 0'' = 1' = 2 $$

И ниже ещё один, равенство $2 \times 1 = 2$ тоже надо расписывать

А почему в ZF никто не хочет? Лень писать?

[neo66]

(Оффтоп)

Ну, Вы, господа, зануды.
Хотя, конечно, правы.

[AGu]

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

Ну, Вы, господа, зануды.

Да, мы такие. И этим гордимся!

Развлечения ради предлагаю чуток поразвивать эту детскую задачку.

Определение 1.
Обозначим через ${\rm IA}$ (Infant Arithmetic) теорию сигнатуры $(\,{}',{+},{\times},0)$
с уже упомянутой аксиоматикой:

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

Определение 2.
Для произвольного $a\in\mathbb N$ обозначим символом $\ulcorner a\urcorner$ терм $0^{\prime\prime\,\cdots\,\prime}$ с $a$ штрихами.
(Такие термы обычно называют нумералами или стандартными нумералами.)
В частности, $\ulcorner 0\urcorner$ — это $0$, $\ulcorner 1\urcorner$ — это $0'$, $\ulcorner 2\urcorner$ — это $0''$ и т.д.

Выше мы показали, что ${\rm IA}\vdash\bigl[\ulcorner2\urcorner\times\ulcorner2\urcorner=\ulcorner4\urcorner\bigr]$.
Иными словами, равенство $2\times 2=4$ доказуемо в ${\rm IA}$.
В этой связи возникает вопрос: какие равенства доказуемы в ${\rm IA}$?
Например, доказуемо ли, что $(2+3)\times4=20$, $6+\bigl((5\times2)\times2\bigr)=2\times13$ и т.п.?

Поскольку $\mathbb N$ является моделью ${\rm IA}$, ясно, что
в ${\rm IA}$ доказуемы только истинные арифметические равенства.
Следующая гипотеза уточняет это наблюдение:

Всякое истинное арифметическое равенство доказуемо в ${\rm IA}$.

Если это так, то истинность какого-либо равенства
равносильна доказуемости этого равенства в ${\rm IA}$.

Горделиво занудствуя, привожу формальный аналог выдвинутой гипотезы:

Гипотеза 1.
Пусть $\sigma(x_1,\dots,x_m)$ и $\tau(y_1,\dots,y_n)$ — произвольные термы сигнатуры $({+},{\times})$
со свободными переменными $x_1,\dots,x_m$ и $y_1,\dots,y_n$
и пусть $a_1,\dots,a_m,b_1,\dots,b_n\in\mathbb N$ таковы, что $\mathbb N\vDash\bigl[\sigma(a_1,\dots,a_m)=\tau(b_1,\dots,b_n)\bigr]$.
Тогда ${\rm IA}\vdash\bigl[\sigma(\ulcorner{a_1}\urcorner,\dots,\ulcorner{a_m}\urcorner)=\tau(\ulcorner{b_1}\urcorner,\dots,\ulcorner{b_n}\urcorner)\bigr]$.

[worm2]

А можно то же самое переформулировать по-рабоче-крестьянски:
Пусть заданы функции $f, g: \mathbb{N}_0^2\to\mathbb{N}_0, h: \mathbb{N}_0\to\mathbb{N}_0$, удовлетворяющие следующим уравнениям для всех $x, y \in \mathbb{N}_0$:
1) $f(x,0)=x$
2) $f(x,h(y))=h(f(x,y))$
3) $g(x,0)=0$
4) $g(x,h(y))=f(g(x,y),x)$
Доказать, что для любых $x, y \in \mathbb{N}_0$ выполняется:
1) $f(h^x(0),h^y(0))=h^{x+y}(0)$
2) $g(h^x(0),h^y(0))=h^{xy}(0)$, где через $h^n(x)$ обозначено $h(h(\dots(x)\dots))$ ($n$ пар скобок), $h^0(x)=x$.

-- Ср июн 23, 2010 18:39:03 --

($\mathbb{N}_0 = \mathbb{N} \cup \{0\}$)

[AGu]

worm2 в сообщении #334144 писал(а):

А можно то же самое переформулировать по-рабоче-крестьянски:

Редукция к «двучленам» понятна. И я согласен, что достаточно рассматривать лишь не более чем счетные модели (теорема Лёвенгейма — Сколема). Но ведь у ${\rm IA}$ есть и конечные модели. С ними точно все очевидно? (Может, все конечные модели ${\rm IA}$ одноэлементны? Не знаю, не думал.)

worm2 в сообщении #334144 писал(а):

($\mathbb{N}_0 = \mathbb{N} \cup \{0\}$)

Я изначально предполагал, что $0\in\mathbb N$. (Впрочем, не суть.)

[worm2]

AGu писал(а):

Но ведь у ${\rm IA}$ есть и конечные модели. С ними точно все очевидно? (Может, все конечные модели ${\rm IA}$ одноэлементны? Не знаю, не думал.)

Я тоже не думал. Наверное, модель вычислений с остатком (по любому модулю) будет адекватной, т.е. характеристика поля здесь однозначно не определяется (Вы ведь что-то подобное имели в виду?).

Согласен, что моя формулировка не эквивалентна Вашей. Я вообще не очень владею матлогикой и её приёмами. Просто мне показалось, что в такой формулировке задача будет тоже интересной и доступной более широкому кругу, вроде меня

[Lyosha]

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

Определение 1.
Обозначим через ${\rm IA}$ (Infant Arithmetic) теорию сигнатуры $(\,{}',{+},{\times},0)$
с уже упомянутой аксиоматикой:

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

Я прошу прощения за детский вопрос,но в теории сигнатуры символы $($ и$)$ должны присутствовать?

[neo66]

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

Всякое истинное арифметическое равенство доказуемо в ${\rm IA}$.

Просветите, пожалуйста. Что означает истинное арифметическое равенство?

[AGu]

worm2 в сообщении #334186 писал(а):

AGu писал(а):

Может, все конечные модели ${\rm IA}$ одноэлементны? Не знаю, не думал.

Наверное, модель вычислений с остатком (по любому модулю) будет адекватной

Хорошая мысль. (Жаль, что не моя. )
Стало быть, анализ интерпретаций сигнатуры только на $\mathbb N$ не будет исчерпывающим.

Lyosha в сообщении #334197 писал(а):

Я прошу прощения за детский вопрос,но в теории сигнатуры символы $($ и$)$ должны присутствовать?

Эти символы входят в алфавит языка теории (наряду с символами переменных, кванторов и прочих логических связок), но в сигнатуру не включаются. В сигнатуру включают только те символы, которые в принципе допускают разные интерпретации. К этим символам относятся символы операций, отношений и констант. Кстати, символу равенства обычно не позволяют интерпретироваться как-то нестандартно, и поэтому его тоже не включают в сигнатуру. (Но если позволяют, — включают.)

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

Просветите, пожалуйста. Что означает истинное арифметическое равенство?

Ответ на этот вопрос есть в приведенном выше формальном аналоге гипотезы. Грубо говоря, истинное арифметическое равенство — это истинное в $\mathbb N$ равенство двух (синтаксически корректных) выражений, составленных из натуральных чисел, операций $+$, $\times$ и скобок. (А строго говоря — см. тот формальный аналог.)

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

Ну вы, ребята, развели тут флейм...

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 будут доказуемы в точности истинные арифметические неравенства.