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

Принцип двойственности

Определение: Две формулы А и В равносильны тогда, когда равносильны А* и В*.

Док-во:

А = В =>

Для любого (x1,…,xn): A(x1,...,xn)=B(x1,…,xn);

Для любого (x1,…,xn): A(x1,..., xn)=B(x1,…, xn);

Для любого (x1,…,xn): (A(x1,..., xn))= (B(x1,…, xn));

По св-ву 2 двойственной функции [Для любого набора (х1,…,хn) справедливо Ф*(х1,…,хn)= (Ф(х1,…, хn)) ], А*(x1,...,xn)=В*(x1,...,xn) для любого (x1,...,xn), => А* = В*

Необходимое и достаточное условие, чтобы формула являлась тавтологией (использование КНФ)

Утверждение φ-тавтология только тогда когда КНФ данной формулы в каждой своей элементарной дизъюнкции содержит некую переменную и ее отрицание
Док-во: Конъюнкция принимает значение И т.и т.т.к. все ее переменные(в данном случае эл. Дизъюнкции) истины. Чтобы элементарные дизъюнкции были истины необходимо, чтобы они состояли из переменной и ее отрицания. Тогда используя свойство АvА= И, мы получаем что все дизъюнкции принимают значение И => конъюнкция из истин =И(всегда равна). Это и есть тавтология.

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

Теорема: ├ (В→Ф_в).

Док-во:

Ф_в – произвольная выводимая формула.

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

В полученной формуле посылка Ф_в – выводимая формула. Следовательно, по правилу заключения (modus ponens) и ее заключение – (В→Ф_в) также выводимая формула.

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

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

Док-во:

Формула (А→В)→ (А→А) выводима. Заменим в этой формуле переменную В на Ф_в. Тогда, по правилу подстановки получим новую выводимую формулу: (А→ Ф_в)→ (А→А). По теореме 1 посылка этой формулы (А→ Ф_в) является выводимой формулой. Следовательно, по правилу заключения (modus ponens) и ее заключение (А→А) также выводимая формула.

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

Заменим в аксиоме 2[(А→ (В→С)) → ((А→В) → (А→С))] переменную С на переменную А. Тогда получим формулу (А→ (В→А)) → ((А→В) → (А→А)).

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

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

Правило: ((Ф₁→Ф₂),(Ф₂→Ф₃))/(Ф₁→Ф₃) или (Ф₁→Ф₂),(Ф₂ →Ф₃)├(Ф₁→Ф₃).

Док-во:

Формула (А→В)→((В →С) → (А→С)) выводима по т.3. Заменим в ней переменную А на Ф₁, переменную В на Ф₂, а переменную С на Ф₃. Тогда по правилу подстановки получим новую выводимую формулу:

(Ф₁→Ф₂)→((Ф₂ →Ф₃) → (Ф₁→Ф₃)). Из этой формулы следует, что если формулы (Ф₁→Ф₂) и (Ф₂ →Ф₃) являются выводимыми, то и формула (Ф₁→Ф₃) также выводимая формула.

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

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

Док-во:

Покажем, что формулу С можно вывести из следующих формул: Ф₁=(А→В), Ф₂=(В→С), Ф₃=А, т.е. Ф₁, Ф₂, Ф₃├ С.

Действительно, формула В выводится из формул Ф₁ и Ф₃ по схеме

(А, А→В)/В. Тогда, по теореме о дедукции из Ф₁, Ф₂, Ф₃├ С получим, что формула Ф₁ → (Ф₂ → (Ф₃ → С)) – выводимая формула, т.е. (А→В)→((В→С)→(А→С)) – выводимая формула.

Правило перестановки

Правило:(Ф₁→ (Ф₂→Ф₃))/(Ф₂→ (Ф₁→Ф₃)).

Док-во:

Заменим в формуле (А→(В→С))→(В→ (А→С)) [т.4] А на Ф₁, В на Ф₂ и С на Ф₃. Тогда получим новую выводимую формулу: (Ф₁→(Ф₂→Ф₃))→(Ф₂→(Ф₁→Ф₃)). Если посылка в этой формуле Ф₁→(Ф₂→Ф₃) является выводимой формулой, то по правилу modus ponens и ее следствие Ф₂→ (Ф₁→Ф₃) также будет выводимой формулой.

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

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

Док-во:

Покажем, что С выводится из следующих формул: Ф₁=А→(В→С), Ф₂=В, Ф₃=А, т.е. Ф₁, Ф₂, Ф₃├ С.

Действительно, по правилу modus ponens имеем: (А,А→ (В→С))/(В→С), т.е. (В→С) – выводимая формула. Тогда по следующей схеме: (В, (В→С))/С, согласно правилу modus ponens, получим, что С – выводимая формула. По теореме дедукции из Ф₁, Ф₂, Ф₃├ С получим выводимую формулу: Ф₁ → (Ф₂ → (Ф₃ → С)). Подставляя в эту формулу вместо Ф₁, Ф₂ и Ф₃ их выражения, получим выводимую формулу, которую надо было док-ть.

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