Пример 6. Применение метода доказательства теоремы дедукции для преобразования данного вывода в результирующий вывод

Применение метода доказательства теоремы дедукции для преобразования данного вывода в результирующий вывод.

Следствия.

Метатеорема 2 (МТ2).

Метатеорема 1 (МТ1).

Свойства отношений выводимости

a) А₁,...,A_n ├ А_i (i=1,…,n).

b) Если A₁,...,A_n├ B₁,..., A₁,...,A_n├ B_k и B₁,...,B_k├ С, то A₁,...,А_п├ С.

Пусть Г- любое множество формул. Тогда:

a) если Г├ АÉ B, то Г, А├ B. В частности,

b) если ├ АÉ B, то А ├B.

Следствия:

a) Если ├ A₁É(…É(A_n-1É(A_nÉB))…), то A₁,...,A_n├ B.

b) Если ├ A₁Ù…ÙA_n ÉB, то A₁,...,A_n├ B.

Метатеорема 3(МТ3), теорема дедукции (ТД), правило введения импликации (ВИ).

Пусть Г - любое множество формул. Тогда:

a) если Г, А├B, то Г├АÉB. В частности,

b) если А├В, то ├АÉB.

a) Если А₁,..., А_п-1, А_п├В, то ├А₁É(…É(А_n-1É(А_nÉB))…). В частности,

b) если А₁,..., А_п-1, А_п├В, то ├A₁Ù…ÙA_nÉB.

В доказательстве теоремы дедукции описан алгоритм преобразования данного вывода в результирующий. (см. теоретический материал). Рассмотрим этот алгоритм в следующих примерах.

Проиллюстрировать метод доказательства теоремы дедукции, преобразовав вывод А É (ВÉ С), В, А├ С в вывод А É (ВÉ С), В├АÉ С.

Данный вывод	Результирующий вывод
		1. А É (ВÉ С)	1. посылка
		2. (А É (ВÉ С))É (АÉ (А É (ВÉ С)))	2.
1. А É (ВÉ С)	1. посылка	3. АÉ (А É (ВÉ С))	3. МР(F1,F2)
		4. В	4. посылка
		5. ВÉ (А É В)	5.
2. В	2. посылка	6. A É В	6. МР(F4,F5)
		7. (А É (ВÉ А))É ((А É ((ВÉ А)É А))É É (АÉ А))	7.
		8. А É (ВÉ А)	8. АС1
		9. (А É ((ВÉ А)É А))É (АÉ А)	9. МР(F7,F8)
		10. (А É ((ВÉ А)É А))	10.
3. A	3. посылка	11. АÉ А	11. МР(F9,F10)
		12. (АÉА)É((АÉ(АÉ(ВÉС)))É(АÉ(ВÉ ÉС)))	12.
		13. (АÉ(АÉ(ВÉС)))É(АÉ(ВÉС))	13. МР(F11,F12)
4. ВÉ С	4. МР(F1,F3)	14. АÉ(ВÉС)	14. МР(F3,F13)
		15. (АÉВ)É((АÉ(ВÉС))É(АÉС))	15. АС2
		16. (АÉ(ВÉС))É(АÉС)	16. МР(F6,F15)
5. С	5. МР(F2,F4)	17. АÉ С	17. МР(F14,F16)

Дата добавления: 2015-06-27