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

Непротиворечивость HS4 относительно семантики Крипке

Теорема. ├_HS4 F ╞_Крипке F

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

Индукцией по длине доказательства.

Базис. Рассмотрим все аксиомы HS4.

А0: все тавтологии КлИВ являются тождественно истинными по Крипке.

Это очевидно, т.к. истинностное значения всех формул КлИВ в каждом мире определяются так же, как и в КлИВ.

А1: □А А

Предположим, что она опровержима по Крипке, т.е.

v • найдется мир v, в котором □А А=0, т.е. □А=1 и А=0,

но R(v, v) и A должно принимать значение 1 в v -

противоречие

Следовательно, □А А истинна по Крипке.

А2: □ (А В) (□А □В)

Предположим, что она опровержима по Крипке, т.е. имеется мир v и достижимый из него мир u, такие что

u • B=0, но А B=1 и А=1 В=1 - противоречие

v • □ ( А B)=1, □А=1 и □B=0

Следовательно, □ (А В) (□А □В) истинна по Крипке.

А3: □А □□А

Предположим, что она опровержима по Крипке, т.е. имеются миры w,u,v – такие что

v • A=0 А=1

По свойству транзитивности R(w, v);

u • □А =0 в w □А=1, то в v должно А=1, а в v имеем А=0 -

противоречие

w• □А=1, □□А=0

Следовательно, □А □□А истинна по Крипке.

Индукционный переход.

Правила вывода:

1)

По индукционному предположению в каждом мире А=1 и А В=1.

Следовательно, В=1 в каждом мире.

2) А

□А

Предположим, что формула □А опровержима по Крипке, т.е. □А=0 в мире v.

u •A=0

v•□А=0

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

Теорема доказана полностью.