3. Включение связанных переменных; мероприятия по сохранению схем при возвратном переносе подстановок; недостаточность прежних методов.

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

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

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

или соответственно

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

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

(за этими формулами могут идти еще и другие, ведущие нас к заключительной формуле

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

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

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

мы получим следующий модифицированный ряд формул:

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

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

[например, по правилу ]; тогда при возвратном переносе подстановок формула 5) не будет затронута.

Если же в рассматриваемой нити доказательства мы применим процедуру возвратного переноса подстановок к первоначальным формулам разложенного вывода, начиная с формулы 5), то вместо формул 3) и 4) получим формулы

и

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

Если же процедуру возвратного переноса подстановок мы применим к формулам, предварительно модифицированным согласно нашему предписанию, то вместо первоначальных формул 3) и 4) мы получим формулы

и

при этом структура доказательства сохранится; только выделенная в схеме переменная будет заменена на

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

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