3. Применения дедукционной теоремы: сведение вопросов, связанных с аксиоматикой, к вопросам выводимости формул в исчислении предикатов; рассмотрение одного распространенного способа умозаключения.

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

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

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

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

окажется, что формула

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

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

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

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

является выводимой.

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

формулы. Например, мы установили [правило (?)], что из

может быть выведена формула

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

Совершенно тем же самым способом мы убеждаемся в выводимости следующих, аналогично построенных, но еще более сложных формул:

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

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

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

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

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

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

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

а из нее по схеме получим

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

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