Mat_Logika_Algebra_i_ischislenie_vyskazyvany

31

Γ выводима формула A B , т.е. из Γ, A├─B следует Γ├─A B . Доказательство проведем методом математической индукции по длине

вывода формулы B из Γ {A}. Пусть B1,..., Bn = B – вывод формулы B из

Γ{A}.

α) База индукции: n =1, так что вывод состоит из одной формулы B1 = B .

Возможны три случая:

а) B1 Γ; б) B1 – аксиома; в) B1 = A.

Для случаев а) и б) построение вывода одинаково, различия лишь в скобках.

Помним, что B1 = B .

Для случая в) вывод очевиден, т.к. формула A B имеет вид A A, но это Т1, и по Св.1 – Γ├─A A.

β) Индукционный переход. Предположим, что для всех выводов формулы

Bk из Γ {A} длины k < n существует вывод Γ├─ A Bk .

γ ) Докажем, что тогда из Γ, A├─Bn следует Γ├─ A Bn .

Возможны четыре случая:

а) Bn Γ; б) Bn – аксиома; в) Bn = A,

г) Bn получена применением МР к предыдущим формулам Bi и Bj .

Для случаев а), б) и в) построение вывода аналогично пункту α) , а для г)

очевидно, имело место Bj = Bi Bn . Так как ному предположению β) :

1. Γ├─ A Bi (β).

32

2.Γ├─ A Bj , т.е. Γ├─ A (Bi Bn ) (β).

3.( A (Bi Bn )) (( A Bi ) ( A Bn )) (А2).

4.Γ├─ ( A Bi ) ( A Bn ) (МР к 2, 3)

5.Γ├─ A Bn (МР к 1, 4).

Что и требовалось доказать, т.к. Bn = B . ■

Ссылку на применение этой теоремы будем обозначать (Т. о д. к n). Выведем три следствия из этой теоремы. Ссылки на следствия – (Сл. n).

Следствие 1. (правило силлогизма)

A B , B C ├─A C .

1.A B (гипотеза).

2.A (гипотеза).

3.B (МР к 2, 1).

4.B C (гипотеза).

5.C (МР к 3, 4). Это значит, что A B , A, B C ├─C .

6.A B , B C , A├─C (Св.4 к 5).

7.A B , B C ├─A C (Т. о д. к 6). ■

Следствие 2.

├─ ( A B) (¬B ¬A).

1.A B (гипотеза).

2.(¬¬A ¬¬B) (¬B ¬A) (А3).

3.B ¬¬B (Т6).

4.A ¬¬B (Сл.1 к 1, 3).

5.¬¬A A (Т5).

6.¬¬A ¬¬B (Сл.1 к 5, 4).

7.¬B ¬A (МР к 6, 2). Это значит, что A B ├─¬B ¬A.

8.├─( A B) (¬B ¬A) (Т. о д. к 7). ■

33

Следствие 3. (правило перевертывания) Если Γ, A├─B , то Γ,¬B ├─¬A.

1.Γ, A├─B (условие).

2.Γ├─A B (Т. о д. к 1).

3.( A B) (¬B ¬A) (Сл.2).

4.Γ├─¬B ¬A (МР к 2, 3).

5.¬B (гипотеза).

6.Γ,¬B ├─¬A. (МР к 5, 4). ■

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

Для сокращения формул (в смысле количества символов, входящих в нее) введем две «новые–старые» (новые в АТЧ, но известные из алгебры высказываний) связки – конъюнкцию и дизъюнкцию, по следующим соотношениям:

A & B обозначает формулу ¬( A ¬B) ;

A B обозначает формулу ¬A B .

Такое введение связок оправдывается равносильностями алгебры высказываний (см. стр. 7), но следует иметь ввиду, что в явном виде все эти равносильности в АТЧ не применяются, т.е. нельзя в формуле АТЧ просто заменить ¬¬A на A, используя инволютивность. Для этого надо построить соответствующий вывод. Производные правила вывода для введенных связок следует рассматривать лишь как сокращение некоторой последовательности формул вывода до одной формулы. Ссылку на примененное производное правило будем обозначать – Пn (n – номер правила).

П1. A & B ├─ A.

1. ¬A ( A B) (Т3).

