4. Полнота системы (А).

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

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

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

усматривается немедленно, а для формулы

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

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

Подведем итоги. Прежде всего, нами получена следующая

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

Приведем еще одно

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

и верифицируема; следовательно, формула является также и выводимой.

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

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

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

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

будет истинной.

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