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

1.5 Непротиворечивость и полнота ИВ

назад | оглавление | вперёд

 

       В этом разделе приведем теоремы, касающиеся свойств исчисления высказываний в целом. Приведем необходимые определения.

Теорема. тавтология
Доказательство. Докажем только необходимость утверждения. Нетрудно проверить, что аксиомы A 1, A 2, A 3, являются тавтoлогиями, а правило вывода modus ponens сохраняет тождественную истинность формул, т.е. из И (истинные, т.е. их значение=1) формул по правилу вывода получаются только И формулы.
       Теорема доказана.

Следствие. Теория L – формально непротиворечива.
Доказательство. Поскольку все теоремы теории L – тавтoлогии, то отрицание тавтологии не есть тавтология. Следовательно, в теории L не существует одновременно теоремы и ее отрицания.
       Следствие доказано.


Теорема. Система аксиом теории L независима.
       Теорема не требует доказательства.

Теорема. Теория L является разрешимой теорией.
Доказательство. Чтобы узнать выводима ли некоторая формула в исчислении высказываний, достаточно проверить тождественную истинность (т.е. то, что формула является тавтологией) этой формулы, что можно сделать за конечное число шагов.
       Теорема доказана.
назад | оглавление | вперёд