2. Дедукционная теорема.

Тем не менее имеет место следующая

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

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

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

Относительно заданного вывода мы сначала сделаем некоторое более сильное предположение; именно, мы будем считать, что в формулу не входят ни [выделенная в схемах (а) и ] переменная а, ни какая-либо другая переменная, в применении к которой в выводе производится какая-нибудь подстановка.

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

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

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

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

формула

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

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

Добавление в формулах посылки не разрушает подстановок, так как по сделанному нами предположению переменные, вместо которых производятся какие-либо подстановки, в не входят. Переименование связанных переменных также не затрагивается добавлением посылок

Любая схема заключения

переходит в последовательность, состоящую из формул

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

из формул

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

Столь же просто решается вопрос и в случае схем (а) и : вместо перехода от

к

производимого по схеме мы получаем последовательность

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

то вместо него мы получаем последовательность

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

посылки, затем к полученной формуле

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

мы снова переставим посылки.

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

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

прослеживании данного вывода не должно соответствовать вхождению этой переменной в исходную формулу

Например, если формула выводится из формулы при помощи ряда формул

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

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

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

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

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

мы вернемся к формуле

в силу сказанного, эта последняя также окажется выводимой.

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

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

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

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

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

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

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