23. Дерево доказательств

Для описания производных правил введем понятие дерево доказательств. Дерево доказательства определим рекурсивно:

1. Деревом доказательства является пустое дерево, состоящие только из корня аксиоматической секвенции.

2. Пусть Т1 .. Тк деревья доказательства с корнями R1 .. Rk. Тогда (Т1 .. Тк)/S – дерево доказательства, где S некоторая секвенция, если S может быть получено из R1 .. Rk с помощью 1 из правил вывода. Корнем такого дерева является S.

E|-F следует из множества формул Е и формула E|-К можно утверждать, что из множества Е|-F&K. Мы можем построить следующую цепочку, рассмотрим Е в качестве формул множества G. Т.к. E|-F&K следует что E|-F&K&U, тогда мы сокращенно записываем т.к. E|-F и E|-K следует E|-F&KVU. Рассмотрим пример 1 из правил вывода, пусть из множества {q,r}|-p при этом из {pVq,r}|-~q, это значит что из определенного множества {q,r,pvq}|-p&~q. Здесь p q r уже некоторые конкретные формулы.

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

1. Modus Ponendo Ponens или MP и это основное правило вывода в рамках любого исчисления высказываний. Это больше секвенция. (P->Q, P)/Q или P->Q,P|-Q.

2. Modus Tollento Tollens если из Р следует Q и при этом Q ложно то и Р ложно. P->Q,~Q / ~P или P->Q, ~Q|-P

3. Modus Ponendo Tollens если P и Q не могут быть истинными при этом P истинно то Q ложно. ~(P&Q),P / ~Q или ~(P&Q), P |- ~Q

4. Modus Tollento Ponens сначала формально: PvQ, ~P / Q или PvQ, ~p |-Q если либо P или Q является истинным и P не истинно, то истинно Q. Правило включающего или. Сама формулировка или или наталкивает использование исключающего или. Это тот случай, когда неопределенность, содержащаяся в естественном языке искажает смысл правила умозаключений, тогда как все становится предельно понятным в формульной записи.

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

Исчисление высказываний L является формальной аксиоматической теорией для логики высказываний. Понятие формулы задается по аналогии с уже рассмотренным, т.е. есть алфавит, состоящий из заглавных латинских букв A B C, есть (), есть связь –> not. Если А и В формулы, то (~A|B) тоже формула. Для упрощения записи часто не пишем (). В частности не имеет смысл писать скобки вокруг отрицания, вообще внешние скобки формулы, при этом они присутствуют. Выделены следующие аксиомы, точнее схемы аксиом.

(A1) A->(B->A)

(A2) A->(B->C)->((A->B)->(A->C))

(A3) (~B->~A)->((~B->A)->B)

Здесь А В и С – произвольные формулы, поэтому каждая из схем описывает бесконечное множество аксиом. Если бы мы считали их непосредственно аксиомами, нам бы пришлось вводить правило подстановки. В исчислении высказываний L используется правило вывода MP. A->B,A => B или A->B, A|-B

При любых А В и С схемы аксиом являются тавтологиями, что легко проверить, построив таблицу истинности. Кроме того, схемы аксиом выбраны так, чтобы множество теорем в исчислении высказывания L совпадало со множеством тавтологий логики высказываний. Полностью это утверждение будет сформулировано в виде теоремы о полноте, которую рассмотрим позднее.

Лемма: |-A->A или для любой формулы А формула А->A является теоремой исчисления высказываний L. Построим цепочку вывода:

1. В схеме аксиом А1 : заменяем В на А, В:=А Получаем формулу A->(A->A)

2. A2: проводим замену А:А, В заменяется В:=А->А С:=А

Получаем (A->((A->A)->A))->(A->(A->A))->(A->A))

3. В схему аксиом А1 подставим А:=А В:=А->А Получаем A->((A->A)->A)

4. Сравниваем 2 и 3-ю формулы, видим общую часть. По правилу МР получаем 2-ю часть формулы 2: ((A->(A->A))->(A->A)).

5. Сравниваем 4-ю формулу и 1, по МР получаем A->A.