Теория L. Аксиомы и правила вывода

Исчисление высказываний – это формальная аксиоматическая теория, теоремами которой являются тавтологии алгебры высказываний, и только они. Существует много разных теорий, удовлетворяющих этому условию. Мы рассмотрим исчисление L, которое строится следующим образом.

1. В качестве переменных употребляются только буква А с индексами: , – пропорциональные буквы, из связок вводятся только две: отрицание и импликация , которые называются примитивными, и скобки ().

2. формулами теории L являются

а) все пропозициональные буквы суть формулы;

б) если и – формулы, то и – также формулы.

Итак, любая формула теории L – это пропозициональная формула, построенная из пропозициональных букв с помощью связок и .

3. Каковы бы ни были формулы , , Х теории L следующие формулы суть аксиомы:

А1. ;

А2. ;

А3. .

4. Единственное правило вывода в L – modus ponens (МР): из формул Ф и непосредственно следует формула .

Связки вводятся в L с помощью определений:

Д1. означает ;

Д2. означает ;

Д3. означает .

Эти определения устанавливают процедуру перевода с языка алгебры высказываний на язык теории L.

Выводы в исчислении высказываний. Вывод в теории L формулы Ф из множества формул Г – это конечная последовательность формул , в которой каждая формула является: а) аксиомой теории L, либо б) принадлежит множеству Г (является гипотезой), либо в) получена из предыдущих членов этой последовательности по правилу modus ponens, а последняя формула этой последовательности совпадает с Ф.

Если существует вывод формулы Ф из множества формул Г, то говорят, что Ф выводима из Г и пишут . Если множество Г пустое, то Ф называется просто выводимой и обозначается . Если , то Ф называется теоремой теории L.

Понятие вывода разъясним на примерах.

Пример. Лемма1. Для любой .

1. В (А2) заменим на , а Х на Ф, получим

(по А2).

2. В (А1) подставим вместо

(по А1).

3. Из и по правилу modus ponens имеем

(из и по МР).

4. В (А1) положим , тогда

(по А1).

5. Из и по правилу modus ponens получаем

(из и по МР).

- доказываемая формула.

Теорема о дедукции (ТД). Если Г – некоторое множество формул, Ф и - формулы, причем , то .

Эта теорема часто очень полезна для доказательства многих утверждений о выводимости других утверждений. Доказывается она индукцией по длине вывода . Доказательство смотри в [2].

Замечание. Если формула совпадает с Ф, то формула принимает вид , выводимость которой доказана в лемме 1, и доказывает справедливость теоремы в этом случае.

В качестве примера применения теоремы о дедукции приведем доказательство следующего утверждения: .

1. - гипотеза.

2. - гипотеза.

3. - гипотеза.

4. - из и по МР.

5. - из и по МР.

Итак, . Отсюда по теореме о дедукции .

Другие примеры применения теоремы о дедукции можно найти в доказательствах леммы 2 теории L: (см. [2], с. 41-43).

а) ;

б) ;

в) ;

г) ;

д) ;

е) ;

ж) .

Контрольные вопросы и упражнения

1. Проверить, что схемы аксиом А1, А2, А3 порождают тождественно истинные формулы.

2. Почему ?

3. Пусть и . Что можно сказать о формуле Ф?

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

5. Какими способами из данного вывода формулы Ф можно получить новый вывод этой же формулы?

6. Являются ли выводами следующие последовательности:

а) ;

б) ;

в) .

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

а) ;

б) ;

в) ;

г) ;

д) .

8. Построить выводы (не пользуясь теоремой о дедукции):

а) ;

б) ;

в) .

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

10. Доказать, что если для некоторой формулы Ф справедливы утверждения и , то , где – любая формула.

11. Доказать, что если схему аксиом А3 заменить схемой , то класс выводимых формул от этого не изменится.

12. В данных доказательствах указать, на основании чего включена та или иная формула (доказательства не являются в данном случае полными выводами):

а) б)

13. Доказать, что не все формулы выводимы.

14. Доказать, что не будет полным исчисление высказываний, полученного из данного путем удаления схемы аксиом А2, А3.

Дата добавления: 2015-11-14