Метод (принцип) резолюции

Доказательство теорем сводится к доказательству того, что некоторая формула G (гипотеза теоремы) является логическим следствием множества формул F₁,F₂,...,F_k(допущений). То есть сама теорема может быть сформулирована следующим образом: «если F₁,F₂,...,F_k истинны, то истинна и G».

Для доказательства того, что формула G является логическим следствием множества формул F₁,F₂,...,F_k, метод резолюций применяется следующим образом. Сначала составляется множество формул { F₁,F₂,...,F_k, ùG}. Затем каждая из этих формул приводится к КНФ (конъюнкция дизъюнктов) и в полученных формулах зачеркиваются знаки конъюнкции. Получается множество дизъюнктов S. И, наконец, ищется вывод пустого дизъюнкта из S. Если пустой дизъюнкт выводим из S, то формула G является логическим следствием формул F₁,F₂,...,F_k. Если из S нельзя вывести 0, то G не является логическим следствием формул F₁,F₂,...,F_k. Такой метод доказательства теорем называется методом резолюций.

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

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

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

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

Полнота формализованного исчисления высказываний состоит в совпадении множества доказуемых формул с множеством тавтологий. Включение первого множества во второе установлено в теореме 1.

Теорема 1. Всякая доказуемая в формализованном исчислении высказываний формула является тождественно истинной формулой (или тавтологией) алгебры высказываний. Символически: .

Обратное включение установлено в теореме 2.

Теорема 2. Всякая тождественно истинная формула (или тавтология) алгебры высказываний доказуема в формализованном исчислении высказываний. Символически: .

Объединив теоремы 1 и 2, получим теорему о полноте.

Теорема 3 (о полноте формализованного исчисления высказываний). Формула тогда и только тогда доказуема в формализованном исчислении высказываний (является теоремой исчисления), когда она является тавтологией алгебры высказываний. Символически:

Теорема адекватности является обобщением предыдущей теоремы о полноте и вытекает из нее.

Теорема 4 (адекватности). Формула G выводима в формализованном исчислении высказываний из конечного множества гипотез Г тогда и только тогда, когда она является логическим следствием всех формул из этого множества. Символически:

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

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

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

2.6.7. Исчисление предикатов.

Логика первого порядка (исчисление предикатов) — формальное исчисление, допускающее высказывания относительно переменных, фиксированных функций и предикатов. Расширяет логику высказываний. В свою очередь является частным случаем логики высшего порядка.

Язык логики первого порядка строится на основе сигнатуры, состоящей из множества функциональных символов F и множества предикатных символов P. С каждым функциональным и предикатным символом связана арность, то есть число возможных аргументов. Допускаются как функциональные, так и предикатные символы арности 0. Первые иногда выделяют в отдельное множество констант. Кроме того, используются следующие дополнительные символы

• Символы переменных (обычно x,y,z,x ₁ и т. д.),
• Пропозициональные связки: Ú,Ù,ù,®,
• Кванторы: всеобщности "и существования $,
• Служебные символы: скобки и запятая.

Перечисленные символы вместе с символами из P и F образуют алфавит логики первого порядка. Более сложные конструкции определяются индуктивно:

• Терм есть символ переменной, либо имеет вид f (t ₁ ,..., t_n), где f — функциональный символ арности n, а t ₁ ,..., t_n — термы.
• Атом имеет вид p (t ₁ ,..., t_n), где p — предикатный символ арности n, а t ₁ ,..., t_n — термы.
• Формула — это либо атом, либо одна из следующих конструкций: ù F _, F ₁Ú F ₂, F ₁Ù F ₂, F ₁® F ₂, " xF, $ xF,, где F, F ₁, F ₂ — формулы, а x — переменная.

Переменная х называется связанной в формуле F, если F имеет вид " xG, либо $ xG, или же представима в одной из форм ù H _, F ₁Ú F ₂, F ₁Ù F ₂, F ₁® F ₂, причем х уже связанна в H, F ₁и F ₂. Если х не связанна в F, ее называют свободной в F. Формулу без свободных переменных называют замкнутой формулой, или предложением. Теорией первого порядка называют любое множество предложений.

Аксиоматика и доказательство формул

Система логических аксиом логики первого порядка состоит из аксиом исчисления высказываний дополненной двумя новыми аксиомами:

· " xA ® A [ t/x ]

· A [ t/x ] ®$ xA

где A [ t/x ] — формула, полученная в результате подстановки терма t вместо каждой свободной переменной х, встречающейся в формуле А.

Правил вывода 2:

• Modus ponens:

• Правило обобщения:

Теорема Гёделя о полноте исчисления предикатов является одной из фундаментальных теорем математической логики: она устанавливает однозначную связь между логической истинностью высказывания и его выводимостью в логике первого порядка. Это аналог теоремы о полноте исчисления высказываний

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

2.6.8. Теоремы Гёделя о неполноте.