3. Правило вывода Modus ponens
Определение 2. Правилом вывода теории L называют процедуру перехода от двух формул вида А и А B к одной формуле вида В для любых А и В.
Это правило называют modus ponens, MP. Правило МР позволяет удалять оператор , поэтому его называют также правилом удаления импликации и обозначают УИ. В случае применения правила МР формулы А и A В называют посылками, а В - заключением этого правила.
4. Формальное доказательство и формальный вывод
Определение 3. Формальным доказательством (в теории L) называется конечная последовательность формул В1, ..., Bk, причем каждая формула этой последовательности либо аксиома, либо получена по правилу МР из каких-либо двух предшествующих формул этой последовательности. Формальное доказательство является доказательством своей последней формулы Вk. Формула В называется формально доказуемой, или формальной теоремой (теории L), если она имеет формальное доказательство.
Утверждение «Формула В формально доказуема в теории L» будем обозначать ├LВ.
Пример 1.
Построить доказательство формулы A B B A
|
1.
|
|
2.
|
|
3. МР(F1,F2) |
|
4.
|
|
5. МР(F3,F4) |
|
9. ОФД (1-5) – определение формального доказательства |
Пример 2.
Построить доказательство формулы A A А
|
1.
|
|
2. АС10 |
|
3. МР(F1,F2) |
|
4.
|
|
5. МР(F3,F4) |
|
9. ОФД (1-5) – определение формального доказательства |
Обобщим понятие формального доказательства на случай вывода некоторой формулы B из других формул А1,...,Ап, называемых посылками (гипотезами).
Определение 4. Формальным выводом формулы В из посылок А1,..., Ап называется конечная последовательность формул В1,...,Bk, заканчивающаяся формулой B (Bk = В), причем каждая формула этой последовательности
или одна из посылок А1, ..., Аn,
или аксиома,
или формула, полученная из некоторых двух предшествующих формул этой последовательности по правилу МР.
Если существует формальный вывод формулы В из формул А1,...,Ап, то формула В называется формально выводимой из формул А1,...,А„ и обозначается так: A1, ..., Ап├В, или Г├В, где Г = {A1,...,An}.
Очевидно, что доказательство - частный случай формального вывода из пустого множества посылок.
Пример 3.
Построить вывод формулы С А, С В, С├ A В
|
1. посылка |
|
2. посылка |
|
3. посылка |
|
4. МР(F1,F3) |
|
5. МР(F2,F3) |
|
6. АС3 |
|
7. МР(F4,F6) |
|
8. МР(F5,F7) |
|
9. ОФВ (1-8) – определение формального вывода |
Пример 4.
Построить вывод формулы A В, С В├ А
|
1. посылка |
|
2. посылка |
|
3.
|
|
4. МР(F2,F3) |
|
5.
|
|
6. МР(F1,F5) |
|
7.
|
|
8. МР(F4,F7) |
|
9. МР(F6,F8) |
|
10. ОФВ (1-9) – определение формального вывода |
Пример 5.
Построить вывод формулы A В, В С├ А С
|
1. посылка |
|
2. посылка |
|
3.
|
|
4. АС2 |
|
5. АС12 |
|
6. МР(F1,F5) |
|
7. МР(F4,F6) |
|
8.
|
|
9. МР(F2,F8) |
|
10.
|
|
11. МР(F9,F10) |
|
12. МР(F7,F11) |
|
13. МР(F3,F12) |
|
14.
|
|
15.
|
|
16. МР(F2,F15) |
|
17. МР(F14,F16) |
|
18. АС13 |
|
19. МР(F1,F18) |
|
20.
|
|
21. МР(F19,F20) |
|
22. МР(F17,F21) |
|
23. МР(F13,F22) |
|
24. ОФВ (1-23) – определение формального вывода |
