yandex rtb 1
ГоловнаЗворотній зв'язок
yande share

Математическая логика

3.4. Метатеорема дедукции

Метатеорема дедукции (МТД)

Если из множества формул Г и формулы А выводима формула В, то из

множества Г выводима формула АВ, т. е. Г, А|—В  Г——АВ.

Доказательство этой метатеоремы может быть проведено по методу математической индукции. Пусть вывод формулы В - это последовательность В1, В2,...,Вn=В. Докажем, что выполняется металемма:

Металемма. Г, А|——В1 Г|——АВ, (i=l,...,n).

 Доказательство металеммы

Базис индукции. Рассмотрим три случая:

а) | В1, т.е. В1 – аксиома;

    | В1В1)                                                                     А1

    | — АВ1  Г|—АВ1                                                       по МР

б) В1 = А;

|—ААГ|ААГ|АВ1;                                       Т1

 в) B1 Г, т.е. В1, - гипотеза из Г;

Доказательство проводится так же, как и в случае а).

 Шаг индукции. Пусть металемма выполнена для всех k<i. Докажем, что она выполняется при k = i. Возможны 4 случая:

а) В1 - аксиома;                доказательство проводится

б) В1 =А;                           таи же, как и для базиса

в) В1 Г                            индукции

г) В1 выводится по МР из предыдущих формул, т.е. в последовательности есть формулы:

Вm;

В1=ВmВ1 (m<l<i) и по предположению индукции справедливы выводы

Г| —ABm

Г|—АВ1 Г|—А( Bm  В1)

По схеме аксиом А2

( Bm  В1)) ((А  Bm ) В1))

Применяя дважды к последним трем выражениям правило МР, получим

Г|— А  В1

При i=n получим формулировку метатеоремы дедукции.

Справедлива метатеорема, обратная метатеореме о дедукции:

Метатеорема 2.

Если существует вывод Г| — А  В, то формула В выводима из Г и А:

 Г | — А  В  Г,А|— В

Доказательство: Пусть вывод формулы А  В имеет вид В1, В2, .... Вn-1 А  В, где В1, В2, .... Вn-1  формулы из множества Г. Тогда вывод формулы В из Г и А будет иметь вид В1, В2, .... Вn-1 А В, А, В, т.к. В следует из А В и А по правилу МР.

Докажем некоторые следствия из метатеоремы о дедукции.

Следствие   1.(В1). Правило силлогизма : А В, ВС| — АС (см. 2.3).

Следствие   2.(В2) Правило удаления средней посылки: АС), В|— АС (см.2.3).

Следствие 3.(ВЗ) Правило удаления крайней посылки: (АВ)С|—ВС.

Пользуясь обратной теоремой дедукции, будем строить вывод: (АВ)С, В|— С

1.В                                                                                      Г1

2. (АВ) С                                                                 Г2

3. В В)                                                                А1

4. А В                                                                            МР(1,3)          

5. С                                                                                     МР(2,4)

Теперь, по теореме дедукции, получаем вывод: (А В) С |—В сС.

Полезно сравнить доказательства этих правил вывода, получаемые при применении теоремы о дедукции и без ее применения.

Метатеорема о дедукции и следствия из нее являются производными правилами вывода. Их применение позволяет упрощать построение выводов и доказательств.

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

Теорема 3.            |—¬¬АА (снятия двойного отрицания)

1.(¬А¬¬А) ((¬А¬А) А)                                 А2

2. ¬А¬А                                                                        Т1

3.(¬А¬¬А) А.                                                          Сл.2(1,2)

4. ¬¬АА.                                                                       Сл.3(3)

Теорема 4.            |—А¬¬А (введение двойного отрицания)

1. (¬¬¬А¬А) ((¬¬¬АА) ¬¬А)                       А2

2. ¬¬¬А¬А                                                                   Т3

3. (¬¬¬АА) ¬¬А                                                      МР(1,2)

4. А¬¬А.                                                                       Сл.3(3)

Теорема 5.            |—¬АВ) (противоречия)

Воспользуемся обратной теоремой дедукции один раз: ¬А |—АВ и еще раз: ¬А,

А|—В. Построим вывод.

1. ¬А                                                                                  Г1

2. А                                                                                                Г2

3. (¬В¬А) ((¬ВА) В)                         А3

4. ¬А(¬В¬А)                                                           А1

5. А(¬ВА)                                                                А1

6. ¬В¬А                                                                        МР(1,4)

7. ¬ВА                                                                          МР(2,5)

8. (¬ВА) В                                                               МР(3,6)

9. В                                                                                     МР(7,8)

Применяя к полученному выводу два раза теорему дедукции, получаем доказательство теоремы.

Теорема 6.           |—(¬А¬В) А) (контрапозиции)

1. ¬А¬В                                                                        Г1

2. (¬А¬В) ((¬АВ) А)                                     А3

3. (¬АВ) А                                                               МР(1,2)

4. ВА                                                                             Сл.

Теорема 7.             |—(ВА) (¬А¬В) (контрапозиции)

ВА |—¬А¬В

1.    ВА                                                                          Г1

2.   ¬¬ВВ                                                                      Т3

3.  А¬¬А                                                                       Т4

4.  ¬¬ВА                                                                       Сл.1(2,1)

5.  ¬¬В¬¬А                                                                   Сл.1(3,4)

6. (¬¬В¬¬А) (¬А¬В)                                         Т6

7. ¬А¬В                                                                        МР(5,6)

Терема 8.              |—А(¬В¬(АВ))  А|—¬В¬(АВ)

1. ((АВ) В) (¬В¬(АВ))                             Т7

2. А                                                                                                Г1

3. А,АВ|—В                                                                 МР

4. А|—(АВ) В                                                          МТД(3)

5. (АВ) В                                                                 Сл.из(2,4)

6. ¬В¬(АВ)                                                              МР(1,5)

       В доказательстве этой теоремы фактически использовались средства метаязыка – было получено новое правило вывода: А|—(АВ) В.

Теорема 9.            |—(АВ) ((¬АВ) В)        АВ, ¬АВ|—В

1. АВ                                                                             Г1

2. ¬АВ                                                                          Г2

3. (АВ) (¬В¬¬А)                                                Т6

4. (¬АВ) (¬В¬¬А)                                              Т6

5. ¬В¬А                                                                        МР(1,3)

6. ¬В¬¬А                                                                      МР(2,4)

7. (¬В¬¬А) ((¬В¬А) В)                                A3

8. (¬В¬А) В                                                             МР{6,7)

9.   В                                                                                   МР(5,8)

 

 

20