3.4. Исчисление высказываний (ив)

Чтобы задать формальную аксиоматическую теорию, необходимо определить:

некоторое счётное множество символов (алфавит) – символов теории Т(конечные последовательности символов теорииТназываются выражениями теорииТ);

подмножество выражений теории Т, называемых формулами;

подмножество формул теории Т, называемых аксиомами;

конечное множество R₁,R₂, ...,R_mотношений между формулами, называемых правилами вывода.

Если Aи формулыA₁,A₂, ...,A_iнаходятся в некотором отношенииR_k(), тоAназываетсянепосредственным следствиемиз формулA₁,A₂, ...,A_i, полученным по правилуR_k.

Выводом в теорииТназывается всякая последовательность₁,₂, ...,_nформул такая, что для любогоi (), формула _iесть либо аксиома теорииТ, либо непосредственное следствие каких-либо предыдущих формул.

Формула Aназываетсятеоремой(греч.theorema– рассматриваю, обдумываю) теорииТ, если в ней существует вывод, в котором последней формулой являетсяA.

Формула Aназываетсяследствием множества формул Г тогда и только тогда, когда существует такая последовательность формул₁,₂, ...,_n, что_nестьA, и для любогоi, 1in,_iесть либо аксиома, либо формула из Г, либо непосредственное следствие некоторых предыдущих формул. Эта последовательность называется выводомAиз Г. Элементы Г называютсяпосылками вывода илигипотезами. Сокращенно можно записать ГA. Если множество Г состоит их формулB₁,B₂, ...,B_k, то пишутB₁,B₂, ...,B_kA, и говорят, что формулаAвыводимаиз формулB₁,B₂, ...,B_k. Если Г – пустое множество, то ГAтогда и только тогда, когдаAесть теорема. В этом случае принято писатьAи говорить, что формулаAдоказуема, а сам вывод (последовательность формул) называютдоказательством .

Формальная аксиоматическая теория называется полной, если в ней доказуема любая тавтология.

Формальная аксиоматическая теория называется непротиворечивой, если в ней не существует вывода формулыAтакой, что одновременно доказуемы формулыAи^A.

Формальную аксиоматическую теорию называют полной в узком смысле, если добавление любой невыводимой формулы в качестве схемы аксиом приводит к противоречивой системе.

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

1. Алфавит ИВ образуют буквыA,B,C... и т.д. (возможно с индексами), которые называютсяпропозициональными переменными, логические символы (связки)^,,,, а также вспомогательные символы скобок (, ).

2. Множество формул ИВ определяется индуктивно:

а) все пропозициональные переменные являются формулами ИВ;

б) если A иBформулы ИВ, то (^A), (AB), (AB), (AB) – формулы ИВ;

в) выражение является формулой ИВ тогда и только тогда, когда это может быть установлено с помощью пунктов а) и б).

Договоримся далее опускать внешние скобки у формулы

3. Аксиомы ИВ (система Клини).

1) A(BA) 6) AAB

2) (AB)((A(BC))(AC)) 7) BAB

3) A(BAB) 8) (AC)((BC)(ABC))

4) ABA 9) (AB)((A^B)^A)

5) ABB 10) ^AA

4.Единственнымправилом выводав ИВ являетсяпривило заключения(modus ponens) : еслиAиAB– выводимые формулы, тоB– также выводимая формула. Символическая запись:.

Выводом A₁,A₂,...,A_n–Aназывается последовательность формул₁,₂,..., _m,A, в которой любая формула либо является одной из формулA₁,A₂,...,A_n(т.е.посылкой), либоаксиомой, либоподстановкойв аксиому, либо получается из предыдущих формул по правилу вывода.

Исчисление высказываний – непротиворечивая, полная аксиоматическая теория, причем ИВ полно и в узком смысле.

Примерыформальных выводов и доказательств в ИВ.

I. Построить выводDCD

1) D посылка,

2) DCD аксиома 7,AC,BD,

3) CD m.p. 1 и 2.

II. Построить вывод AB, BCAC

1) AB посылка,

2) (AB)((A(BC))(AC)) аксиома 2,

3) (A(BC))(AC) m.p. 1 и 2,

4) BC посылка,

5) (BC)(A(BC)) аксиома 1,

6) (A(BC)) m.p. 4 и 5.

7) AC m.p. 6 и 3.

III. Доказать DD

1) D(DD) акс. 1, AD, BD,

2) (D(DD))((D((DD)D))(DD))

акс. 2, AD, BDD, CD,

3) (D((DD)D))(DD)m.p.1 и 2,

4) D((DD)D) акс. 1, AD, BDD,

5) DD m.p.4 и 3.

Теорема о дедукции.Если имеется вывод формулыBиз последовательности формул,A, то можно построить вывод формулыABиз последовательности формул(символически: Если,AB, тоAB), где – набор некоторых формулA₁,A₂,...,A_n.

Докажем эту теорему конструктивно, т.е. предложим алгоритм построения вывода ABиз имеющегося вывода,AB.

Пусть имеется последовательность формул ₁,₂,...,_m,B, является выводом,AB. Далее будем называть этот выводвспомогательным. На первом шаге нахождения результирующего вывода припишем спереди к каждой из формул вспомогательного вывода символыA, добавляя, если это необходимо, скобки. Получим последовательностьA₁,A₂,...,A_m,ABс последней формулойAB, которая и должна быть последней в результирующем выводе. Очевидно, эта последовательность может не являться выводом изA₁,A₂,...,A_n. Однако можно перед каждой формулойA_i,вставить дополнительные формулы так, чтобы превратить ее в вывод изA₁,A₂,...,A_n. Выбор дополнительных формул при каждомiзависит от того, чем оправдывается наличие формулы_iво вспомогательном выводе. Возможны следующие случаи:

