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

Исчисление высказываний ИВ – это аксиоматическая логическая система гильбертовского типа, адекватная алгебре высказываний. Опишем это исчисление.

В качестве алфавита исчисления высказываний возьмем следующее множество символов:

1) счетное множество высказывательных переменных, обозначаемых прописными латинскими буквами с индексами и без них;

2) символы логических операций ;

3) скобки ( , ).

Вместе с символами алфавита будем использовать и метасимволы: латинские буквы жирного шрифта для обозначения формул и знак = для обозначения формул метасимволами.

Множество формул обычно задается индуктивным определением. Допустимыми последовательностями символов или словами в языке исчисления высказываний являются формулы алгебры высказываний. Пункты 1 и 2 этого определения определяют элементарные формулы, а п. 3 – механизм образования новых формул.

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

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

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

10.

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

Определим правила вывода, которые являются отношениями на множестве формул.

1. Правило подстановки.

Пусть U– формула, содержащая высказывательную переменную X. Тогда если U – истинная формула в исчислении высказываний, то, заменяя в ней переменную X всюду, куда она входит, произвольной формулой B, мы также получим истинную формулу.

U(¼, X,¼)

_____________________________

U(¼, X,¼){В//X}

2. Правило заключения (modus ponens).

Если U и U®B истинные формулы в исчислении высказываний, то B также истинная формула, т.е.

Замечание 1. Рассмотренная нами аксиоматика не является единственно возможной. Приведем и другие, эквивалентные данной, системы аксиом.

I. Операции: (аксиоматика С.Клини (1952)).

10.

II. Операции: (аксиоматика Россера (1953)).

III. Операции: (аксиоматика Д.Гильберта и Аккермана (1938)).

IV. Операции: ®, Ø (аксиоматика Лукасевича).

Приведём примеры доказательства теорем в ИВ.

Задание 1. Показать, что формулы:

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

Решение.

I) 1. Формула

является результатом подстановки в аксиому 2 высказывательной переменной A вместо C.

2. – аксиома 1

3. Применяя правило заключения к формулам 1 и 2, получим, что

истинная формула.

II) 1. В соответствии с правилом подстановки, заменив все вхождения переменной A в аксиоме 5 на формулу , получим

2. – аксиома 4

3. Применяя правило заключения к формулам 1 и 2, получим, что

является истинной формулой.

4. Заменим в этой формуле высказывательную переменную C на A

5. – аксиома 3

6. Снова воспользовавшись правилом заключения к формулам 4, 5 получим требуемую формулу

Рассмотрим пример вывода формулы.

Задание 2. Доказать, что A |- .

Решение. Для данного примера система посылок содержит 1 формулу U₁=A, а выводимая формула B = . Построим вывод этой формулы.

1) B₁=A

2) B₂ = - аксиома 1

3) B₃= B = - получено из B₁ и B₂ в силу правила заключения.

Замечание 2.Из каждой формулы U с помощью правила подстановки, производящего замену высказывательных переменных в этой формуле любыми формулами, может быть получено бесконечное множество формул. Это множество формул называется схемой формулы U и обозначается выражением, полученным заменой в формуле U всех входящих в нее высказывательных переменных метасимволами .

Например, из формулы

возникает схема формул

. (2)

Этой схеме принадлежит формула

Новые схемы формул можно получить заменой ее метасимволов схемами формул. Эти схемы выделяют некоторое подмножество формул из множества формул, принадлежащих исходной схеме. Например, из схемы (2) можно получить схему формул

. (3)

Формула принадлежит как схеме формул (2), так и (3).

Для формул, являющимися аксиомами или теоремами, схемы формул называются соответственно схемами аксиом или схемами теорем. Схемами аксиом являются:

10.

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

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

Перечислим основные из производных правил вывода. Как и прежде, метасимволы являются произвольными формулами, а через T обозначим конечное множество формул (возможно пустое). Так как доказательство большинства правил непосредственно следует из определения выводимости и аксиом ИВ, то приведём только их формулировки, доказав лишь ключевое правило 5 – в форме теоремы дедукции.

1. Правило повторения посылки.

T, |-

2. Правило введения посылки.

ЕслиT |- , тоT, |- .

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

Если T, |- и T |- , то T |- .

4. Правило силлогизма.

ЕслиT |- , . . . ,T |- и |- , тоT |- .

5. Правило введения импликации.

ЕслиT, |- , тоT |- .

Это весьма важное свойство называют еще теоремой дедукции. Учитывая, что - конечное множество формул, правило 5 можно сформулировать в следующем виде:

Теорема дедукции. Если

|- B,

то

|- .

Доказательство. Пусть (1) есть вывод формулы B из . Индукцией по t докажем вспомогательное утверждение

|- . (4)

1⁰. Пусть . Тогда по определению выводимой формулы является либо посылкой , либо теоремой. Если , то = входит в систему посылок утверждения (4), а, следовательно, оно верно. Если B – теорема, то применив к ней и схеме аксиомы 1 правило заключения получим, что – теорема, и утверждение (4) верно.

2⁰. Пусть (4) верно при , покажем, что оно справедливо и при . Теперь, в дополнении к двум случаям п. 1⁰, формула B может быть получена по правилу заключения из двух предыдущих формул вывода, т.е.

, .

Тогда , и, воспользовавшись схемой аксиом 2

получим

|- . (5)

В соответствии с предположением индукции имеем

|- , (6)

|- . (7)

Применив к утверждениям (6), (7), (5) правило силлогизма 4, получим (4)

|- .

Формула является теоремой ИВ, поэтому

|- ,

и в соответствии с правилом 3 может быть удалена из системы посылок. Таким образом, справедливо утверждение

|- . (8)

Применяя к формулам и , полученной из схемы аксиом 1, правило заключения, получим |- . Отсюда и из (8) по правилу силлогизма 4 следует утверждение теоремы.

6. Правило удаления импликации.

ЕслиT |- , тоT, |- .

7. Правило введения конъюнкции.

T, |- .

8. Правило удаления конъюнкции.

T, |- ,

T, |- .

9. Правило введения дизъюнкции.

T, |- ,

T, |- .

10. Правило удаления дизъюнкции.

Если T, |- и T, |- , то T, |- .

11. Правило введения отрицания.

Если T, |- и T, |- , то T |- .

12. Правило удаления отрицания.

T, |-

13. Правило контрапозиции.

Если T, |- , то T, |- .

Правила 1-13 называют обычно правилами естественного вывода, а вывод формулы из системы посылок, при котором используются эти правила, - естественным выводом.

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

Задание 3. Доказать выводимость следующих формул:

1) |- ;