Доказательство.

Полнота СКИВ относительно семантики Крипке.

Теорема (о полноте).

Если формула тождественно истинна по Крипке, то она доказуема в КИВ, т.е.

╞_Крипке F ├_скив → F

Доказательство.

План доказательства:

1 этап – построение за конечное число шагов дерева редукций для секвенции → F.

2 этап – определение типа дерева («+», «-»).

3 этап – доказательство двух утверждений.

Утверждение 1. Если дерево редукций имеет тип «+», то строится доказательство секвенции → F.

Утверждение 2. Если дерево редукций имеет тип «-», то строится интерпретация Крипке Kр=<W, w₀, R, >, такая что .

Отсюда будет следовать, что если секвенция → F не доказуема в СКИВ, то F опровержима по Крипке, что и требуется доказать.