5. Свойства отношений выводимости
Метатеорема 1 (МТ1).
А1,...,An ├ Аi(i=1,…,n).
Если A1,...,An├ B1, ..., A1,...,An├ Bk и B1,...,Bk├ С, то A1,...,Ап├ С.
Метатеорема 2 (МТ2).
Пусть Г- любое множество формул. Тогда:
если Г├ А B, то Г, А├ B. В частности,
если ├ А B, то А ├B.
Следствия:
Если ├ A1(…(An-1(AnB))…), то A1,...,An├ B.
Если ├ A1…An B, то A1,...,An├ B.
Метатеорема 3 (МТ3), теорема дедукции (ТД), правило введения импликации (ВИ).
Пусть Г - любое множество формул. Тогда:
если Г, А├B, то Г├АB. В частности,
если А├В, то ├АB.
Следствия.
Если А1, ..., Ап-1, Ап├В, то ├А1(…(Аn-1(АnB))…). В частности,
если А1, ..., Ап-1, Ап├В, то ├A1…AnB.
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) |
