3. Функция w(A); формализация понятия наименьшего числа с помощью функции mxA(x); формулы однозначности.

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

Формулы единственности для нее запишутся в виде

Обе они могут быть выведены с помощью аксиом равенства. Вывод первой формулы протекает следующим образом.

Из первой аксиомы равенства подстановкой и добавлением посылок получаем

Из тождественной формулы

подстановкой получаем

Полученные формулы по схеме конъюнкции дают

далее, из формулы (b) подстановкой получается формула

которая вместе с предыдущей формулой по правилу силлогизма дает

Аналогичным образом мы получим и формулу

Теперь по схеме для дизъюнкции можно получить формулу

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

Совершенно аналогичным образом протекает вывод второй формулы единственности: с одной стороны, ее можно вывести с посылкой А, а с другой стороны, с посылкой Вместо первой аксиомы равенства, используемой в доказательстве первой формулы, здесь используется формула

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

а также аналогичная формула с посылкой вместо формулы (Ь) здесь используются схема (а) и правило переименования.

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

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

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

а из них, применив формулу

получим эквивалентность

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

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

в которые вместо можно будет снова подставить какую-нибудь формулу Тогда

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

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

Здесь снова вместе можно будет подставить какую-нибудь конкретную формулу и тогда

изобразит нам значение или 1 в зависимости от того, верен предикат для всех элементов индивидной области или же он неверен по крайней мере для одного из них.

При введении функции и при выводе характеризующих ее формул

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

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

выведена формула

изображающая принцип наименьшего числа. Если формулу

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

Из этой формулы с помощью схемы мы получим формулу

Применим -правило к формуле

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

Упомянутые выводы могут быть получены средствами исчисления предикатов с помощью формул

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

Если (с помощью подстановок) мы поменяем в ней местами переменные то получим

Взяв обе полученные формулы, мы с помощью исчисления высказываний получим формулу

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

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

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

выражение

может быть введено в качестве -терма. В качестве единственной свободной переменной в нем фигурирует формульная переменная А с одним аргументом. Мы возьмем для этого терма в качестве сокращения символ

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

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

Если мы разобьем эту конъюнкцию на члены и переименуем переменную то получим

Теперь учтем уже использовавшуюся ранее (при выводе второй формулы единственности) формулу

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

а эта последняя вместе с упоминавшейся выше формулой

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

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

которая выражает тот факт, что для свойства которое не выполняется ни для какого числа, принимает в качестве значения 0.

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

так как это последнее, во-первых, применимо лишь к предикатам специального типа и, кроме того, оно содержит ограничение на интервал фигурирующих здесь чисел, которые должны не превосходить k.

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

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

при незатронутых формульных переменных вывести равенство

Для этого мы сначала получим из формулы

которые совместно друг с другом дадут

Теперь мы воспользуемся формулой

из которой могут быть получены формулы

Первая из них в сочетании с формулами

получающимися из дает формулу

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

так что в целом мы получим

а из нее, в сочетании с выведенной выше формулой

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

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

мы получим

а эта формула в сочетании с получающимися из формулами

и с формулой

Но две полученные нами формулы

и

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

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

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

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

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

Прежде всего, с учетом выведенных формул единственности, -правило дает нам формулы

Из формулы

может быть получена формула

откуда, далее, получаем

а эта формула вместе с формулами

дает нам

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

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

Заметим, что в этом выводе формулу

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

Из этого обстоятельства вытекает, что в случае выводимости формул единственности для и для формула

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

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

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

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

Действительно, в этом случае, согласно -правилу, мы получим

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

так что мы будем иметь

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

так что мы действительно приходим к равенству

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

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