Метатеория формальных систем

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

Интерпретацией формальной теории Т в область интерпретации M называется функция I: Á ® M, которая каждой формуле формальной теории Т однозначно сопоставляет некоторое содержательное высказывание относительно объектов множества (алгебраической системы) M. Это высказывание может быть истинным или ложным (или не иметь истинностного значения). Если соответствующее высказывание является истинным, то говорят, что формула выполняется в М.

Интерпретация I называется моделью множества формул G, если все формулы этого множества выполняются в интерпретации I. Интерпретация I называется моделью формальной теории Т, если все теоремы этой теории выполняются в интерпретации I (то есть все выводимые формулы оказываются истинными в данной интерпретации).

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

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

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

С помощью введенных понятий можно сформулировать следующий тезис, что теория Т пригодна для описания тех множеств, которые являются ее моделями. Модель для теории Т существует тогда и только тогда, когда Т семантически непротиворечива. Чисто логические теории – исчисление высказываний и исчисление предикатов пригодны для описания любых множеств, что соответствует общенаучному принципу универсальности законов логики. Лейбниц формулировал его как выполнимость логических законов во всех «мыслимых мирах». Аналогом этого критерия, сформулированным в терминах самих формальных теорий без привлечения семантических понятий, является формальная или дедуктивная непротиворечивость.

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

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. Исчисление предикатов и теории первого порядка.

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

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

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

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