34

2.¬A├─ A ¬B (МР к 1).

3.¬( A ¬B)├─ ¬¬A (Сл.3 к 2).

4.¬¬A A (Т5).

5.¬( A ¬B)├─ A (МР к 3, 4). Это значит, что A & B ├─ A. ■

П2. A & B ├─ B .

1.¬B, A├─ ¬B (Св.3).

2.¬B ├─ A ¬B (Т. о д. к 1).

3.¬( A ¬B)├─ ¬¬B (Сл.3 к 2).

4.¬¬B B (Т5).

5.¬( A ¬B)├─ B (МР к 3, 4). Это значит, что A & B ├─ B . ■

П3. A, B ├─ A & B .

1.A, A ¬B ├─ ¬B (МР).

2.A,¬¬B ├─ ¬( A ¬B) (Сл.3 к 1).

3.A, B ├─ A (Св.3).

4.A, B, B ¬¬B ├─ ¬¬B (МР).

5.A, B ├─ ¬¬B (Св.6 к 4).

6.A, B ├─ ¬( A ¬B) (Св.7 к 3, 5, 2). Это значит, что A, B ├─ A & B . ■

П4. A├─ A B .

1.A ¬¬A (Т6).

2.¬¬A (¬A B) (Т3).

3.A (¬A B) (Сл.1 к 1, 2).

4.A├─ ¬A B (МР к 3). Это значит, что A├─ A B . ■

П5. B ├─ A B .

35

1.B,¬A├─ B (Св.3).

2.B ├─ ¬A B (Т. о д. к 1). Это значит, что B ├─ A B . ■

П6. Если A├─ C и B ├─ C , то A B ├─ C .

1.A├─ C (условие).

2.¬C ├─ ¬A (Сл.3 к 1).

3.B ├─ C (условие).

4.¬C ├─ ¬B (Сл.3 к 3).

5.¬A,¬B ├─ ¬A & ¬B (П3).

6.¬C ├─¬A & ¬B (Св.7 к 2, 4, 5).

7.¬(¬A & ¬B) ├─¬¬C (Сл.3 к 6). Отметим, что формула ¬(¬A & ¬B)

обозначает формулу ¬¬(¬A ¬¬B) . Поэтому, если «снять» все двой-

ные отрицания, получим необходимый вывод.

8.¬¬C C (Т5).

9.¬¬(¬A ¬¬B) ├─C (МР к 7, 8).

10.(¬¬(¬A ¬¬B)) C (Т. о д. к 9).

11.(¬A ¬¬B) (¬¬(¬A ¬¬B)) (Т6).

12.(¬A ¬¬B) C (Сл.1 к 11, 10).

13.¬A B, B ¬¬B ├─¬A ¬¬B (Сл.1).

14.¬A B ├─¬A ¬¬B (Св.6 к 13).

15.¬A B ├─C (МР к 14, 12). Это значит, что A B ├─ C . ■

П7. Если A├─ B и A├─ ¬B , то ├─ ¬A.

1.A├─ B (условие).

2.¬B ├─ ¬A (Сл.3 к 1).

3.A├─ ¬B (условие).

4.¬¬B ├─ ¬A (Сл.3 к 3).

5.¬B ¬¬B ├─ ¬A (П6 к 2, 4).

36

6. ├─ ¬A (Св.6 к 5). Формула ¬B ¬¬B является обозначением формулы ¬¬B ¬¬B , а это Т1, т.е. ее можно удалить из списка гипотез. ■

2.4. Полнота и непротиворечивость аксиоматической теории Чёрча

Множество гипотез Γ называется противоречивым, если из него одно-

временно выводятся формулы A и ¬A , т.е. Γ├─ A и Γ├─ ¬A . В противном случае Γ называется непротиворечивым.

Аксиоматическая теория называется непротиворечивой, если не суще-

ствует формулы A такой, что одновременно├─ A и ├─ ¬A , т.е. сама формула, и ее отрицание одновременно выводимы (являются теоремами).

Аксиоматическая теория называется полной (в широком смысле), если любая формула являющаяся тавтологией выводима в этой теории.

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

Аксиоматическая теория называется альтернативной, если для каждой формулы A этой теории, либо ├─ A , либо ├─ ¬A .

