2018-01-21
436
Существует другое определение следования, которое выглядит совершенно отличающимся от данного выше, но в действительности эквивалентное ему. В соответствие с этим определением, G влечёт F, если F может быть выведено из G с использованием определенного набора ``правил вывода''. Первое определение, основанное на интерпретации, – ``семантическое'', второе, основанное на понятии вывода – ``синтаксическое'' или ``дедуктивное''.
О корректности, полноте и разрешимости
Выводы в логике высказываний – наш основной объект изучения до конца данной части.
Вывод строятся из конструкций, которые называются `` секвенциями ''.
Определение 15 (Секвенция). Секвенция – это выражение вида G |– F (`` F при посылках G'') или G |– ^ (``посылки G противоречивы''), где F – формула и G – конечное множество формул. *
Мы определим, какие секвенции рассматриваются ``начальными'', и опишем несколько ``правил вывода'' для порождения новых секвенций из секвенций, порождённых ранее. Начальные секвенции называются аксиомами.
|
|
|
Определение 16 (Аксиомы). Аксиомы в исчислении высказываний имеют вид
{ F } |– F.
Мы определим 12 правил вывода, и удобно вводить их постепенно.
Предполагая, что это уже сделано, определим понятие вывода. Выводы у нас будут представляться в виде деревьев доказательства.
Определение 17 (Дерево доказательства). Дерево доказательства определим рекурсивно:
1. Деревом доказательства является пустое дерево доказательства, состоящее только из корня – аксиомы.
2. Пусть T 1 ,..., Tk – деревья доказательства с корнями R 1 ,..., Rk. Тогда
| T 1 ... Tk |
| S |
3. (где S – некоторая секвенция) – дерево доказательства, если S может быть получена из R 1 ,..., Rk с помощью одного из правил вывода. Корнем такого дерева является S.
Определение 18 (Доказуемая секвенция). Если существует дерево доказательства с корнем R, то R называют доказуемой секвенцией. Если этот корень имеет вид G |– F, то говорят о выводе формулы F из G.
В соответствие с дедуктивным определением следования говорят, что F следует из G, если существует вывод F из подмножества G.
