Правила с конъюнкцией

Правила: 4) (Ф₁,Ф₂)/(Ф₁&Ф₂). 5) (Ф₁&Ф₂)/(Ф₁,Ф₂). 3) (Ф₁&Ф₂)/(Ф₂&Ф₁). 1)А&В├А. 2)А&В├В

Док-ва:

4) Обозначим Ф₁=А и Ф₂=В. Тогда из формулы├А→(В→(А&В)) [т.5] получим новую выводимую формулу: Ф₁→ (Ф₂→Ф₁&Ф₂). Если в этой формуле посылки Ф₁ и Ф₂ являются выводимыми формулами, то будет справедливо следующее правило:(Ф₁,Ф₂)/(Ф₁&Ф₂)

5) Справедливо также и обратное правило: (Ф₁&Ф₂)/(Ф₁,Ф₂) которое вытекает из аксиом 3 [(А&В) →А] и 4 [(А&В)→В].

3) Из этих двух правил следует правило:(Ф₁&Ф₂)/(Ф₂&Ф₁), которое можно получить из выводимой формулы: (А&В)→(В&А).

Выводимость формулы (А&В)→(В&А):

Заменим в аксиоме 5 [(А→В)→((А→С)→(А→В&С))] переменную А на формулу (А&В). Тогда согласно правилу подстановки получим выводимую формулу: (А&В→В)→((А&В →С)→(А&В →В&С)). Заменим в этой формуле переменную С на переменную А. Тогда, согласно правилу подстановки получим новую выводимую формулу: (А&В→В)→((А&В→А)→(А&В→В&А)).

Посылка этой формулы (А&В)→В является аксиомой 4, поэтому по правилу modus ponens заключение ее будет также выводимой формулой, т.е. (А&В→А)→(А&В→В&А) – выводимая формула. В этой формуле посылка является аксиомой 3, поэтому по правилу modus ponens заключение ее также будет выводимой формулой, т.е. (А&В)→(В&А) – выводимая формула.

Теорема 5 исчисления высказываний

Теорема:├ А→(В→(А&В)).

Док-во:

Обозначим через Ф₁ следующую формулу: Ф₁=(Ф_в→А)→((Ф_в→В)→(Ф_в→(А&В)). Формула А→ (Ф_в→А) – выводимая формула, т.к. она получается из аксиомы 1[А → (В→А)] заменой В на Ф_в. Следовательно, по правилу modus ponens формула (Ф_в→А) выводима из А, т.к. она является следствием в последней формуле. Тогда, тем более, формула (Ф_в→А) будет выводима из формул Ф₁, А, В, т.е. Ф₁, А, В├(Ф_в→А).

Рассуждая аналогично получим: Ф₁, А, В├(Ф_в→В). Тогда, если формула Ф₁ выводима, то из нее, учитывая 2 предыдущие полученные формулы, по сложному правилу заключения из Ф₁=(Ф_в→А)→((Ф_в→В)→(Ф_в→(А&В)) получим: Ф₁, А, В├А&В. Обозначая Ф₂=А и Ф₃=В, из Ф₁, А, В├А&В по теореме дедукции получим:├Ф₁→(Ф₂→ (Ф₃→А&В), или так ├Ф₁→(А→ (В→А&В). Осталось док-ть, что Ф₁ – выводимая формула. Это действительно так, т.к. она получается из аксиомы 5 [(А→В)→((А→С)→(А→В&С))]при замене в ней А на Ф_в, затем В на А и затем Сна В. Тогда из ├Ф₁→(А→(В→А&В) по правилу modus ponens получим, что ее следствие: А→(В→А&В) – выводимая формула.

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

Правило: А→(В→С) ├ (А&В→С)

Док-во:

По т. Дедукции А→(В→С),А&В├С

1. А&В├А (правило 1 с конъюнкцией)

2. А, А→(В→С) ├ В→С (по modus ponens)

3. А&В├В (Правило 2 с конъюнкцией)

4. В, В→С├С (по modus ponens)

Теорема 6 (а) исчисления высказываний

Теорема: ├(А→(В→С))→(А&В→С)

Док-во:

По т. Дедукции: А→(В→С)├А&В→С – проверяется правилом соединения посылок.

Правило разъединения посылок

Теорема: (А&В→С) ├ А→(В→С)

Док-во:

По т. Дедукции: А&В→С,А├ В→С; А&В→С,А,В├ С (докажем)

1. А,В├А&В (пр. 4 с конъюнкцией [(Ф₁,Ф₂)/(Ф₁&Ф₂)])

2. А,А&В→С├С (по modus ponens)

Теорема 6 (б) исчисления высказываний

Теорема: ├(А&В→С)→(А→(В→С))

Док-во:

По т. Дедукции: (А&В→С)├ А→(В→С)– проверяется правилом разъединения посылок.

Правило доказательства разбором случаев

Правило: (Г, А├C; Г, В├C)/(Г, АvВ├C)

Док-во:

Г-список гипотез.

1.Г, A├C <=> Г├A→C (по т. дедукции)

2.Г, В├C <=> Г├В→C (по т. дедукции)

3..(A→C) →((B→C) →((AvB) →C)) (аксиома 8)

По т. Дедукции: A→C├(B→C) →((AvB) →C) => А→C,В→C ├((AvB) →C)

Из св-в вывода ф-ии исчисления высказываний: Г├((AvB) →C) => Г,AvB├C доказано.

16.Равносильные преобразования с кванторами: перенос квантора через отрицание

Дата добавления: 2015-10-30