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

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

Теорема.

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

├_скив ╞_Крипке .

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

Пусть секвенция доказуема в СКИВ.

Рассмотрим доказательство секвенции :

(1)

Докажем, что каждая из секвенций данного доказательства тождественно истинна по Крипке.

Доказательство проведём по индукции.

Заметим, что секвенция Г→∆ опрвержима по Крипке, если существует интерпретация КрипкеK=<W, w₀, R, >, в которой все формулы из Г истинны, а формула ∆ ложна.

n =1. Секвенция имеет вид А→А.

Предположим, что она опровержима по Крипке.Пусть K=<W, w₀, R, > - интерпретация Крипке, в которой А истинна и А ложна. Чего не может быть.

Пусть теорема верна для всех n<k. Докажем для n=k.

Последняя секвенция Г→∆ выводится по одному из правил вывода.

Рассмотрим 6 возможных случаев.

1) введение &

По индукционному предположению, общезначимы по Крипке. Предположим, что секвенция-заключение опровержима по Крипке. Тогда существует интерпретация Крипке K=<W, w₀, R, >, где

или .

Отсюда следует, что секвенция

опровержима по Крипке. Это противоречит нашему индукционному предположению.

Значит, секвенция Г→ A&B общезначима по Крипке.

2)удаление &

По индукционному предположению, общезначима по Крипке. Пусть секвенция-заключение опровержима по Крипке. Тогда существует интерпретация Крипке K=<W, w₀, R, >, где

, , .

Отсюда следует, что опровержима по Крипке.

Это противоречит нашему индукционному предположению.

Значит, секвенция общезначима по Крипке.

3) введение

а) б)

а). По индукционному предположению общезначима по Крипке. Пусть секвенция- заключение опровержима по Крипке. Тогда существует модель Крипке K=<W, w₀, R, >, где

.

Отсюда следует, что опровержима по Крипке.

Это противоречит нашему индукционному предположению.

Значит, секвенция общезначима по Крипке.

б). Полностью аналогично.

4)удаление

По индукционному предположению секвенции общезначимы по Крипке. Пусть секвенция-заключение опровержима по Крипке. Тогда существует модель Крипке K=<W, w₀, R, >, где ,

или .

Отсюда следует, что опровержима по Крипке.

Это противоречит нашему индукционному предположению.

Значит, секвенция общезначима по Крипке.

5) удаление

По индукционному предположению секвенции общезначимы по Крипке. Пусть секвенция-заключение опровержима по Крипке. Тогда существует модель Крипке K=<W, w₀, R, >, где ,

или

используя свойство рефлексивности отношения R, заключаем, что одна из секвенций опровержима по Крипке.

Это противоречит нашему индукционному предположению.

Значит, секвенция общезначима по Крипке.

6) введение

По индукционному предположению общезначима по Крипке.

Пусть секвенция-заключение опровержима по Крипке. Тогда существует модель Крипке K=<W, w₀, R, >, где .

Следовательно, существует мир w, достижимый из w₀, где А принимает значение1, В принимает значение 0. Какое значение принимают формулы из Г в мире w? Покажем, что все они истинны в w. (Отсюда будет следовать, что секвенция опровержима по Крипке. Это противоречит нашему индукционному предположению. Значит, секвенция будет общезначима по Крипке.)

Для этого докажем лемму о монотонности.

Лемма. Пусть К – произвольная модель Крипке, w – произвольный мир и u – произвольный мир, достижимый из w. Пусть F – произвольная формула. Тогда если

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

Доказываем индукцией по сложности формулы F (m- число логических связок в F).

m=0.

Тогда F – элементарная переменная. Утверждение леммы следует из свойства монотонности разметки интерпретаций Крипке для КИВ.

Пусть лемма справедлива для m<k. Докажем для m=k. Рассмотрим главную связку F.

а) F=A&B

В мире w F=1 A=B=1. Тогда по индукционному предположению в мире u А=В=1. Следовательно, F=1 в мире u.

b) F=A B

В мире w F=1 A=1 или B=1. Тогда по индукционному предположению в мире u А=1 или В=1. Следовательно, F=1 в мире u.

c) F=A B

В мире w F=1. Докажем, что в мире u также F=1.

Доказательство от противного. Пусть F=0 в мире u, т.е. существует мир v, достижимый из u, где А=1, В=0. Но по свойству транзитивности мир v достижим и из w тоже. Т.е. в мире w истинностное значение F должно равняться 0. Противоречие. Значит F=1 в мире u. Лемма доказана полностью.

Доказательство теоремы о непротиворечивости закончено.