4.5 Вопросы для самопроверки.

1) Как строятся аксиоматические системы?

2) Назовите основные понятия теории формальных систем.

3) В чем заключается непротиворечивость и полнота формальных систем?

4) Назовите основные составляющие части формальных систем?

5) В чем заключается принцип логического вывода?

6) В чем заключается разрешимость формальных систем?

7) Дать основные понятия аксиоматических систем.

8) В чем заключается метод использования формальных моделей при исследовании систем?

9) Разрешимо ли исчисление высказываний и исчисление предикатов?

10) Что такое синтаксис и семантика формальных систем?

5. Исчисление высказываний

Теорема Дедукции определяет условия, при которых можно проверить правиль­ность схемы рассуждений без использования таблиц истинности. Именно на этой теореме основаны все методы логического вывода как в логике высказываний, так и в логике предикатов. Поэтому ее можно назвать основной теоремой теории логи­ческого вывода.

Теорема 5.1 Формула R является логическим следствием формул тог­да и только тогда, когда формула общезначима.

Доказательство. (Необходимость). Предположим, что R является логическим следствием формулы и докажем при этом предположении, что общезначима. Пусть I есть произвольная интерпретация атомов. Если все истинны на I, то истинна на I и по определению логи­ческого следствия R истинна на I, и, следовательно, на этой интерпретации истинна. Если же хотя бы одна ложна на I, то на этой интерпре­тации ложна, но также истинна независимо от R в силу оп­ределения импликации. Следовательно, на I формула истинна. В силу произвольности интерпретации I этот вывод справедлив для всякой интерпрета­ции, поэтому формула общезначима.

(Достаточность). Предположим, что формула общезначима. Тогда для всякой интерпретации, на которой все истинны, формула тоже ис­тинна, и поскольку общезначима, на этой интерпретации R тоже ис­тинна в силу определения импликации.

Теорема 5.2 Формула R является логическим следствием формул тогда и только тогда, когда формула невыполнима.

Доказательство. По теореме 5.1 формула R является логическим следствием фор­мул тогда и только тогда, когда формула общезначима или, что то же, отрицание формулы невыполнимо. Но по закону де-Моргана равносильно . Теорема доказана.

На основании теорем 5.1 и 5.1 вопрос о правильности схемы рассуждения сводит­ся к проверке общезначимости либо невыполнимости некоторой формулы. Эта проверка может быть выполнена множеством различных способов.

Как, анализируя формулу в нормальной форме, можно сделать вывод о ее обще­значимости или невыполнимости? Возьмем ДНФ, то есть представление форму­лы в виде дизъюнкции конъюнкций . Для того чтобы сделать вы­вод о ее общезначимости, нужно анализировать всю формулу целиком: каждая конъюнкция общезначимой формулы может быть истинной только на нескольких интерпретациях. В то же время вывод о невыполнимости дизъюнкции конъюнк­ций можно сделать легко: каждая конъюнкция ДНФ невыполнимой функции должна быть невыполнима, а это очень легко проверить: конъюнкция литер невы­полнима тогда и только тогда, когда она содержит хотя бы одну пару противоположных литер. Полностью аналогично можно использовать представление в виде КНФ, но для определения общезначимости функции. Очевидными следствиями предыдущих теорем являются:

Теорема 5.3 Для того, чтобы формула R была логическим следствием формулы , необходимо и достаточно , чтобы каждый конъюнкт дизъюнктивной нормальной формы представления формулы содержал пару противоположных литер .

Теорема 5.4. Для того , чтобы формула R была логическим следствием формул ., необходимо и достаточно, чтобы каждый дизъюнкт конъюнктивной нормальной формы представления содержал пару противоположных литер.

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

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

В1. Введение конъюнкции:

В2. Удаление конъюнкции:

ВЗ. Отрицание конъюнкции (закон Де Моргана):

В4. Введение дизънкции;

В5. Удаление дизъюнкции:

В6. Отрицание дизъюнкции (закон Де Моргана):

В7 Удаление импликации (modus ponens):

В8. Отрицание импликации:

В9. Введение эквивалентности:

В10. Удаление эквивалентности:

В11. Введение двойного отрицания:

В12. Удаление двойного отрицания:

В13. Правило дедкуции:

В14. Доказательство от противного:

В15. Сведение к абсурду:

В правилах В1 — В15 А и В — формулы, а Г— множество формул, возможно пустое.

Пример. Обосновать выводимость

Следовательно, по определению вы­вода на основе 1—5.

Этот метод использует тот факт, что если некоторая формула является невыпол­нимой, то наиболее сильное следствие этой формулы - константа False. Предло­женный в 1965 году Дж. Робинсоном метод резолюции позволяет получить максимально сильное следствие множества формул с помощью систематической процедуры последовательного построения логических следствий формулы, назы­ваемых резольвентами. Иными словами, метод резолюции обладает свойством полноты: для формулы Ф следствие False обязательно будет получено, если Ф — невыполнима.

Теорема 5.5 Пусть В — логическое следствие формулы А. Тогда А&В = А.

Доказательство теоремы легко проводится на основании определения понятия логического следствия. Действительно, пусть условие теоремы выполнено. Тогда А => В True.

Отсюда

.

Определение. Резольвентой двух дизъюнктов называется дизъюнкт Dl v D2.

Теорема 5.6 . Резольвента является логическим следствием порождающих ее дизъ­юнктов.

Доказательство. Пусть DlvL и D2vL,- два дизъюнкта. Тогда DlvD2- их резольвента. Легко показать , что формула (DlvL)&(D2vL)=> (DlvD2) обще­значима. Отсюда следует заключение теоремы.

Метод резолюций доказательства невыполнимости формулы Ф состоит в том, что формула Ф представляется в КНФ и к ней конъюнктивно присоединяются все возможные резольвенты ее дизъюнктов и получаемых в процессе доказательства резольвент. Полнота метода резолюций состоит в том, что он гарантирует полу­чение для формулы Ф следствия False, если Ф невыполнима. Если же, перебрав все возможные резольвенты формулы Ф, мы не нашли пустую резольвенту, то Ф не является невыполнимой.

Метод резолюций есть фактически правило присоединения к рассуждению, в состав которого входят два утверждения А => В и А => С их следствия — ут­верждения В v С, что интуитивно совершенно очевидно. Действительно, первое утверждение гарантирует, что если А истинно, то В тоже истинно, а второе — что если А ложно, то истинно С. Очевидно, что в этом случае хотя бы одно из двух, В или С, всегда истинно. Добавление этого нового утверждения к исходному рас­суждению не меняет его смысла.

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

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

в частном случае

Говорят, что квантор связывает соответствующую переменную. Предикат (формула) называется замкнутым, если связаны все переменные ( если нет свободных, т.е. несвязанных переменных).

Другими словами синтаксис логики предикатов можно определить так:

Алфавит

1. Предметные переменные x,y,z,… и переменных константы а,b,c,…

2. Функциональные константы или имена функции

3. Предикатные константы или имена предикатов

4. Логические операторы

5. Символы кванторов

Термы

1. Всякая переменная или константа есть терм.

2. если – термы и – функциональная n- местная константа , то – терм. Здесь верхний индекс определяет количество аргументов.

3. Никакие другие выражения не являются термами.

Атомы

1. Если - термы и - m-месная предиката константа , то - атом . При m=0 предикат Р( ) обращается в высказывание Р. Атомом является также равенство , т.е. выражение типа (s=t), где s и t – термы .

2. Никаких других атомов нет .

Формулы

Формулы (или правильно построенные формулы – ППФ) определяются следующим образом:

1. Всякий атом есть формула.

2. Если А – формула, то –А – формула

3. Если А и В – формулы , а х – свободная переменная , то

- формулы.

4. Никаких других формул нет.

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

Предикат служит для выражения свойства объекта (при n=1) и отношений между объектами (при п 2). Атомарная формула некотором "мире"истинна в некотором "мире" (М), если между объектами в М имеет отношение, соответствующее Р.

Связывание свободной переменной происходит либо квантификацией (взятием квантора по этой переменной) либо присвоением значения.