Теорема дедукции

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

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

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

G₁, G₂,..., G_β-1, G_β |— R,

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

G₁, G₂,..., G_β-1 G_β |— R

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

G₁, G₂, G₃, G₄ |— R

G₁, G₂, G₃ |— G₄ => R

G₁, G₂ |— G₃ => (G₄ => R)

G₁ |— G₂ => (G₃ => (G₄ => R))

|— G₁ => (G₂ => (G₃ => (G₄ => R)))

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

G₁, G₂,..., G_β-1 |— G_β => R

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

G₁, G₂,..., G_β-1, G_β => R

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

G_β, G_β => R |— R // MP

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

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

Обратите внимание, что в доказательстве МТД нам ни разу не понадобилась информация о том, в каком порядке следуют гипотезы G₁, G₂,..., 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, G₁ = a b, G₂ = b c, G_β = a, B₁ = b, B₂ = 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

Посмотрите на то, что получилось. Доказательство, вроде бы, правильное, но избыточное. Кое-где, кое-что можно сократить. В результате подстановки в формулах 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 строки. Собственно, мы бы могли найти столь короткое решение мысленно, угадывая. Однако, благодаря МТД, процесс поиска доказательства оказывается чисто механическим, доступным даже для компьютера.