Математическая логика
жүктеу/скачать 0.93 Mb.
|
| Теорема 6.1. Формула ( ) тогда и только тогда выводима из системы формул (1), когда все полные элементарные дизъюнкции формулы входят в СКН-форму , эквивалентную формуле (3) относительно высказывательных переменных .
Так как теорема 1 формулирует необходимое и достаточное условие выводимости формулы, то на основе нее можно сформулировать алгоритм доказательства выводимости формулы. Из системы посылок (1) строится конъюнкция (3). Находим СКН-форму от высказывательных переменных для формулы (3). Строим СКН-форму для формулы и проверяем вхождение полных элементарных дизъюнкций СКН-формы для формулы в СКН-форму для формулы (3). Задание 1. Доказать выводимость . Решение. Обозначим = X, = . Строим их конъюнкцию . Найдем СКН-форму эквивалентную этой конъюнкции. V Получим СКН-форму для формулы B . Так как обе дизъюнкции входят в СКН-форму , то выводимость доказана. Замечание. Выводимость формулы можно получить и без нахождения ее СКН-формы. Для этого нужно преобразовать с помощью известных эквивалентностей формулу (3) или даже конъюнкцию некоторых полных дизъюнкций из этой СКН-формы. Например, конъюнкция 1-ой и 3-ей полных дизъюнкций формулы из задания 1 преобразуется с помощью формулы склеивания к искомой формуле. Кроме того, воспользовавшись теоремой 1, можно построить все СКН-формы выводимые из данной системы посылок. Для этого требуется небольшая модификация алгоритма доказательства выводимости формулы. После построения СКН-формы для формулы (3) необходимо 3. Из полных элементарных дизъюнкций полученной СКН-формы строим различные комбинации конъюнкций. Эти конъюнкции и будут исчерпывать все СКН-формы, выводимые из системы посылок (1). Задание 2. Найти все формулы, выводимые из системы посылок задания 1. Решение. Построим различные комбинации полных элементарных дизъюнкций формулы . Как легко видеть, при построении всех СКН-форм, выводимых из данной системы посылок, мы получили, как частный случай, формулу . Следует заметить, что на понятии выводимости основан способ доказательства утверждений методом приведения к абсурду. При использовании этого метода для доказательства истинности утверждения строится его отрицание , а затем показывается, что из этого утверждения могут быть выведены некоторые противоречащие друг другу утверждения и , т.е. доказываются выводимости и . После этого делается заключение, что утверждение истинно, так как формула является ТИ-высказыванием. В силу определения выводимости, это означает, что формула выводима из формул и . жүктеу/скачать 0.93 Mb. Достарыңызбен бөлісу:
|