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

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

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

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

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

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

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

Если мы применим эту процедуру к нашему предыдущему примеру, то вместо формулы 9) мы должны будем написать повторение формулы 10):

Эта формула получается из 9) в результате подстановки вместо а. Теперь мы должны произвести ту же самую подстановку и в трех идущих в обратном направлении схемах заключения; иными словами, мы должны будем в формулах

всюду вместо а подставить 0. Наконец, мы должны будем вместо формулы 2) написать формулу, получающуюся в результате этой подстановки из формулы 3), а вместо формулы 1) — формулу, получающуюся в результате этой подстановки из формулы 4).

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

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

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

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

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

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

заключения, а потом в нитях доказательства

и

вместо 4) надо будет вставить ту формулу, которая у нас получится вместо 8), а в нитях

вместо 4) — ту формулу, которая получится вместо 5).

Но при возвратном переносе подстановки вместо а мы вместо 8) получим формулу

а вместо 5) — формулу

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

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

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

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

б) вместо формульной переменной с аргументом а равенство

в) вместо формульной переменной с несколькими аргументами формулу

и вместо всякой индивидной переменной цифру 0.

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

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

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

Но наша фигура обладает еще и той существенной особенностью, что все ее формулы суть нумерические формулы.

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

и

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

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

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

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

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

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

Действительно, истинными являются все формулы, стоящие на месте исходных.

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

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

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

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

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

так как в этом случае отлично от и тем самым равенство ложно.

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

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

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

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

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

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

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

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

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