double arrow

Полнота и непротиворечивость исчисления


На основе введенных определений полноты и непротиворечивости логические исчисления можно поделить на следующие группы: полные и непротиворечивые; неполные и непротиворечивые; противоречивые.

Наша задача — построение неклассических исчислений, относящихся к первым двум группам. Заметим, что на практике полнота исчисления является желательным, но редко удовлетворяемым фактором. Объясняется это многими причинами, среди которых доминирующими являются следующие две.

Размерность задач для конкретных сред (число переменных, констант, предикатов, функций), для которых имеет смысл использовать логические исчисления, как правило, велика. Полное исчисление требует полной аксиоматизации. Это приводит к большому росту числа необходимых аксиом даже для сравнительно простых сред и необходимости обоснования достаточности этих аксиом.

Число типов выводимых формул (целей) для реальной среды ограничено конкретными потребностями. Вывод только этих формул следует гарантировать, ограничиваясь тем множеством аксиом, которые это позволяют сделать.

Проблемой полноты и непротиворечивости исчислений занимались и продолжают заниматься. Для некоторых исчислений вопрос о полноте имеет положительный ответ, например для классического исчисления высказываний и для классического исчисления предикатов первого порядка. Для классического исчисления предикатов вопрос полноты был решен немецким математиком Куртом Геделем в 1930-1931 годах. Он доказал теорему, которая называется теоремой о полноте классического исчисления логики предикатов первого порядка. Согласно этой теореме любая общезначимая формула классического исчисления логики предикатов первого порядка выводима в этом исчислении. Это означает, что для классического исчисления логики предикатов первого порядка существует полная стратегия вывода.




Гедель доказал теорему о полноте классического исчисления предикатов первого порядка, но не привел полной стратегии вывода, которую можно достаточно эффективно использовать на практике. Это сделал в 1965 г. Дж. Робинсон, опубликовав полную стратегию вывода для классического исчисления высказываний на основе правила резолюции. Заметим, что упомянутые положительные ответы о полноте относятся к классическому исчислению предикатов первого порядка. Нас же в практическом плане интересуют, прежде всего, неклассические исчисления. Вопрос об их полноте и непротиворечивости обсудим далее. Однако еще раз заметим, что неклассические исчисления, использующие классическое исчисление предикатов первого порядка, могут, наряду с другими, включать его правила вывода, в частности правило резолюции. Вследствие теоретической и практической значимости этого правила стратегию вывода на его основе рассмотрим детально в следующем параграфе.



Отметим еще один важный момент, связанный с теоремой о полноте классического исчисления логики предикатов первого порядка и вопросом об установлении факта невыводимости формулы из начальной базы знаний без вывода. Теорема Геделя гласит, что любая общезначимая формула логики предикатов первого порядка выводима в классическом исчислении логики предикатов первого порядка. Но в каждом конкретном случае до тех пор пока вывод не осуществлен, мы не знаем, выводима ли данная формула. А если она не выводима и, следовательно, вывод никогда не будет найден, то как отличить ситуацию, когда мы еще не достигли вывода, от ситуации, когда он никогда не будет достигнут? К сожалению, ответ на этот вопрос не утешителен: невозможно различить эти две ситуации и выводимость формулы может быть установлена только тогда, когда она выведена. Если же она не выводится, то придется осуществить все варианты вывода и только после этого, если она все-таки не была выведена, сделать заключение о невыводимости. Это же считается справедливым и для неклассических исчислений.

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







Сейчас читают про: