Исчисления высказываний.
Легко сопоставить каждой формуле исчисления высказываний соответствующую ей формулу алгебры высказываний, и наоборот (с
учётом операции <->, т.к. она выражается через другие). Вместо конструкции A<->B, в языке исчисления высказываний пишем
(A->B)<*>(B->A).
Все аксиомы предложенные в исчислении высказываний являются тождественно истинными в логике высказываний.
Следствие 1: ├а<*>а тождественно истинно.
В исчислении высказываний нельзя вывести формулу и её отрицание одновременно. То есть исчисление высказываний является
непротиворечивой теорией.
Следствие 2: Всякая тождественно истинная формула выводима в исчислении высказываний, т.е. исчисление высказываний является
полной теорией в широком смысле.
Исчисление высказываний является полной теорией и в узком смысле. То есть присоединение к аксиоме какой-нибудь не выводимой
формулы приводит к противоречию.
Независимость аксиом исчисления высказываний означает, что ни одна из них не выводима из других, и если отбросить хоть
какую-нибудь, то потеряем полноту, т.к. не будет выводиться она сама.
Рассмотренный подход построения исчисления называется Гильбертовским. Такого же типа является формализация, где вместо modes
pones (U, U-> ?, то<*>) берётся правило modUs tollens (А->В,<*>В, то<*>А).
Существуют и другие типы подходов, позволяющие получить исчисление высказываний. Например, секвенциальные (Генценовские), в
основу которых положены только правила вывода(Г├U, Г├ ?, то Г├U<*>? ), там почти нет аксиом и т.д.
В исчислениях гильбертовского типа выводимость описывается технически проще, зато исчисления генценовского типа более
естественны – вывод в них похож на то, как на самом деле рассуждает математик.