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

Устранимость

t-символов из выводов таких формул, которые сами i-символов не содержат, будет устанавливаться таким образом, что каждой формуле будет сопоставляться некоторая ее «редукция» , которая является формулой без -символов и которая совпадает с в том случае, если является формулой без -символов. С учетом такого определения редукции провозглашенная нами устранимость будет доказана, если из каждого вывода формулы осуществленного в формализме описанного типа, мы сможем извлечь вывод формулы не содержащий -символов. Этот факт будет установлен, если мы сможем показать, что: 1) редукция всякой исходной формулы может быть выведена без использования -символов; 2) если в применении какого-либо правила мы заменим посылки этого правила их редукциями, то из этих редукций можно будет без использования -символов вывести редукцию формулы, получаемой по этому правилу.

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

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

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

а не в виде

Редукцией формулы

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

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

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

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

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

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

редукция формулы одного из следующих видов:

сама является формулой такого же вида.

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

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

выводима без использования -символов.

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

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

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