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

по схемам А1 и А2, h { A ) будет тавтологией. Очевидно, что h{A=>B) есть h { A ) ^ h { B ) . Если h(A=>B) = h(A)=^h(B) и h(A)- тавтологии, то и h ( B ) — тавтология, следовательно, правило MP сохраняет свойство А иметь в качестве h ( A ) тавтологию. Таким образом, всякая формула А , выводимая из А \ ,А2 с помощью M P , имеет в качестве h { A ) тавтоло­ гию. Но /?(('Ui=>1v4i)=>((lv4i=:e>^i)=> v4i)) = (v4i=i> .4i)=:>((v4i=i> a^)=ai) и эта последняя формула не является тавтологией. Следовательно, частный случай A3 - формула ('l4i=i>1 .^i)=>((l Ai=i>А{)=А^) - не выво­ дима из^1 и А 2 с помощью MP. Теорема доказана. Р а з р е ш и м о с т ь . Дедуктивная теория, в том числе и исчисление высказываний, является разрешимой, если в этой теории понятие тео­ ремы эффективно, т.е. существует правило (метод), позволяющее для произвольной формулы за конечное число действий выяснить, являет­ ся она теоремой или нет. Теорема 4 , 7 . Исчисление высказываний (теория L) является разрешимой теорией. Доказательство. Было доказано, что каждая теорема теории L является тавтологией и (обратно) кажцая формула, являющаяся тавто­ логией, есть теорема. Таким образом, формула А теории L является теоремой тогда и только тогда, когда она является тавтологией. Сле­ довательно, для того, чтобы выяснить, А - теорема или нет, достаточ­ но выяснить, А - тавтология или нет. Последнее легко определить, например, с помощью таблиц истинности или приведением к к.н.ф. В результате имеем требуемое правило, позволяющее для каждой формулы А за конечное число шагов выяснить: А - теорема или нет. Итак, исчисление высказываний является непротиворечивой, полной в широком и узком смыслах, разрешимой и эффективно аксиоматизированной формальной теорией с независимой системой аксиом. 166