Схема аксиом Чёрча

А1)(p®(q®r))®((p®q)®(p®r));

А2)p®(q®p);

А3)(ùp®ùq)®(q®p).

Определение. Логическая формула В является логическим следствием формулы А

(АaВ), если для любой интерпретации I значение В – «истина» всякий раз, когда значение А – «истина».

Из определения следует, что В является следствием А тогда и только тогда, когда А®В – тавтология.

A(I)®B(I)º1

Теорема 1: Если А – тавтология и А®В – тавтология, то В – тавтология.

Обобщение тавтологии в виде логического правила вывода

A&(A®B)aB А,А®В (если А – тавтология и А®В – тавто

МП-правило (modus penuus) В логия, то В – тавтология).

Если формула В – теорема логики высказываний, т.е. следует из аксиом, то это обозначается «aВ».

Теорема 2: Если в вычислении высказываний А выводимо, то А – тавтология.

Утверждение о полноте теории. Если формула А – тавтология, то она является теоремой исчисления высказываний.

Утверждение о непротиворечивости. Не существует формула А такой, что А и ùА являются теоремами.

Следствие: Существуют формулы, которые не являются тавтологиями. Если А – тавтология, то ùА – не тавтология (противоречивость).

Пример: Нужно доказать aАÚùА.

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

1) АÚА®А (А1);

2) (АÚА)®(ùАÚ(АÚА)®ùАÚА) (из А4: С=ùА, А=АÚА, В=А);

3) ùАÚ(АÚА)®ùАÚА (МП: (1,2)®3);

4) (А®(АÚА))®(А®А) (тождественная замена дизъюнкции импликацией);

5) А®АÚА (А2: ВºА);

6) А®А (МП: (4,5)®6);

7) ùАÚА (замена импликации на дизъюнкцию);

8) ùАÚА®АÚùА (А3: В=А, А=ùА);

9) АÚùА (МП: (7,8)®9).

Метод вывода с использованием аксиом неэффективен – направленная стратегия применения аксиом. Само применение основано на интуиции.

Тьюринг и Чёрч доказали, что аксиоматическая система не имеет разрешающей алгоритмической процедуры.

1.4 Логический вывод

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

Определение. Формула В называется логическим следствием из гипотез F₁F₂…F_m(m³1), если при всякой интерпретации F₁(I)…F_m(I),B(I), если F₁F₂…F_m истинны, то и В – «истина».

Обозначается F₁F₂…F_maВ.

При m=1 мы получаем просто формулу или теорему исчисления FaB и это справедливо, когда F®B - тавтология.

При m>1

Теорема 1: Формула В –логическое следствие из гипотез F₁F₂…F_maВ тогда и только тогда, когда эта формула следует из конъюнкции F₁ & F₂ &…&F_maВ или импликация F₁ & F₂ &…&F_m®В.

Если (F₁ & F₂ &…&F_m)®В, то F®B m=1совпадает с определением F.

Теорема 2: В является логическим следствием из гипотез F₁F₂ …F_m тогда и только тогда, когда F₁®(F₂®(…(F_m-1®(F_m®B))- тавтология.

Берём тавтологию

((А&В)®С)º(А®(В®С)). Последовательно применяя эту тавтологию к F₁&(F₂&…&F_m)®В, т.е. F₁&F®BÞ(F₁®(F®B)).

F

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

Алгоритм. Доказательство – цепочка формул А₁,А₂…А_i…А_t,В, где А_i – формула, полученная либо из гипотез, либо применением аксиом, или ранее полученные формулы – аксиомы – результат применения правил вывода.

Правила вывода (упрощают доказательство) являются обобщением многократно применяемых тавтологий:

1)МП-правило

A&(A®B)aB; A,A®B

B

2)Удаление конъюнкции (УК)

p&qap; p&qaq

p&qp&q

p q

3)Введение конъюнкции (ВК)

p&qap&q p,q

p&q

4)Введение дизъюнкции (ВД)

papÚq p

pÚq

5)Удаление дизъюнкции (УД)

УД1: (pÚq)&ùpaq pÚq,ùp

q

УД2: (pÚq)&paùq pÚq,p

ùq

6)Дизъюнктивное расширение (ДР)

(p®q)a(pÚb®qÚb) p®q

pÚb®qÚb

7)Транзитивная импликация (ТИ)

(p®r)&(r®q)a(p®q) p®r,r®q

p®q

Пример:

AÚB,A®C,B®D

CÚD

1) A®C (гипотеза);

2) AÚB®CÚB (ДР 1®2);

3) B®D (гипотеза);

4) CÚB®CÚD (ДР 3®4);

5) AÚB®CÚD (ТИ 2,4® 5);

6) AÚB (гипотеза);

7) CÚD (МП 5,6 ®7).

Пример:

(A1&A2)®B,A1&C,C®A2

B

1) A1&C (гипотеза);

2) A1 (УК 1®2);

3) C (УК 1®3);

4) C®A2 (гипотеза);

5) A2 (МП 3,4®5);

6) (A1&A2) (ВК 2,5®6);

7) (A1&A2)®B (гипотеза);

8) B (МП 6,7®8).