Первая аксиома Пеано

[Someone]

Прежде всего, нужно иметь в виду, что формальная арифметика обязана включать в себя исчисление высказываний и исчисление предикатов с их аксиомами и правилами вывода. Эти исчисления могут быть как классическими, так и интуиционистскими.

vesennygnom в сообщении #1403677 писал(а):

это значит изучить остальные формализации $\mathbb{N}$ ?

Про все "остальные" ничего сказать не могу, но две можно найти в книге

П. Дж. Коэн. Теория множеств и континуум гипотеза. "Мир", Москва, 1969. Глава I, § 6, системы $Z_1$ и $Z_2$.

Одна формализация есть в книге

С. К. Клини. Математическая логика. "Мир", Москва, 1973. Глава IV, § 38.

Ещё одна — в книге

Е. Расёва, Р. Сикорский. Математика метаматематики. "Наука", Москва, 1972. Глав V, § 13.

Если хорошо поискать, то, наверное, можно и ещё найти.

[vesennygnom]

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

[Booker48]

vesennygnom
Посмотрите статью В. Успенского. Там по оглавлению понятно, что именно смотреть.

[arseniiv]

vesennygnom в сообщении #1403677 писал(а):

Где то читал прочитал про формализацию Пеано и меня заинтересовала эта рекурсивная машина.

М-м, ну это ещё не «рекурсивная машина». Рекурсия — это способ определения функций от индуктивно заданного множества. (Тут она параллельна индукции, дающей доказывать истинность предикатов для всех элементов такого множества.) Вот определение сложения как $m + 0 = m,\; m + Sn = S(m + n)$ — рекурсивное (по второму аргументу $+$, а первый фиксирован).

[vesennygnom]

Цитата:

Рекурсия — это способ определения функций от индуктивно заданного множества.

эт да с точки зрения математика))
объясню на примере

def sum(num, numToReach):
     if num == numToReach:
          return num
     return sum(n+1, numToReach)

это типа то о чем говорит Пеано. Но тут есть сравнение с образцом... Как мы узнаем что инкременту пора остановиться?

[Someone]

vesennygnom в сообщении #1403865 писал(а):

это типа то о чем говорит Пеано. Но тут есть сравнение с образцом... Как мы узнаем что инкременту пора остановиться?

Как только левая пятка чесаться начнёт, так сразу и останавливаемся.

[arseniiv]

vesennygnom в сообщении #1403865 писал(а):

это типа то о чем говорит Пеано

Если функция называется как надо, то нет, это не сумма.

Если так хочется залезать в программирование, лучше взять индуктивное определение типа натуральных чисел на хаскеле:

data Nat = Z | S Nat

Это определение даёт нам почти всё, что описывается теми пятью аксиомами:
(1) элемент Z :: Nat,
(2) функцию S :: Nat -> Nat,
(3) то, что S n не совпадает с Z никогда,
(4) то, что S m совпадает с S n лишь в случае, если совпадают m и n,
(5) то, что можно определять функции от Nat отдельно для случаев Z и S n.

Правда, (5) даёт вещь слабее индукции (только сопоставление с конструкторами Nat), потому что сам язык не создавался для чистоты таких иллюстраций и позволяет вставлять рекурсивные вызовы куда попало и какого угодно вида (как обычно бывает и в других) и тем выходит за рамки рассматриваемого. Лучшей альтернативой было бы определить функцию свёртки

foldNat :: a -> (a -> a) -> Nat -> a
foldNat z s Z = z
foldNat z s (S n) = s (foldNat z s n)

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