Математическая логика и теория алгоритмов 4

Теорема. Для любой формулы ИВ существует ДНФ (КНФ) ИВ такая, что ≡ .

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

Формула (1, … , ) ИВ называется тождественно истинной (обозначается ), если (1, … , ) – тождественно истинная формула, как формула алгебры высказываний.

Теорема (о полноте). Формула ИВ доказуема тогда и только тогда, когда тождественно истинна:

.

Теорема. (о непротиворечивости). ИВ непротиворечиво.

Схема аксиом называется независимой в исчислении, если хотя бы один ее частный случай не доказуем в исчислении без этой схемы.

Теорема. Схемы аксиом ИВ независимы.