Лемма.

этой оценке списка переменных, и:

Доказательство проведем методом математической индукции по l(A) –

длине формулы A , равной числу k вхождений связок в формулу.

I)A = ¬B и II) A = B C .

I)A = ¬B. Список переменных формулы B, очевидно, совпадает со спи-

а) Если εI = Л , то ε = И . Aε = A , и BεI =¬B. По β) имеет место

X1ε1 ,..., Xnεn ├─ BεI = ¬B= A = Aε .

б) Если εI = И , то ε = Л . Aε =¬A , и BεI =B. По β) имеет место

1.X1ε1 ,..., Xnεn ├─ BεI =B (β).

2.B = ¬¬B (Т6).

3.X1ε1 ,..., Xnεn ├─ ¬¬B = ¬A = Aε (МР к 1, 2).

II)A = B C . Так как l(B) +l(C) = l(A) −1 = k −1 < k и длины неотри-

цательны, то 0 ≤ l(B),l(C) ≤ k −1 < k , и к ним применимо индукционное допущение. Списки переменных формулы B и C, очевидно, являются подмножествами списка переменных формулы A . Значение каждой из них на оценке <ε1,...,εn > находится подстановкой в «свои» переменные, если они входят в формулу. Пусть εI =B(ε1,...,εn ) и εII =C(ε1,...,εn ) . То-

39

венное правило вывода MP, примененное к тавтологиям, снова приводит к тавтологии (см. стр. 9). Поэтому каждая теорема является тавтологией. ■

Теорема. (о полноте АТЧ)

Любая тавтология является теоремой АТЧ. Доказательство

Пусть формула A – тавтология, зависящая от пропозициональных пе-

ременных X1,..., Xn . На любой оценке списка этих переменных <ε1,...,εn >

она принимает значение Истина. В силу леммы, учитывая что Aε = A :

X1ε1 ,..., Xnεn ├─ A .

Для двух различных оценок <ε1,...,εn−1, И > и <ε1,...,εn−1, Л >, соответственно:

X1ε1 ,..., Xnε−n−11 , Xn ├─ A и X1ε1 ,..., Xnε−n−11 ,¬Xn ├─ A .

Применяя к ним П6 получим:

X1ε1 ,..., Xnε−n−11 , Xn ¬Xn ├─ A .

Формула Xn ¬Xn ≡¬Xn ¬Xn есть Т1, и по Св.6 может быть уда-

лена из списка гипотез, т.е. из списка гипотез будет удалена X n :

X1ε1 ,..., X nε−n−11 ├─ A .

Аналогичным образом можно удалить из списка гипотез Xn−1 и так да-

лее все пропозициональные переменные. В результате получим:

├─ A . ■

Замечание. Теорема о полноте дает простой алгоритм проверки выводимости логических формул: достаточно проверить ее на тавтологичность, т.е., например, построить таблицу истинности.

Пример.

Выводима ли формула A & B из формулы A B ?

40

Предположим, что выводима, т.е. A B ├─A & B . Тогда по Теореме о дедукции ├─( A B) ( A & B), но эта формула не является тавтологией.

Например, на оценке <И, Л> она принимает значение Л.

Теорема. (о непротиворечивости АТЧ)

АТЧ является непротиворечивой теорией. Доказательство

Пусть ├─ A . Тогда по Теореме о полноте A – тавтология. Следова-

тельно, ¬A – противоречие и по Теореме о корректности не является теоремой АТЧ, т.е. невыводима. ■

Теорема. (об альтернативности АТЧ)

АТЧ не является альтернативной теорией. Доказательство

В АТЧ существуют формулы, которые невыводимы сами вместе со своими отрицаниями. Например, A B . ■

Теорема. (об абсолютной непротиворечивости АТЧ)

АТЧ является абсолютно непротиворечивой теорией. Доказательство

Пусть F – невыводимая формула в АТЧ (это может быть любая не тож-

дественно истинная формула); X1,..., Xn – ее список переменных, и на оценке списка этих переменных <ε1,...,εn > она принимает значение Ложь. Пусть

A произвольная формула. Определим формулы Bi по следующей схеме:

Тогда формула F(B1,...,Bn ) – противоречие (тождественно ложная), по по-