Редукции 1 рода применяем до тех пор, пока можно

Полнота GS4 относительно семантики Крипке

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

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

Доказательство аналогично доказательству теоремы о полноте для КИВ.

Изменения при построении дерева редукции:

Редукции 1 рода:

1) - справа

u •

v •

2) - слева

• •

u₁ u₂

v

•

3) - справа

u •

v •

4) - слева

u •

v •

5) □ – слева

Г*, Г₁, (□А)*, А → ∆

u •

v •

Г*, Г₁, □А → ∆

Заметим, что к формулам, помеченным ^*, редукция 1 рода не применяется.

Редукции 1 рода применяем до тех пор, пока можно.

В результате к самым верхним вершинам дерева редукций могут быть приписаны секвенции единственного вида: Г*, р₁,…, р_n → q₁,…, q_n, □A₁,…, □A_k

Пусть v – одна из таких вершин.

а) если секвенция, приписанная v, содержит одинаковую переменную и слева и справа, то v больше не раскрывается и помечается значком «+».

б) иначе если в секвенции, приписанной v, k=0, то v больше не раскрывается и помечается значком «-».

в) иначе если секвенция, приписанная v, уже приписана некоторой вершине w, располагающейся в дереве редукций ниже v, то v больше не раскрывается и помечается значком <-, w>.

г) иначе к вершине v применяется редукция 2 рода следующего вида:

Г→А₁... Г→ А_i … Г→А_k

Г*, р₁,…, р_n→q₁,…, q_n, □A₁, …, □A_k

Заметим, что все формулы из Г* в качестве главной связки имеют □.

Все остальное аналогично.