Корректность и полнота в логике высказываний Корректность и полнота логического вывода

Доказательства корректности и полноты методов, применяемых в логике высказываний, содержатся в [1, 2, 3, 4, 5,].

Корректность и полнота метода семантических таблиц

Теорема корректности. Если высказывание s доказуемо по Бету, то оно логически истинно. Формальная запись:

├_В s Þ ╞ s.

Согласно определению, высказывание s доказуемо по Бету, если семантическая таблица с помеченной формулой fs в корне является противоречивой, т.е. противоречивы все ее ветви. Если высказывание s не является логически истинным, то найдется интерпретация (множество логических значений атомов), для которой в семантической таблице обнаружится непротиворечивая ветвь c. Однако в этом случае s не доказуемо по Бету.

Теорема полноты. Если высказывание s логически истинно, то оно доказуемо по Бету. Формальная запись:

╞s Þ├ _В s.

Значок ╞ означает общезначимость, т.е. ╞s означает, формула s истинна во всех возможных интерпретациях. Если высказывание s логически истинно, то для любой интерпретации I верно: I(s)=t.

Пусть высказывание s общезначимо. Построим для него семантическую таблицу с корнем f(s). Если высказывание s не выводимо по Бету, то в таблице окажется хотя бы одна противоречивая ветвь. Это означает, что в некоторой интерпретации высказывание s ложно, что противоречит общезначимости s.

Следовательно, доказательство по Бету для s обязано существовать.

Построение семантической таблицы для формулы s гарантирует, получение для формулы s либо доказательства, либо опровержения.

Корректность и полнота аксиоматической системы вывода

Сформулируем теоремы корректности, полноты и компактности аксиоматических методов.

Множество дизъюнктов S противоречиво тогда и только тогда, когда существует опровержение в S.

Теорема корректности и полноты. Высказывание s выводимо из множества высказываний S тогда и только тогда, когда s-- логическое следствие S. Формальная запись:

S├s Û S╞ s.

Теорема компактности. Множество высказываний S выполнимо тогда и только тогда, когда выполнимо каждое его конечное подмножество.

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

Теорема о полноте исчисления высказываний. Каждая тождественно истинная формула выводима в исчислении высказываний.

Теорема об истинности доказуемых секвенций. Все доказуемые секвенции истинны.

Для каждой формулы ИС существует процедура, позволяющая определить, является ли данная формула теоремой или нет. Достаточно построить вывод, основанный на схеме аксиом и правилах вывода.

Разрешимость ИС означает существование решения (вывод) для каждой формулы.

Непротиворечивость ИС означает, что не могут быть одновременно выводимы формула и ее отрицание.

Корректность и полнота метода резолюций

Корректность метода резолюций доказывается тем, что множество дизъюнктов S невыполнимо тогда и только тогда, когда существует резолютивный вывод пустого дизъюнкта из S, так как пустой дизъюнкт не может быть истинным ни при какой интерпретации.

Пусть из S существует резолютивный вывод пустого дизъюнкта. Докажем, что S невыполнимо. Поскольку резольвента R есть логическое следствие порождающих ее дизъюнктов D_i и D_k, то конъюнктивное присоединение резольвенты R к конъюнкции дизъюнктов D_i и D_k не меняет ее логическое значение. Если в множестве резольвент S имеется пустая резольвента (дизъюнкт ранга 0), то множество S невыполнимо, поскольку соответствующая множеству R(S) КНФ содержит ложный логический сомножитель (дизъюнкция ранга 0 ложна по определению).

Полнота метода резолюций состоит в том, что он гарантирует получение пустой резольвенты, если множество дизъюнктов S невыполнимо. Если же пустая резольвента не найдена, то множество S не является невыполнимым.

Теорема. Множество дизъюнктов S противоречиво тогда и только тогда, когда существует опровержение S.

Корректность метода резолюций очевидна, так как пустой дизъюнкт не может быть истинным ни при какой оценке.

Правило резолюций имеет свойство полноты в том смысле, что позволяет вывести из множества дизъюнктов пустой дизъюнкт, если исходное множество дизъюнктов S противоречивое.

Отношение выводимости компактное вследствие конечности вывода.