Полнота СКИВ относительно семантики Крипке.
Теорема (о полноте).
Если формула тождественно истинна по Крипке, то она доказуема в КИВ, т.е.
╞Крипке F ├скив → F
Доказательство.
План доказательства:
1 этап – построение за конечное число шагов дерева редукций для секвенции → F.
2 этап – определение типа дерева («+», «-»).
3 этап – доказательство двух утверждений.
Утверждение 1. Если дерево редукций имеет тип «+», то строится доказательство секвенции → F.
Утверждение 2. Если дерево редукций имеет тип «-», то строится интерпретация Крипке Kр=<W, w0, R, >, такая что .
Отсюда будет следовать, что если секвенция → F не доказуема в СКИВ, то F опровержима по Крипке, что и требуется доказать.