2. Доказательство того, что сумма и разность не представимы в формализме системы (В); рекурсивные равенства для сложения как аксиомы; система (D).

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

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

переводимо в конъюнкцию неравенств

Для неравенства, не содержащего никаких переменных, кроме , имеются следующие возможности:

Либо оно является нумерическим; тогда оно истинно или ложно. Либо оно имеет вид

тогда оно переводимо в нумерическое неравенство

Либо оно имеет вид

тогда, если оно переводимо в ложное неравенство

если же оно переводимо в некоторое неравенство

неравенство такого рода мы будем называть верхней оценкой для а.

Либо оно имеет вид

тогда, если оно переводимо в истинное неравенство

если же то оно переводимо в некоторое неравенство

неравенство такого рода мы будем называть нижней оценкой для а.

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

Рассмотрим последний из перечисленных случаев. Здесь мыслимы следующие две возможности. Либо верхних оценок для а нет по крайней мере в одном из дизъюнктивных членов; тогда при любой подстановке цифры, большей чем определенная цифра 0), эта формула переходит в некоторую истинную формулу. Либо же верхняя оценка для а встречается в каждом дизъюнктивном члене; тогда при любой подстановке какой-либо цифры, большей чем определенная цифра эта формула переходит в некоторую ложную формулу.

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

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

Теперь на основе этого факта легко показать, что функции представимы в формализме системы (В).

В самом деле, допустим, что равенство

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

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

Тогда формула

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

либо для всех достаточно больших выводимо отрицание этой формулы, а значит, и формула

Таким образом, если мы выберем цифру достаточно большой, то для цифры , являющейся значением средствами системы (В) будут выводимы либо обе формулы

либо обе формулы

В первом случае, вследствие выводимости формулы

по теореме о частичной редукции мы нашли бы цифру I, такую что средствами системы (В) была бы выводима формула

во втором случае вследствие выводимости формулы

была бы выводимой формула

Но ни формула

ни формула

не могут быть выведены средствами системы (В).

Действительно, так как является значением то ввиду того, что формула

представляет равенство

формула

должна быть выводимой средствами системы (В). Из того же самого свойства формулы следует, что и формула

выводима, так как при больше значения , а в случае оно меньше этого значения и, значит, в любом случае отлично от значения Таким образом, и в случае выводимости

и в случае выводимости

средствами системы (В) была бы выводима некоторая формула вместе с ее отрицанием, между тем как мы ранее показали, что система (В) непротиворечива.

Тот факт, что равенство

также не представимо в формализме системы (В) никакой формулой

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

Для того чтобы убедиться в этом, нам не нужно снова повторять проведенное рассуждение, а достаточно лишь заметить, что справедливость равенства

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

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

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

В этой системе кроме аксиомы равенства (аксиома оказывается излишней ввиду наличия аксиомы ) имеются обе пеановские аксиомы которые в системе были заменены рекурсивными равенствами для и формулой а также рекурсивные равенства для а и аксиома индукции.

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

Основываясь на этом определении, мы можем вывести формулы

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

третья — с помощью формулы

выводимой из формул

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

и

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

Тем самым все аксиомы системы (В) оказываются выводимыми средствами системы с учетом явного определения выражения

В формализме системы равенство

может быть представлено формулой

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

либо формулу

в зависимости от того, совпадает или не совпадает со значением

Если бы мы захотели добавить к системе в качестве терма, то это проще всего было бы сделать, добавив к аксиомам этой системы формулы

и

В получившейся таким образом системе посредством равенства

можно было бы явно определить функцию и на основании этого определения вывести рекурсивные равенства для и Тем самым из этой системы можно было бы вывести все формулы системы (С).