1) _i– аксиома или подстановка в аксиому;

2) _i – одна из посылок A₁, A₂,..., A_n;

3) _i=A;

4) _i – modus ponens _x и _y, где x<i, y<i, причем _y=_x_i.

Рассмотрим для каждого из четырех случаев, на какую последовательность формул нужно заменить _i.

Случаи 1 и 2:

1) _i ,

2) _i(A_i) акс. 1 A_i, BA,

3) A_I m.p. 1 и 2.

Случай 3:

1) A(AA) акс. 1, BA,

2) (A(AA))((A((AA)A))(AA)) акс. 2, BAA, CA,

3) (A((AA)A))(AA) m.p. 1 и 2,

4) A((AA)A) акс. 1, BAA,

5) AA m.p. 4 и 3.

Случай 4:

Пусть _i– modus ponens_xи_y, гдеx<i,y<i, причем_y=_x_i. Пусть также в результирующем выводе формулаA_xимеет номерp, а формулаA(_x_i) имеет номер q.

1) (A_x)((A(_x_i))(A_i)) акс.2, AA, B_x, C_i ,

2) (A(_x_i))(A_i) m.p. p и 1,

3) A_i m.p. q и 2.

Следствие. A₁,A₂,...,A_nAтогда и только тогда, когда

 (A₁(A₂...(A_n-1(A_nA))...)).

Пример 34. Построить выводAB^B^A.

Рассмотрим на этом примере алгоритм, приведенный в доказательстве теоремы о дедукции.

Строим таблицу истинности для формулы ((AB)(^B^A)).

A	B	^B	^A	^B^A	AB	((AB)(^B^A))
0	0	1	1	1	1	1
0	1	0	1	1	1	1
1	0	1	0	0	0	1
1	1	0	0	1	1	1

Мы выяснили, что формула ((AB)(^B^A)) ТИФ, значит, выводAB^B^A существует (по следствию из теоремы о дедукции).

Вспомогательный вывод	Основной вывод
1'. ABпосылка	1. ABпосылка 2. (AB)(^B( AB)) акс. 1 AAB, B^B 3(1'). ^B( AB)m.p.1, 2
2'. (AB)((A^B)^A) акс. 9	4. (AB)((A^B)^A) акс. 9 5. (AB)((A^B)^A)(^B((AB)((A^B)^A)) акс. 1 A(AB)((A^B)^A),B^B 6(2'). ^B((AB)((A^B)^A))m.p.4, 5
3'. (A^B)^A m.p. 1'и2'	7. (^B( AB))((^B((AB)((A^B)^A))) (^B((A^B)^A))) акс. 2A^B,B(AB),C((A^B)^A) 8. (^B((AB)((A^B)^A)))(^B((A^B)^A))m.p.3, 7 9(3').^B((A^B)^A)m.p.6, 8
4'. ^B посылка	10. ^B(^B^B) акс. 1,A^B, B^B 11. (^B(^B^B))((^B((^B ^B)^B))(^B^B)) акс. 2, A^B,B^B^B,C^B, 12. ^B((^B^B)^B) акс. 1,A^B, B^B^B 13. (^B((^B^B)^B))(^B^B)m.p.10, 11 14(4'). ^B^Bm.p.12, 13
5'.^B(A^B) акс.1 A^B,BA	15. ^B(A^B) акс.1,A^B,BA 16. (^B(A^B))(^B(^B(A^B))) акс. 1A(^B(A^B)),B^B 17(5'). ^B(^B(A^B)m.p.15, 16
6'. A^B m.p.4' и 5'	18. (^B^B)((^B(^B(A^B)))(^B(A^B)))акс. 2.A^B,B^B,C(A^B) 19. (^B(^B(A^B)))(^B(A^B)) m.p.14, 18 20(6'). ^B(A^B)m.p.17, 19
7'. ^Am.p.6' и 3'	21. (^B(A^B))((^B((A^B)^A))(^B^A))акс. 2.A^B,B(A^B),C^A 22. (^B((A^B)^A))(^B^A) m.p.20, 21 23(7'). ^B^Am.p.9, 22

Отметим, что алгоритм, приведенный в доказательстве теоремы о дедукции, дает лишь способ получения из вспомогательного вывода ,A Bвывода AB, но не гарантирует оптимальности результирующего вывода. Очень часто полученный вывод можно сократить.

В качестве оптимального (с минимальным количеством формул) вывода AB^B^A(получен сокращением основного вывода) можно взять следующий вывод:

1". AB посылка,

2". (AB)((A^B)^A) акс. 9,

3". (A^B)^A m.p. 1" и 2",

4". ((A^B)^A)(^B((A^B)^A))

акс.1 A(A^B)^A), B^B,

5". ^B((A^B)^A) m.p. 3" и 4",

6". ^B(A^B) акс.1 A^B, BA,

7". (^B (A^B))(( ^B ((A^B)^A))( ^B ^A))

акс. 2 A^B, B(A^B), C^A,

8". ( ^B ((A^B)^A))( ^B ^A)

m.p.6" и 7",

9". ^B^A m.p. 5" и 8".