Мы определим 12 правил вывода, и удобно вводить их постепенно.
Предполагая, что это уже сделано, определим понятие вывода. Выводы у нас будут представляться в виде деревьев доказательства.
Определение 17 (Дерево доказательства). Дерево доказательства определим рекурсивно:
7. Деревом доказательства является пустое дерево доказательства, состоящее только из корня – аксиомы.
8. Пусть T1, ..., Tk – деревья доказательства с корнями R1, ..., Rk. Тогда
| T1 ... Tk |
| S |
(где S – некоторая секвенция) – дерево доказательства, если S может быть получена из R1, ..., Rk с помощью одного из правил вывода. Корнем такого дерева является S.
Определение 18 (Доказуемая секвенция). Если существует дерево доказательства с корнем R, то R называют доказуемой секвенцией. Если этот корень имеет вид G |– F, то говорят о выводе формулы F из G.
В соответствие с дедуктивным определением следования говорят, что F следует из G, если существует вывод F из подмножества G.
Правила для конъюнкции и импликации
| G |– F G |– G | G |– F & G | G |– F & G | ||||||||||||
| (У&) | ||||||||||||||
| G |– F | G |– G | |||||||||||||
| (В&) | ||||||||||||||
| G |– F & G | ||||||||||||||
| G И { F } |– G | G |– F G |– FЙ G | |||||||||||||
| (ВЙ) | (УЙ) | |||||||||||||
| G |– F Й G | G |– G | |||||||||||||
В каждом из этих пяти правил вывода, одно или два выражения над горизонтальной чертой представляют ``посылки'', к которым правило может быть применено, и выражение под чертой представляет ``заключение'' которое выводится по этому правилу. Правила В& и ВЙ – ``правила введения'' конъюнкции и импликации; У& и УЙ – ``правила удаления''. Подставляя конкретные формулы вместо метапеременных F и G и конкретные конечные множества формул вместо метапеременной G некоторое правило вывода, мы получаем пример этого правила. Например,
| {q, r} |– p {p Ъ q, r} |– q |
| {q, r, p Ъ q} |– p & q |
Дата добавления: 2015-10-05; просмотров: 802;