Теорема дедукции
[предыдущая глава]  [оглавление]  [следующая глава]

Теорема дедукции, доказанная Эрбраном,- по-видимому самый эффективный прием в классическом исчислении высказываний. Хотя она и называется "теоремой" дедукции - это не теорема КИВ, а метод, который применяется для доказательства теорем КИВ. То есть, как говорят, метатеорема.

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

Если имеется доказательство

G1, G2,..., Gβ-1, Gβ R,

то можно составить доказательство

G1, G2,..., Gβ-1 Gβ R

Проще говоря, значок можно переносить справа налево, на место запятой, оставляя вместо него на каждом шаге символ :

G1, G2, G3, G4 R

G1, G2, G3 G4 R

G1, G2 G3 (G4 R)

G1 G2 (G3 (G4 R))

G1 (G2 (G3 (G4 R)))

Обратное движение также допустимо, причем, обоснование этого (в отличии от метатеоремы дедукции) элементарно. Пусть у нас имеется старое доказательство:

G1, G2,..., Gβ-1 Gβ R

Построим на его основе новое доказательство:

G1, G2,..., Gβ-1, Gβ R

Если R - аксиома, или одна из гипотез G1, G2,..., Gβ, то новое доказательство получится сразу (длиной в 0 строк). Иначе возьмем старое доказательство целиком и добавим в его конец одну дополнительную строку:

Gβ, Gβ R R // MP

- старое доказательство плюс одна эта строка как раз и составят новое доказательство.

Самое крайнее положение значка при движении вправо - перед последней формулой R (дальше modus ponens двигать значок не позволяет). Самое крайнее положение значка при движении влево - с краю формулы. При движении значка вправо символ должен ставится на место операции , которая обрабатывается (согласно скобкам и приоритетам) самой последней. Если в формуле последней обрабатывается другая операция, то дальнейшее движение значка невозможно. При движении влево надо не забывать расставлять скобки, чтобы в образовавшейся формуле новый символ обрабатывался (согласно скобкам и приоритетам) самым последним.

Обратите внимание, что в доказательстве МТД нам ни разу не понадобилась информация о том, в каком порядке следуют гипотезы G1, G2,..., Gβ-1. Поэтому мы можем их свободно переставлять. Все вместе предоставляет нам интересный прием: сначала передвигаем значок до упора вправо, потом переставляем гипотезы как хочется и передвигаем значок до упора влево. В результате получаем новую теорему, доказанную без всяких гипотез - только из аксиом. Этот прием мы используем в следующей главе.

Рассмотрим пример применения МТД. Дано доказательство:

a b, b c, a c

Тело доказательства состоит из двух строк:

1) a, a b b // MP
2) b, b c c // MP

Требуется с помощью МТД построить доказательство:

a b, b c a c

Значения переменных, которые упоминаются в МТД:

β = 3, γ = 2, δ = 0, G1 = a b, G2 = b c, Gβ = a, B1 = b, B2 = c, R = c

Новое доказательство:

2.1.1) Imp1 (ab) (a(ab)) // a ~> ab, b ~> a
2.1) (ab), №2.1.1 a(ab) // MP
 
2.2.1) Imp1 (bc) (a(bc)) // a ~> bc, b ~> a
2.2) (bc), №2.2.1 a(bc) // MP
 
2.3.1)Imp1 a(ba)// a ~> a
2.3.2)Imp1 a(baa)// a ~> a, b ~> ba
2.3.3)Imp2 a(ba) (a(baa)(aa))// a ~> a, b ~> ba, c ~> a
2.3.4)№2.3.1, №2.3.3 a(baa)(aa)// MP
2.3) №2.3.2, №2.3.4 aa// MP
 
3.1.1) Imp2 (aa) ((a(ab)) (ab)) // a ~> a, b ~> a, c ~> b
3.1.2) aa, №3.1.1 (a(ab)) (ab) // MP
3.1) a(ab), №3.1.2 ab // MP
 
3.2.1) Imp2 (ab) ((a(bc)) (ac)) // a ~> a, b ~> b, c ~> c
3.2.2) ab, №3.2.1 (a(bc)) (ac) // MP
3.2) a(bc), №3.2.2 ac // MP

Скажу честно: это доказательство я "писал" путем копирования строк из доказательства МТД с последующей заменой всяких Gβ на нужные строки. Собственно, с такой работой мог бы справиться и компьютер. Посмотрите на то, что получилось. Доказательство, вроде бы, правильное, но избыточное. Кое-где, кое-что можно сократить. В результате подстановки в формулах 2.3.1 и 3.2.1 получаются аксиомы, эти строки можно убрать, а ссылки на эти строки заменить ссылками на аксиомы. В строках 3.1.1 - 3.1 доказывается одна из гипотез, что излишне, поэтому эти строки можно убрать. После того, как мы их уберем, окажется, что формула aa, полученная в строках 2.3.2 - 2.3, больше нигде не используется, так что эти строки тоже можно убрать целиком. После того, как мы его уберем, оказываются ненужными строки 2.1.1 - 2.1. В строке 3.2 можно заменить формулу на ее номер. После всех описанных сокращений получится доказательство:

2.2.1) Imp1 (bc) (a(bc)) // a ~> bc, b ~> a
2.2) (bc), №2.2.1 a(bc) // MP
 
3.2.2) ab, Imp2 (a(bc)) (ac) // MP
3.2) №2.2, №3.2.2 ac // MP

Все, что осталось - 4 строки. Собственно, мы бы могли найти столь короткое решение мысленно, угадывая. Однако, благодаря МТД, процесс поиска доказательства оказывается чисто механическим, доступным даже для компьютера. Да и последующую работу по убиранию лишних строк вполне можно было бы поручить компьютеру (кстати, составление подобной программы - неплохая тема для какого-нибудь курсового проекта студента-программиста).