Математика - Классическое исчисление высказываний

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

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

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

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

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 - аксиома, или одна из гипотез G_₁, G_₂,..., 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

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

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

1.1)	?	G_{_β} A_₁	// ?
1.2)	?	G_{_β} A_₂	// ?
...
1.δ)	?	G_{_β} A_{_δ}	// ?

2.1)	?	G_{_β} G_₁	// ?
2.2)	?	G_{_β} G_₂	// ?
...
2.β)	?	G_{_β} G_{_β}	// ?

3.1)	?	G_{_β} B_₁	// ?
3.2)	?	G_{_β} B_₂	// ?
...
3.γ)	?	G_{_β} B_{_γ}	// ?

1.ω.1)	Imp1	A_{_ω} (G_{_β} A_{_ω})	// a ~> A_{_ω}, b ~> G_{_β}
1.ω)	A_{_ω}, №1.ω.1	G_{_β} A_{_ω}	// MP

2.ω.1)	Imp1	G_{_ω} (G_{_β} G_{_ω})	// a ~> G_{_ω}, b ~> G_{_β}
2.ω)	G_{_ω}, №2.ω.1	G_{_β} G_{_ω}	// MP

2.β.1)	Imp1	G_{_β}(BG_{_β})	// a ~> G_{_β}
2.β.2)	Imp1	G_{_β}(BG_{_β}G_{_β})	// a ~> G_{_β}, b ~> BG_{_β}

2.β.3)	Imp2	G_{_β}(BG_{_β}) (G_{_β}(BG_{_β}G_{_β})(G_{_β}G_{_β}))	// a ~> G_{_β}, b ~> BG_{_β}, c ~> G_{_β}

2.β.4)	№2.β.1, №2.β.3	G_{_β}(BG_{_β}G_{_β})(G_{_β}G_{_β})	// MP
2.β)	№2.β.2, №2.β.4	G_{_β}G_{_β}	// MP

2.β.1)	Imp1	G_{_β}(BG_{_β})	// a ~> G_{_β}
2.β.2)	Imp1	G_{_β}(BG_{_β}G_{_β})	// a ~> G_{_β}, b ~> BG_{_β}

2.β.3)	Imp2'	G_{_β}(BG_{_β}G_{_β}) (G_{_β}(BG_{_β})(G_{_β}G_{_β}))	// a ~> G_{_β}, b ~> BG_{_β}, c ~> G_{_β}

2.β.4)	№2.β.2, №2.β.3	G_{_β}(BG_{_β})(G_{_β}G_{_β})	// MP
2.β)	№2.β.1, №2.β.4	G_{_β}G_{_β}	// MP

1)	...	B_₁	// ...
2)	...	B_₂	// ...
3)	...	B_₃	// ...
...
γ)	...	B_{_γ}	// ...

3.ω.1)	X	B_{_ω}	// ...
3.ω.2)	Imp1	B_{_ω} (G_{_β} B_{_ω})	// a ~> B_{_ω}, b ~> G_{_β}
3.ω)	№3.ω.2, №3.ω.1	G_{_β} B_{_ω}	// MP

3.ω.1)	Imp2	(G_{_β} X_{_ω}) ((G_{_β} (X_{_ω} B_{_ω})) (G_{_β} B_{_ω}))	// a ~> G_{_β}, b ~> X_{_ω}, c -> B_{_ω}
3.ω.2)	G_{_β} X_{_ω}, №3.ω.1	(G_{_β} (X_{_ω} B_{_ω})) (G_{_β} B_{_ω})	// MP
3.ω)	G_{_β} (X_{_ω} B_{_ω}), №3.ω.2	G_{_β} B_{_ω}	// MP

3.ω.1)	Imp2'	(G_{_β} (X_{_ω} B_{_ω})) ((G_{_β} X_{_ω}) (G_{_β} B_{_ω}))	// a ~> G_{_β}, b ~> X_{_ω}, c -> B_{_ω}
3.ω.2)	G_{_β} (X_{_ω} B_{_ω}), №3.ω.1	(G_{_β} X_{_ω}) (G_{_β} B_{_ω})	// MP
3.ω)	G_{_β} X_{_ω}, №3.ω.2	G_{_β} B_{_ω}	// MP

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