§ 5. Следствия, вытекающие из устранимости характеристик

1. Представимость рекурсивных функций в системе (Z).

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

Как известно, применение функции и формул и здесь может быть сведено к применению -правила.

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

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

или же его отрицание

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

Теперь рассмотрим равенство

с переменными Редукцией этого равенства является не содержащая -символов формула для которой выводима эквивалентность

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

либо ее отрицание.

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

поскольку в ней не содержится -символов, применение -правила может быть устранено. Поэтому средствами самой системы может быть выведена либо формула

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

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

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

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

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

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

равно как и эквивалентность

Подставив вместо и воспользовавшись эквивалентностью и аксиомой мы придем к равенству

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

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

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

где и рекурсивные термы, и пусть функции и изображаются -термами

где формулы системы Тогда вместо этих рекурсивных равенств мы сначала получим равенства

Затем из первого равенства с помощью выводимых эквивалентностей

и формулы

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

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

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

а из нее с помощью эквивалентностей

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

Тем самым для характеризации предиката мы получаем две формулы без -символов:

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

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

Пусть, например, функция определяется, исходя из функций при помощи функционального соотношения и пусть

где формулы из системы представляющие эти функции. Тогда в качестве

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

Из него, опираясь на эквивалентности

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

а затем из нее — опираясь на эквивалентности

и используя аксиому формулу

посредством которой предикат характеризуется в системе

Из этих формул и из формул единственности по последнему аргументу для формул могут быть выведены формулы единственности для по второму аргументу.

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

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

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

в том случае, если является значением

2. В рамках системы они допускают сведение к явному определению при помощи функции

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

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