Непротиворечивость и полнота аксиоматической теории исчисления высказываний

Нет ничего проще создания аксиоматических теорий! Как сказал один известный математик: "Аксиоматизация сродни воровству!".

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

свою аксиоматическую теорию.

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

@ ½¾ @@.

Тогда в данной теории будет выводима любая последовательность из одного или более символов @.

Одно плохо, толку в таких теориях обычно никакого нет…

А вот рассмотренная ранее аксиоматическая теория исчисления высказываний имеет ряд важных (интересных, замечательных) свойств. Формулы этой теории можно интерпретировать как формулы алгебры высказываний, записанные с использованием (функционально полного набора!) операций: Ø и ® (отрицания и импликации).

Для этой теории доказано, что она полна. То есть в этой теории могут быть выведены все тавтологии логики высказываний (которые могут быть записаны с помощью Ø и ®).

Более того, данная теория непротиворечива. То есть в этой теории не могут быть выведены какая-то формула Ф и ее отрицание (ØФ).

Докажем непротиворечивость этой теории.

Прямой проверкой доказывается, что все аксиомы, получаемые из схем аксиом, являются тавтологиями. Например, для первой схемы аксиом:

А ® (В ® А)

А	В	Ф

А из тавтологий с помощью m.p. ( A, A ® B ½¾ B) можно получить только тавтологии. А поскольку любая полученная в этой теории формула Ф есть тавтология,

то ее отрицание ØФ было бы противоречием, которое не выводимо.

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

Что же касается непротиворечивости, то это очень жесткое требование.

Стоит допустить в теории возможность хотя бы одного противоречия (для одной формулы Ф допустит возможность вывода и ØФ), как теория становится бессмысленной, так как тогда в ней можно вывести любую формулу. (Из ложной посылки может следовать что угодно).