История изменений
Исправление a--, (текущая версия) :
Берем аксиоматику Пеано; поскольку программистом странно видеть, когда имена объектов начинаются на цифру, у нас они будут называться так:
число_1
число_2
число_3
число_4
Наши аксиомы:
АКСИОМА: есть число_1, оно натуральное число
АКСИОМА: есть операция next
АКСИОМА: все наши объекты (натуральные числа) это результат операции next над натуральными числами либо число_1
АКСИОМА: Равенство чисел: x=y если и только если x это число_1 и y это число_1 или x это next(a) и y это next(b) и a=b
ОПРЕДЕЛЕНИЕ: число_2 это next(число_1)
ОПРЕДЕЛЕНИЕ: число_3 это next(число_2)
ОПРЕДЕЛЕНИЕ: число_4 это next(число_3)
Далее определяем операцию prev
ОПРЕДЕЛЕНИЕ: prev(y) это x если и только если next(x)=y
ТЕОРЕМА: операция prev определена для всех натуральных чисел, кроме число_1
ДОКАЗАТЕЛЬСТВО: очевидно (смотрим на аксиомы).
Нам достаточно что:
ТЕОРЕМА: prev(число_2)=число_1
ТЕОРЕМА: prev(число_3)=число_2
ТЕОРЕМА: prev(число_4)=число_3
Далее определяем сложение add(x,y)
ОПРЕДЕЛЕНИЕ: add(x,число_1) это next(x)
ОПРЕДЕЛЕНИЕ: add(x,y) это next(x,prev(y))
Можно доказать, что add определена корректно и для всех натуральных чисел, но тут опять нам это не нужно. Нам достаточно что
ТЕОРЕМА: add(число_2, число_2)=число_4
ДОКАЗАТЕЛЬСТВО: add(число_2, число_2)=next(add(число_2,число_1))=next(next(число_2))=next(число_3)=число_4
Далее определяем сложение add(x,y)
ОПРЕДЕЛЕНИЕ: mul(x,число_1) это x
ОПРЕДЕЛЕНИЕ: mul(x,y) это add(mul(x,prev(y)),x)
Можно доказать, что mul определена корректно и для всех натуральных чисел, но тут опять нам не нужно. Нам достаточно что
ТЕОРЕМА: mul(число_2, число_2)=число_4
ДОКАЗАТЕЛЬСТВО: mul(число_2, число_2)=add(mul(число_2,число_1),число_2)=add(число_2, число_2)=число_4
Исправление a--, :
Берем аксиоматику Пеано; поскольку программистом странно видеть, когда имена объектов начинаются на цифру, у нас они будут называться так:
число_1
число_2
число_3
число_4
Наши аксиомы:
АКСИОМА: есть число_1, оно натуральное число
АКСИОМА: есть операция next
АКСИОМА: все наши объекты (натуральные числа) это результат операции next над натуральными числами либо число_1
АКСИОМА: Равенство чисел: x=y если и только если x это число_1 и y это число_1 или x это next(a) и y это next(b) и a=b
ОПРЕДЕЛЕНИЕ: число_2 это next(число_1)
ОПРЕДЕЛЕНИЕ: число_3 это next(число_2)
ОПРЕДЕЛЕНИЕ: число_4 это next(число_3)
Далее определяем операцию prev
ОПРЕДЕЛЕНИЕ: prev(y) это x если и только если next(x)=y
ТЕОРЕМА: операция prev определена для всех натуральных чисел, кроме число_1
ДОКАЗАТЕЛЬСТВО: очевидно (смотрим на аксиомы).
Нам достаточно что:
ТЕОРЕМА: prev(число_2)=число_1
ТЕОРЕМА: prev(число_3)=число_2
ТЕОРЕМА: prev(число_4)=число_3
Далее определяем сложение add(x,y)
ОПРЕДЕЛЕНИЕ: add(x,число_1) это next(x)
ОПРЕДЕЛЕНИЕ: add(x,y) это next(x,prev(y))
Можно доказать, что add определена корректно и для всех натуральных чисел, но тут опять нам это не нужно. Нам достаточно что
ТЕОРЕМА: add(число_2, число_2)=число_4
ДОКАЗАТЕЛЬСТВО: add(число_2, число_2)=next(add(число_2,число_1))=next(next(число_2))=next(число_3)=число_4
Далее определяем сложение add(x,y)
ОПРЕДЕЛЕНИЕ: mul(x,число_1) это x
ОПРЕДЕЛЕНИЕ: mul(x,y) это add(mul(x,prev(y)),y)
Можно доказать, что mul определена корректно и для всех натуральных чисел, но тут опять нам не нужно. Нам достаточно что
ТЕОРЕМА: mul(число_2, число_2)=число_4
ДОКАЗАТЕЛЬСТВО: mul(число_2, число_2)=add(mul(число_2,число_1),число_2)=add(число_2, число_2)=число_4
Исходная версия a--, :
Берем аксиоматику Пеано; поскольку программистом странно видеть, когда имена объектов начинаются на цифру, у нас они будут называться так:
число_1
число_2
число_3
число_4
Наши аксиомы:
АКСИОМА: есть число_1, оно натуральное число
АКСИОМА: есть операция next
АКСИОМА: все наши объекты (натуральные числа) это результат операции next над натуральными числами либо число_1
АКСИОМА: Равенство чисел: x=y если и только если x это число_1 и y это число_1 или x это next(a) и y это next(b) и a=b
ОПРЕДЕЛЕНИЕ: число_2 это next(число_1)
ОПРЕДЕЛЕНИЕ: число_3 это next(число_2)
ОПРЕДЕЛЕНИЕ: число_4 это next(число_3)
Далее определяем операцию prev
ОПРЕДЕЛЕНИЕ: prev(y)=x если и только если next(x)=y
ТЕОРЕМА: операция prev определена для всех натуральных чисел, кроме число_1
ДОКАЗАТЕЛЬСТВО: очевидно (смотрим на аксиомы).
Нам достаточно что:
ТЕОРЕМА: prev(число_2)=число_1
ТЕОРЕМА: prev(число_3)=число_2
ТЕОРЕМА: prev(число_4)=число_3
Далее определяем сложение add(x,y)
ОПРЕДЕЛЕНИЕ: add(x,число_1) это next(x)
ОПРЕДЕЛЕНИЕ: add(x,y) это next(x,prev(y))
Можно доказать, что add определена корректно и для всех натуральных чисел, но тут опять нам это не нужно. Нам достаточно что
ТЕОРЕМА: add(число_2, число_2)=число_4
ДОКАЗАТЕЛЬСТВО: add(число_2, число_2)=next(add(число_2,число_1))=next(next(число_2))=next(число_3)=число_4
Далее определяем сложение add(x,y)
ОПРЕДЕЛЕНИЕ: mul(x,число_1) это x
ОПРЕДЕЛЕНИЕ: mul(x,y) это add(mul(x,prev(y)),y)
Можно доказать, что mul определена корректно и для всех натуральных чисел, но тут опять нам не нужно. Нам достаточно что
ТЕОРЕМА: mul(число_2, число_2)=число_4
ДОКАЗАТЕЛЬСТВО: mul(число_2, число_2)=add(mul(число_2,число_1),число_2)=add(число_2, число_2)=число_4