2. Одна система исходных формул для дедуктивной логики высказываний; полнота этой системы.

Ниже приводится система исходных формул, выбранная нами с учетом сформулированных требований. По аналогии с тем, как это сделано в «Основаниях геометрии» Гильберта, исходные формулы разбиты в ней на отдельные группы.

I. Формулы для импликации:

II. Формулы для конъюнкции:

III. Формулы для дизъюнкции:

IV. Формулы для эквивалентности:

V. Формулы для отрицания:

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

Кратко наметим доказательство этого утверждения. Во-первых, мы показываем, что из нашей системы может быть выведена любая тождественно истинная конъюнктивная нормальная форма. Затею устанавливаем, что если выражение заменимо — в соответствии с каким-либо правил замены 1—4 (быть может, в сочетании с правилом выражением то из формул нашей системы может быть выведена формула

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

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

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

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

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

Поэтому, если к нашей системе формул мы присоединим формулу то, применив несколько раз схему заключения, мы сможем получить формулу а затем, пользуясь формулами II, мы сможем получить и каждый в отдельности член этой конъюнкции. Но так как не является тождественно истинной, то среди ее конъюнктивных членов (которые со своей стороны являются простыми дизъюнкциями) найдется по меньшей мере один такой, у которого каждая из числа входящих в него переменных встречается либо только со знаком отрицания, либо только без него. Если мы теперь вместо переменных без знака отрицания подставим А, а вместо переменных со знаком отрицания подставим то получим дизъюнкцию, у которой каждый ее член есть либо А, либо а из нее, пользуясь формулами I, III и V 3), можно будет вывести выражение, представляющее собой одну-единственную переменную А. А из переменной А подстановкой можно будет получить любое выражение.

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

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