Альтернативные системы аксиом

Описание системы аксиом Гилберта Иакермана, Россера, Мередита, Клини. Доказательств о равносильности аксиом и введенных в них связок. Расчет корректности вывода ModusTollendoTollens. Теорема о полноте метода резолюций. Выводимость на базе противоречия.
Краткое сожержание материала:

Размещено на

24

Альтернативные системы аксиом

Система аксиом Гилберта Иакермана

Связки:

, ,

Вводятся следующие аксиомы:

Система аксиом Россера

Вводятся связки:

&,-,A->B=-(A&-B)

A->(A&A)

A&B->B

(A->B)->(-(B&C)->-(C&A))

Система аксиом Мередита:

(Связки: ->, -)

[((A->B)->(-C->-D))->C]->((C->A)->(D->B))

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

Если дана формула Ф(А1… Аn) и имеются некоторые формулы Ф1…Фn, то мы можем получить формулу Ф(Ф1…Фn), подставив формулы Фi вместо соответствующих пропозиционных переменных.

Система аксиом Клини.

(K1) А->(B-A)

(K2)

(K3) A&B->A

(K4) A&B->B

(K5) A->(B->(A&B))

(K6) A->(AB)

(K7) B->(AB)

(K8) (A->C)->((B->C)->((AvB))->C

(K9) (A->B)->((A->-B)->-A)

(K10) - -A->A

Здесь все логические связки вводятся напрямую, а не рассматриваются, как сокращения друг друга.

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

Например, рассмотрим эквивалентность формул:

-(A->-B) в аксиоматике ИВ L и A&B.

На основании схемы К5 и МР доказывается, что из формулы A&B выводится формула в аксиоматике К формула А->В. Далее на основе аксиом К3 и К4 видим что из A&B выводится А, из A&B выводится В.

В теории L имеется тавтология A->(B->-(A->-B)) выводимость которой можно доказать с помощью теоремы о полноте. Исходя из этой формулы и МР, получаем, что .

В аксиоматике L имеет место тавтологии и , следовательно, по МР имеем и .

В итоге можно сделать вывод (A&B).

На основании вышеизложенного, можно сделать вывод

По аналогии можно вывести

Что касается , то уже было доказано и.

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

Теорема

Рассмотрим теоремы:

F1…Fn,

т.е. тогда, когда последняя формула является тавтологией.

Рассмотрим доказательство:

Выводимость G и множества F1…Fn означает по теореме дедукции

F1,F2…Fn-1Fn->G…

(тут типа все через импликации через вложенные скобки)

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

Представим импликацию через дизъюнкцию:

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

Пример покажем с использованием ModusTollens.

Покажем, что

Для этого нам нужно доказать что

является тавтологией

Просто находим таблицу истинностей для всех значений P и Q.

F1…Fn,

т.е. является противоречием.

Док - во. В соответствие с предыдущей теоремой, эта теорема равносильна является тавтологией, это в свою очередь равносильно , раскроем импликацию

,

далее по законам Де Моргана

В качестве примера рассмотрим доказательство корректности еще одного правила вывода ModusTollendoTollens. Т.е. покажем, что

В соответствии с только что доказанной теоремой надо вывести, что

по таблице истинности видно, что это верно.

Теорема

F₁,…,F_nG когда выводима формула F₁F₂…F_nG, т.е. когда эта формула -- тавтология

Док-во:

F₁,…,F_n |- Gпо теореме дедукции F₁,…, F_n-1 |- F_nG<=>F₁,…, F_n-2 |- F_n-1 (F_nG) <=> … <=> |- F₁ (F₂ … (F_n G) … ) <=> {по теореме ополноте} <=>F₁ (F₂ … (F_nG) … ) - тавтология ? =

F₁V (F₂ … (F_nG) … ) = … = F₁VF₂V … VF_nVG = (по з-ну Де Моргана) = (F₁&F₂& … &F_n) VG = F₁&F₂& … &F_n G - тавтология.

Теорема:

F₁, … ,F_n |- G<=>

является ли формула F₁&F₂& … &F_n&G - противоречием ?

Док-во:

По предыдущей теореме: F₁, … ,F_n |- G<=>F₁&F₂& … &F_nG - тавтология ? <=> (F₁&F₂& … &F_nG) - противоречие ?<=> ( (F₁&F₂& … &F_n) VG) - противоречие ?<=> {по з-ну Деморгана} <=>F₁&F₂& … &F_n&G - противоречие ?

Способ доказательства утверждения от противного: (А B) (BA).

Пример:

Докажем, что из формулы PQ и Q выводится P, т. е. PQ, Q |- P/

По 1-й теореме достаточно показать, что формула ((PQ) &Q) P - тавтология.

P	Q	1	2	3
Л	Л	И	И	И
Л	И	И	Л	Л
И	Л	Л	Л	Л
И	И	И	Л	Л

тавтология=>такая выводимость имеет место.

Приведение формулы к КНФ. Выводимость на основе противоречия

Дизъюнктом наз. дизъюнкция пропозициональных переменных или их отрицаний, кот.наз. литералами. Для простоты дизъюнкт принято записывать как перечень литералов, т. е. если C = L₁VL₂V … VL_n, то С = (L₁, …, L_n).

КНФ наз. логическое произведение дизъюнктов. Принято считать, что в дизъюнкте переменные и литералы не повторяются, т. к. LVL = L, LVL И (тождественная истина).В КНФ нет одинаковых дизъюнктов, т. к. C&C = C.

Пример:

(AVB)(AVC)( AVB) - КНФ.

КНФ тоже можно записывать как множество дизъюнктов. Т. е. есть

КНФ С₁ С₂ … С_n => (C₁, C₂, …,C_n) - КНФ.

Приведем формулу

F₁& … F_n&G к КНФ => вопрос: КНФ - противоречива ?

Для приведения формулы к КНФ используются тождества булевой алгебры:

A B = A V B

A B = (A B)(B A)

A &И = A

A V И = И

A & (B V C) = (A & B) V (A & C)

A V (B & C) = (A V B) & (A V C)

(AVB) = A&B

(A&B) = AVB

з-ны иденпатентности, ассоциативности, дистрибутивности.

Пример: (AB) V (A&C) приведем к КНФ.

(A B) V (A & C) = A V B V (A & C) = ( A V B V A) & ( A V B V C) = A V B V C.

Теперь проверяем на противоречивость КНФ.

Резольвентой 2-х дизъюнкта R(C₁, C₂), где

C₁ = L₁ V L₂ V … V L_k,

C₂ = L₁ V L'₂ V … V L_m