Есть ли в этом учебнике ошибка об арифметике Пеано?

Question

Я столкнулся с этим сомнением в открытом вводном курсе по интро-логике, предложенном Stanford Uni.

В разделе 9.4 этого учебника здесь: http://logic.stanford.edu/intrologic/secondary/notes/chapter_09.html

Это говорит:

Аксиомы, показанные здесь, определяют то же самое отношение в терминах 0 и s (где функциональная постоянная буква s ниже представляет функцию-преемник, например, s (0) = 1, s (1) = 2, s (2) = 3)

∀x.same (х, х)

∀x. (¬same (0, s (x)) ∧ ¬same (s (x), 0))

∀x.∀y. (¬same (x, y) ⇒ ¬same (s (x), s (y)))

Как я понимаю,

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

Второй говорит, что ни один из преемников любого числа не равен 0.

Третий говорит, что если два числа не совпадают, то их преемники не совпадают. Например, если 1≠3, то 2≠4.

Тем не менее, я думаю, что третье предложение должно быть двухусловным, потому что, если я не ошибаюсь, определение не охватывает случай, когда свидетельствующее число меньше заданного числа, в противном случае можно сказать, если 2 2 4, то 1=3.

Так что я подумал: это ошибка в учебнике или что-то не так в моих рассуждениях?

Answer 1

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

Формальное доказательство будет включать в себя аксиомы, которые определяют функцию преемника. Кто-то, более привыкший к использованию автоматических пруверов или просто хорошо изучающий логику, мог бы выполнить такое формальное доказательство.

Вот только набросок доказательства. Он использует символ "=" для обозначения термина равенство, то есть u = v означает, что u и v являются синтаксически идентичными терминами, написанными с использованием символов 0 и s (). Также " u < v " означает, что u и v оба являются основными терминами, и u имеет строго меньшее применение s (), чем v.

предполагать

∀x.∀y.(¬ то же самое (s(x),s(y)) ⇒ ¬ то же самое (x, y))

не выполняется, то существуют такие члены x0 и y0, что

одинаковые (x0, y0) и ¬ одинаковые (s (x0), s (y0)).

Поскольку s (x0) является функцией, из ¬same(s(x0),s(y0)) и ∀x.same(x,x) следует, что x0 и y0 - два разных члена. Сначала рассмотрим случай, когда x0 n приложений s () и n > 0. Другой случай, когда y0

Подставляя s (... s (x0)) для y0 в то же самое (x0, y0), мы получаем то же самое (x0, s (... s (x0))).

Также x0 = s(...s(0)), где есть m приложений s () для некоторого неотрицательного целого числа m. Используя третью аксиому в указанном направлении, мы можем сказать, что если то же самое (s (u), s (v)), то то же самое (u, v). Таким образом, из того же (x0, s (... s (x0))) мы можем "убрать" m приложений s (), чтобы получить

то же самое (0, s (... s (0))), где во втором аргументе есть n применений s (). Это противоречит второй аксиоме. QED