3. Вернфицируемость выводимых формул, не содержащих формульных переменных; заменимость аксиом схемами аксиом.

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

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

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

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

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

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

3)) если формулы верифицируемы, то также верифицируема;

4)) верифицируемость какой-либо формулы не нарушается вследствие переименования связанных переменных;

5)) всякая формула вида не содержащая формульных переменных и кванторов всеобщности, верифицируема;

6)) если формула (у которой а встречается только на местах, указанных в качестве аргумента) верифицируема, то формула также верифицируема.

Обоснование утверждения для формул

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

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

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

есть редукция формулы то редукция результирующей формулы будет иметь вид

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

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

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

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

Обоснование утверждений 5)) и 6)) мы получим из теоремы о частичной редукции.

Для доказательства утверждения 5)) мы рассмотрим произвольную формулу вида

без формульных переменных и кванторов всеобщности. Пусть редукция формулы и — редукция Тогда редукция рассматриваемой формулы имеет вид

Нам нужно показать, что любая нумерическая формула

получающаяся формулы

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

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

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

Пусть редукция формулы редукция редукция Тогда

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

а

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

Верифицируемость формулы

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

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

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

верифицируема, формула

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

а так как истинна, то истинной будет также и

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

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

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

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

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

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

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

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

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

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