2. Доказательство непротиворечивости добавления рекурсивных определений в рамках элементарного исчисления со свободными переменными; привлечение схемы индукции.

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

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

из системы (А) и аксиому индукции из (В).

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

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

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

Пусть у нас имеется система аксиом, состоящая из формулы

и, кроме того, из некоторых других формул

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

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

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

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

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

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

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

либо

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

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

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

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

средствами элементарного исчисления со свободными переменными, будет истинной.

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

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

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

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

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

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

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

Тем самым мы приходим к констатации следующего факта:

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

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

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

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

этой схемы какой-нибудь другой свободной переменной.

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

выполнения соответствующих операций) имеют вид

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

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

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

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

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