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

Я столкнулся с этим сомнением на открытом онлайн-курсе по интрологике, предлагаемом Стэнфордским университетом.

По разделу 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,x)

∀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≠4, то 1=3.

Поэтому я задался вопросом, это ошибка в учебнике или что-то не так с моими рассуждениями.


logic first-order-logic peano-numbers
person badbye    schedule 22.07.2016    source источник
comment
Кажется, это не про программирование. Вы можете попробовать задать вопрос на math.stackexchange.com.   -  person OneCricketeer    schedule 22.07.2016

Ответы (1)


arrow_upward
1
arrow_downward

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

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

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

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

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

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

тот же(x0,y0) и ¬same(s(x0),s(y0)).

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

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

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

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

person Dmitri Chubarov    schedule 24.07.2016