§ 2. Дедуктивное построение арифметики на основе системы аксиом (Z) с добавлением формализованного понятия наименьшего числа

1. Понятие «меньше»; сравнения; деление с остатком; делимость; взаимно простые числа.

Для введения функции мы из арифметики использовали здесь только аксиомы системы (В). Теперь мы добавим рекурсивные равенства для сложения и умножения и таким образом перейдем от системы (В) к системе Значение функциональной конструкции полностью раскроется только в рамках этого формализма. В частности, мы покажем, что с помощью функции все остальные рекурсивные определения можно будет заменить явными определениями.

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

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

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

а после этого, используя связанные переменные, мы ввели его при помощи функции а посредством определения

Это последнее определение мы и возьмем за основу для дальнейшего.

Из этого определения могут быть получены [как мы показалв в гл. VII при рассмотрении системы ] формулы а также

из которых дальше (как было установлено в гл. VI) могут бьгп выведены формулы

Кроме того, к этому могут быть добавлены формулы

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

Мы начнем теперь с определения сравнения по модулю

которое формулируется следующим образом:

Из этого определения, в силу законов для сложения и умножения, а также формул

могут быть получены следующие формулы:

Понятие сравнения по какому-либо модулю находится в тесной связи с операцией деления. От деления нам нужно здесь лишь понятие остатка. Функцию изображающую остаток от деления а на мы введем с помощью следующего явного определения:

Здесь мы впервые встречаемся с примером определения арифметической функции через функцию Формальные свойства определенной таким образом функции должны получаться с использованием формул В рассматриваемом случае нам будут нужны только первые две из них. Если мы подставим в вместо формульной переменной формулу

то, используя определяющее функцию равенство, мы получим

Затем из равенства

средствами исчисления предикатов мы получим формулу

тем самым мы получаем формулу

а отсюда, используя определение сравнения, получаем

Теперь возьмем формулу Прежде всего, подставим в нее вместо а переменную а вместо именной формы мы снова

подставим формулу

это дает нам

С другой стороны, применив соответствующие законы для сложения и умножения, мы получим формулу

а из нее — средствами исчисления предикатов — формулу

Фигурирующую здесь в качестве посылки формулу

мы уже вывели ранее. Тем самым мы получаем

а эта формула вместе с ранее полученной формулой

дает формулу

из которой мы получим, далее,

С помощью формулы

которая выводится из эквивалентности

мы теперь получим

а отсюда средствами исчисления предикатов —

Если мы еще раз воспользуемся эквивалентностью

то придем к формуле

а из нее, произведя контрапозицию и использовав дизъюнкцию

получим формулу

Эта формула и является изображением результата нашего применения формулы Вместе со сравнением

она дает нам полную характеристику функции Формально это обстоятельство выражается выводимостью формулы

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

Из формулы

можно, кроме того, вывести эквивалентность

которую в рекурсивной арифметике мы брали в качестве определения сравнения.

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

Для достижения поставленной нами цели требуется формализация понятий делимости, взаимной простоты и наименьшего общего кратного. Для делимости мы возьмем применяемый иногда в теории чисел символ а (а делит определение которого имеет вид

Из этого определения могут быть выведены следующие эквивалентности:

затем мы можем получить формулы

Из эквивалентности

можно также получить

С целью формализации понятия «а взаимно просто с мы сформулируем следующее определение:

Из этого определения легко получить следующие формулы:

Несколько более трудным делом является вывод свойства симметрии, выражаемого формулой

Этот вывод протекает с использованием следующих формул:

Из формулы

пользуясь определением мы получим

Если воспользоваться формулой

то получится