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

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

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

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

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

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

1. если Г├ А B, то Г, А├ B. В частности,

2. если ├ А B, то А ├B.

Следствия:

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

2. Если ├ A₁…A_n B, то A₁,...,A_n├ B.

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

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

1. если Г, А├B, то Г├АB. В частности,

2. если А├В, то ├АB.

Следствия.

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

2. если А₁, ..., А_п-1, А_п├В, то ├A₁…A_nB.

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

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

Пример 6.

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

Данный вывод		Результирующий вывод
		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)

Пример 7.

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

Данный вывод		Результирующий вывод
		1. А  (В С)	1. посылка
		2. (А  (В С))(АВ(А(В С)))	2.
1. А(В С)	1. посылка	3. АВ (А  (В С))	3. МР(F1,F2)
		4.(АВ(ВАВ))((АВ((ВАВ) АВ)) (АВ АВ))	4.
		5. АВ(ВАВ)	5.
		6.(АВ((ВАВ)АВ))(АВАВ)	6. МР(F4,F5)
		7. АВ((ВАВ)АВ)	7.
2. АВ	2. посылка	8. АВАВ	8. МР(F6,F7)
		9. АВА	9. АС4
		10. (АВА)(АВ(АВА))	10.
3. АВА	3. АС4	11. АВ(АВА)	11. МР(F9,F10)
		12.(АВАВ)((АВ(АВА))(А ВА))	12.
		13. (АВ(АВА))(АВА)	13. МР(F8,F12)
4. А	4. МР(F2,F3)	14. АВА	14. МР(F11,F13)
		15. АВВ	15. АС5
		16. (АВВ)(АВ(АВВ))	16.
5. АВВ	5. АС5	17. АВ(АВВ)	17. МР(F15,F16)
		18.(АВАВ)((АВ(АВВ))(А ВВ))	18.
		19. (АВ(АВВ))(АВВ)	19. МР(F8,F18)
6. В	6. МР(F2,F5)	20. АВВ	20. МР(F17,F19)
		21.(АВА)((АВ(А(ВС)))(АВ (ВС)))	21.
		22. (АВ(А(ВС)))(АВ(ВС))	22. МР(F14,F21)
7. ВС	7. МР(F1,F4)	23. АВ(ВС)	23. МР(F3,F22)
		24. (АВВ)((АВ(ВС))(АВС))	24.
		25. (АВ(ВС))(АВС)	25. МР(F20,F24)
8. С	8. МР(F6,F7)	26. АВС	26. МР(F23,F25)