Доказательство утверждения 1.

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

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

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

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

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

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

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

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

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

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

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

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

I. Построение дерева редукций.

1. Начальную секвенцию приписываем к кореню дерева:

v • → F

2. Шаг построения дерева редукций («раскрытие» вершины).

Пусть v – «самая верхняя» вершина дерева редукций, и ей приписана секвенция .

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

1) секвенция содержит формулу вида A&B справа. Тогда применяем редукцию 1 рода вида:

• •

u₁ u₂

•

2) секвенция содержит формулу вида A&B слева. Тогда применяем редукцию 1 рода вида:

u •

v •

3) секвенция содержит формулу вида A V B слева. Тогда применяем редукцию 1 рода вида:

• •

u₁ u₂

•

4) секвенция содержит формулу вида A V B справа. Тогда применяем редукцию 1 рода вида:

u •

v •

5) секвенция содержит формулу вида A B слева. Тогда применяем редукцию 1 рода вида:

• •

u₁ u₂

•

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

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

В результате к самым верхним вершинам дерева редукций могут быть приписаны секвенции единственного вида .

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

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

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

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

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

… …. …

и т.д.

Ясно, что алгоритм построения дерева редукций закончит работу за конечное число шагов.

II. Тип дерева редукций.

а) Разметка концевых вершин дерева редукций описана выше.

б) Разметка внутренних вершин дерева редукций.

«–»и«+»приписываются всем внутренним вершинам дерева редукций по правилам:

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

+ + – – + –

+ – – + –

редукции 2 рода:

+ – – –

+ –

III. Построение доказательства или опровержения по Крипке по дереву редукций.

Утверждение 1.

Если корневая вершина дерева редукций помечена «+», то приписанная ей секвенция доказуема в КИВ.

Доказательство утверждения 1.

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

Базис Р =1.

₊С помощью избавляемся от многосукцедентности.

v •

что и требовалось.

Пусть утверждение справедливо для Р<k, докажем для P=k.

Рассмотрим все возможные случаи (6 штук):

1) редукция & - справа.

+ • + •

+• v

По индукционному предположению доказаны секвенции, соответствующие дочерним вершинам.

Построим доказательство секвенции, соответствующей v. Для этого достаточно доказать секвенцию , и затем применить 2 раза правило сечения.

2) редукция &- слева.

+ •

+ • v

По индукционному предположению доказана секвенция, приписанная дочерней вершине. Построим доказательство секвенции, приписанной v. Она доказуема по правилу удаления &.

3) редукция v- справа.

+ •

тривиально

+ • v

4) редукция v – слева.

• •

+ +

+• v

По индукционному предположению доказываются секвенции, приписанные дочерним вершинам. Построим доказательство секвенции, приписанной v. Она доказывается по правилу удаления .

5) редукция – слева.

• •

+ +

+• v

По индукционному предположению доказываются секвенции, приписанные дочерним вершинам. Построим доказательство секвенции, приписанной v: .

Аналогично п.1 докажем сначала секвенцию ,

и применим затем 2 раза правило сечения.

6) редукция – справа (2 рода).

+ v

По индукционному предположению доказывается одна из секвенций, приписанных дочерним вершинам. Построим доказательство секвенции, приписанной v: .

Доказательство состоит в применении правила введения и правил введения V.

Утверждение 1 доказано.

Утверждение 2.

Если корневая вершина дерева редукций помечена «-», то существует интерпретация Крипке, в которой опровергается приписанная к ней секвенция.

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

1. По дереву редукций построим минимальное отрицательное дерево D*.

Берём корневую вершину дерева редукций, она помечена «-», включаем её в поддерево.

Если к ней применялась редукция 1-го рода, то одну из дочерних вершин, помеченную «-», тоже включаем в поддерево. Если к ней применялась редукция 2 рода, то в минимальное дерево включаем все дочерние вершины, помеченные «-».

И т.д. Поступаем аналогично со всеми внутренними вершинами дерева редукций, пока не дойдём до листьев, помеченных «-».

Т.о. построим минимальное, отрицательное дерево D*.

2. По дереву D* построим интерпретацию Крипке Kр=<W, w₀, R, > следующим образом.

1). W. Миры – это участки редукции 1 рода, которые оканчиваются на вершинах, к которым приписаны секвенции вида . Они формируют множество возможных миров W={w₀, w₁,…}.

Т.е. с каждым миром ассоциируется вершина с приписанной секвенцией .

2) w₀ – мир, в который входит корневая секвенция.

3). R. Отношение достижимости. R(u, v)определяется так: R(u, v) – истинно, если в минимальном отрицательном дереве D* существует путь, проходящий из u в v.

Отметим, что если некоторая вершина-лист u помечена значком <-,w>, то мы будем считать что из u имеется путь в w.

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

4) . В каждом мире определим значения элементарных высказываний.

- v

- •u для всех остальных переменных q.

Пропозициональные переменные, один раз попав в антецедент секвенции, исчезнуть не могут, т.к. входят в антецеденты всех «верхних» секвенций. Поэтому свойство монотонности разметки очевидно выполняется: если любая пропозициональная переменная истина в мире u, то она истина во всех мирах, достижимых из него.

Докажем, что формула F принимает 0 в реальном мире w₀.

Доказательство проведём индукцией по сложности Р = <N, M> формулы G, входящей в секвенцию, приписанную вершине v в минимальном отрицательном дереве D*. Здесь N – число логических связок в формуле G, а M–количество вершин, расположенных над v в дереве D*.

Отношение порядка. Пусть P1 = <N1,M1> и P2 = <N2,M2>.

Тогда P1 < P2 т. и т.т. когда N1 < N2 или N1 =N2 & M1<M2.

Так определенное отношение обладает свойством фундированности (следовательно, по нему можно вести индукцию).

Индукционное предположение: «Пусть v -вершина дерева D*, принадлежащая к миру w, и G – формула сложности P, входящая в - секвенцию, приписанную v. Тогда если G – формула из , то она истинна в w, а если G – формула из , то она ложна в w ».