Проблемы аксиоматического исчисления высказываний

Теорема. Проблема разрешимости для исчисления высказываний разрешима.

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

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

Определение. Аксиоматическое исчисление называется непротиворечивым, если в нем не существует такая формула A, что доказуема A и доказуема , в противном случае (если такая формула существует), исчисление противоречиво.

Теорема. Исчисление высказываний непротиворечиво.

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

Определение. Исчисление высказываний называется полным в широком смысле, если любая тавтология в нем доказуема.

Теорема. Исчисление высказываний полно в узком смысле.

Теорема. Исчисление высказываний полно в широком смысле.

Определение. Аксиома A называется независимой от всех остальных аксиом, если она не может быть выведена из остальных аксиом.

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

Теорема. Система аксиом исчисления высказываний независима.