4. Доказательство.

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

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

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

где элементарная формула без -символов. Ее редукцией будет формула

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

но эта последняя и есть в точности

Тем самым эквивалентность

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

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

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

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

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

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

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

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

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

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

эти две формулы совместно друг с другом дают

При помощи этой формулы формула (1) может быть переведена в формулу

а эта последняя может быть переведена в (2) согласно выводимой схеме формул

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

Предположим, что это последнее места не имеет. Тогда имеет вид

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

а формулой

Чтобы в этом случае установить, что формула выводима без использования -символов, в силу теоремы о дедукции достаточно показать, что, используя формулу можно без использования -символов перевести друг в друга формулы [1] и [2] при помощи исчисления предикатов и с применением аксиомы равенства Кроме того, мы можем воспользоваться индукционным предположением. Его можно будет применить к формуле (с именными переменными где мы рассматриваем как параметры; эта формула содержит по крайней мере на один логический символ меньше, чем формула так как число добавляемых знаков конъюнкции на единицу меньше числа упраздненных -символов Мы сокращенно запишем эту конъюнкцию в виде

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

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

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

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

и далее в формулу

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

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

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

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

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

Поэтому формулу [1] мы можем перевести в формулу

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

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

где с снова не входит в

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

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

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

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

Для этого мы применим наше индукционное предположение к формуле (где параметры). Это даст нам возможность заменить формулу

формулой

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

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

в формулу

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

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

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

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

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

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

(1) если наше утверждение о выводимости без использования -символов справедливо для формулы то оно будет справедливо и для формулы

(2) если оно справедливо для формул и то оно будет справедливо и для формулы ;

(3) если оно справедливо для формулы (с отличной от с и не входящей в свободной переменной а), то оно будет справедливо и для формулы

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

из формулы

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

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

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

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

и во всех этих выводах будут отсутствовать -символы. Из формулы [3], подставив вместо мы получим формулу

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

Ввиду наличия вспомогательной формулы в случаях (2) и (3) речь идет о том, чтобы из двух эквивалентностей и вывести эквивалентность , а из вывести эквивалентность (мы здесь предполагаем, что переменная а не входит в

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