Правило опровержения

Упражнение:Докажите формально остальные основные равносильности.

6. Доказуемость и тождественная истинность формул. Теперь уже можно доказать основной результат этого параграфа.

Теорема (о доказуемости и тождественной истинности формул ИВ).Формула формального исчисления высказываний доказуема тогда и только тогда, когда она тождественно истинна.

Доказательство. То, что доказуемая формула является тождественно истинной, уже отмечалось выше: для этого нужно лишь заметить, что все аксиомы исчисления высказываний тождественно истинны и что множество всех тождественно истинных формул замкнуто относительно правила вывода modus ponens.

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

Ø избавиться от всех импликаций, выразив её через дизъюнкцию и отрицание.

Ø избавиться от “длинных отрицаний” с помощью законов де Моргана.

Ø избавиться от кратных отрицаний, применив закон двойного отрицания.

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

Ø использовать законы поглощения, ограничения, склейки и другие для упрощения формул.

Упражнение.Докажите законы поглощения, ограничения, склейки и другие, полезные для упрощения формул.

Примеры: 1.(® (Ù (x Ú ))) ~

~ (Ú ( Ù (x Ú ))) ~

~ ( Ú (Ù (x Ú ))) ~

~ (((Ù)Ú (x Ù )) Ú (Ù (x Ú ))) ~

~ (((x Ù ) Ú (x Ù )) Ú (Ù (x Ú ))) ~

~ ((x Ù ) Ú ((Ù x)Ú (Ù))) ~ ((x Ù) Ú (Ù)) (СДНФ) ~

~ ~ (?!) ~ (x Ú ) Ù (Ú ) (СКНФ).

2. ((a ® b) ® ((a ® c) ® (a ® (b Ù c))) ~ ((Ú b) ® ((Ú c) ® (Ú (b Ù c))) ~

~ (Ú (Ú (Ú (b Ù c)))) ~ ((a Ù ) Ú ((a Ù ) Ú (Ú (b Ù c)))) ~

~ (a Ù ) Ú (a Ù )Ú Ú (b Ù c) ~ (a Ù ) Ú ((a Ú ) Ù (Ú ))Ú (b Ù c) ~

~ (a Ù ) Ú Ú Ú (b Ù c) ~ ((a Ù ) Ú ) Ú (Ú (b Ù c)) ~

~ ((a Ú ) Ù (Ú )) Ú ((Ú b) Ù (Ú c)) ~ (Ú ) Ú (Ú b) ~

~ (Ú ) Ú (b Ú ) ~ (b Ú ) ~ (?!) ~

~ (a Ù b Ù c) Ú (a Ù b Ù ) Ú (a Ù Ù c) Ú (a Ù Ù ) Ú

Ú (Ù b Ù c) Ú (Ù b Ù ) Ú (ÙÙ c) Ú (ÙÙ ) (СДНФ).

Рассуждая в общем виде, можно доказать теорему о СДНФ и СКНФ:

Теорема (о СДНФ и СКНФ).(1) Любая формула ИВ равносильна либо противоречию (x Ù ), либо единственной СДНФ.

(2) Любая формула ИВ равносильна либо тождественно истинной формуле (x Ú ), либо единственной СКНФ.

Хотя сейчас вопросы о единственности получаемых форм нас не интересуют, поду­майте, как это можно доказать.

Вернёмся теперь к доказательству теоремы о доказуемости и тождественной истинности формул. Поймём, что любая тождественно истинная формула Ф доказуема в формальном исчислении высказываний. По теореме о СДНФ либо Ф ~ (x Ù ), либо Ф ~ D(x₁ , … , x_n ) = . Поскольку равносильность ~ формул сохраняет тождественную истинность (?!), то полученная формула тоже тождественно истинна. Поэтому первый случай невозможен, и D(x₁ , … , x_n ) является тождественно истинной дизъюнктивной формой указанного выше вида.

Когда CДНФ тождественно истинна ? Докажем, что это возможно только в случае D(x₁ , … , x_n ) ~ (x Ú ). Отсюда будет следовать (?!) доказуемость формулы D(x₁ , … , x_n ), а значит, доказуемость и исходной тождественно истинной формулы Ф.

Если в D(x₁ , … , x_n ) участвует некоторая переменная x, то группируя с помощью закона дистрибутивности все конъюнкции, содержащие x и соответственно, СДНФ можно записать в виде

D(x , y₁ , … , y_n–1 ) ~ (x Ù D_x ) Ú (Ù ) Ú D₀ ,

где D_x , и D₀ – некоторые ДНФ, не зависящие от x и (D₀ и могут быть пустыми, а D_x – нет). Можно считать, что D₀ отсутствует:

(x Ù D_x ) Ú (Ù) Ú D₀ ~ (x Ù D_x ) Ú (Ù) Ú (x Ù D₀ Ú Ù D₀ ) ~

~ (x Ù (D_x Ú D₀ )) Ú ( Ù (Ú D₀ )).

Значит, можно сразу считать, что D(x , y₁ , … , y_n–1 ) ~ (x Ù D_x ) Ú (Ù). При этом формулы D_x и непусты: если, например, D_x отсутствует, то получаем противоречие с тождественной истинностью формулы D:

D(1, y₁ , … , y_n–1) = = 0.

Подставляя x = 0, получим тождественно истинную ДНФ (y₁ , … , y_n–1) от меньшего количе­ства переменных, так что (y₁ , … , y_n–1) ~ (y Ú ) и

D(x , y₁ , … , y_n–1 ) ~ (x Ù D_x ) Ú (Ù (y Ú )) ~ (x Ù D_x )Ú .

Аналогично, подставив x = 1, придём к D_x(y₁ , … , y_n–1 ) ~ (z Ú ),

D(x , y₁ , … , y_n–1 ) ~ (x Ù D_x ) Ú ~ ((x Ù (z Ú )) Ú ) ~ (x Ú ),

что и требовалось.

Итак, исходная тождественно истинная формула равносильна доказуемой формуле (x Ú ), а потому и сама доказуема.

Теорема полностью доказана.

Итак, обоснована адекватность формальной аксиоматической теории исчисления высказываний её неформальному варианту.