2.6.4. Теорема дедукции

Теорема (дедукции). Если формула ψ выводима из формул ₁, ₂, …, _n, , то выводимой является формула ( → ψ), т.е.

Если

₁, ₂, …, _n,  ├ ψ,

то

₁, ₂, …, _n├ ( → ψ).

Замечание. Применяя к утверждению теоремы снова несколько раз теорему де­дукции, можно, очевидно, получить новые следствия:

₁, ₂, …, _n−1├ (_n → ( → ψ));

…

├ (₁ → … → (_n−1 → (_n → ( → ψ)))…).

2.6.5. Принцип резолюций.

Пусть C₁'и C₂' — два предложения в исчислении высказываний, и пусть C₁=PvC₁', а C₂=PvC₂', где P — пропозициональная переменная, а C₁' и C₂'  — любые предложения (в частности, может быть, пустые или состоящие только из одного литерала). Правило вывода

называется правилом резолюции.

Предложения C₁ и C₂ называются резольвируемыми (или родительскими), предложение C₁'v C₂' — резольвентой, а формулы P и P — контрарными литералами. В общем в правиле резолюции берутся два выражения и вырабатывается новое выражение, содержащее все литералы двух первоначальных выражений, за исключением двух взаимно обратных литералов.

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

Доказательство теорем сводится к доказательству того, что некоторая формула 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. Система исчисления высказываний является полной.

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

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