4.1.Семантическая непротиворечивость алгоритма

В предыдущей главе детально описан алгоритм поиска натурального вывода в системе BMV. Возникает вопрос о семантической непротиворечивости алгоритма, т.е. не возникнет ли ситуация, что алгоритм докажет формулу, которая не является общезначимой?

Есть несколько способов доказательства теоремы о семантической непротиворечивости алгоритма.

Другой способ состоит в доказательстве, что все выводы, которые строит алгоритм, суть выводы в системе BMV. Учитывая, что система BMV семантически непротиворечива, получаем, что алгоритм также семантически непротиворечив.

Для доказательства такого утверждения необходимо ввести ряд новых понятий, центральным из которых является понятие алгоритмического BMV-вывода.

АлгоритмическимBMV-выводом называется пара , где

(А) непустая последовательность формул вывода (ПВ), для которой верно:

(i) Каждая формула в ПВ является или начальной посылкой, или посылкой, полученной по ц-правилам, или формулой, полученной из предыдущих по одному из BMV-правил, причем, правила введения применяются следующим образом:

• Правило &_в применяется к формулам D и В, если в ПВ есть D, формула В есть текущая достигнутая цель и предыдущей целью по отношению к D и В является формула D &В;^[13]

• Правило v_bприменяется к формуле D или к формуле В, если D или В является текущей достигнутой целью и предыдущей целью по отношению к D или В является формула D V В;

• Правило ⊃_bприменяется к формуле В, если В является текущей достигнутой целью, формула С является последней неисключенной посылкой и предыдущей целью по отношению к В является формула С ⊃В;

• Правило —_в применяется к формулам B, —B, если цель противоречие является текущей достигнутой целью, формула —С является последней неисключенной посылкой и предыдущей целью по отношению к цели противоречие является С;

• Правило З_в применяется к формуле D(β), если D(β), где β - новая неабсолютная переменная, является текущей достигнутой целью и предыдущей целью по отношению к D(β) является формула ∃αD(α);

• Правило V_bприменяется к формуле D(β), где β - новая абсолютно ограниченная переменная, если D(β) является текущей достигнутой целью и предыдущей целью по отношению к D(β) является формула VαD(α).

(ii) Если в ПВ применялись правила ⊃_bи — _в, то все формулы, начиная с последней посылки и вплоть до результата применения данного правила, исключаются из ПВ;

(iii) Ни одна переменная не ограничивается более одного раза;

(iv) Ни одна переменная в результате унификации не ограничивает сама себя;

и (B) непустая последовательность формул целей (ПЦ), в которой каждая цель получена или по вц-правилам или по одному из ц-правил из предыдущих целей.

В дальнейшем мы будем называть алгоритмический BMV-вывод алго- выводом.

Алго-выводом формулы А из (возможно, пустого) множества посылок Г называется конечный алго-вывод, в котором

• Последовательность формул вывода есть BMV-вывод формулы А из Г;

• Формула А является главной целью и А достигнута.

Согласно вышеприведенному определению, последовательность формул вывода в алго-выводе А из Г есть BMV-вывод формулы А из Г. Возникает вопрос, является ли этот BMV-вывод завершенным или нет? Положительный ответ на этот вопрос дает следующая

Лемма 4.1.1.В алго-выводе формулы А из (возможно, пустого) множества посылок Г последовательность формул вывода есть завершенныйBMV-вывод А из Г.

Доказательство. Напомним, что BMV-вывод является завершенным, если ни одна переменная, абсолютно ограниченная в этом выводе, не входит свободно ни в множество Г, ни в формулу А.

Согласно описанию алгоритма (пункт 1), все свободные переменные из Г, A помечаются как абсолютно ограниченные.

Поскольку ни одна переменная в алго-выводе A из Г не ограничивается абсолютно более одного раза, ни одна свободная переменная из Г, A не ограничиваются абсолютно в данном алго-выводе, а значит, ни одна переменная, абсолютно ограниченная в этом выводе, не входит свободно ни в Г, ни в A.

Доказано.

В главе 2 нашей работы показана семантическая непротиворечивость исчисления BMV. Значит, семантическая непротиворечивость алгоритма устанавливается следующей

Теоремой 4.1.2.В алго-выводе формулы A из (возможно, пустого) множества Г формула A семантически следует из Г.

Доказательство: из леммы 4.1.1 и теоремы 2.2.4.

Доказано.

В процессе построения алго-вывода зафиксируем каждое применение вц- правил. Интуитивно представим процесс построения алго-вывода как ряд применений вц-правил. Такие последовательности формул и целей в алго-выводе, полученные в результате применения одного вц-правила вплоть до другого применения вц-правила, будем называть блоками.

В общем случае блок может состоять только из последовательности формул вывода (последовательность целей пуста, если блок получен по вц-правилу V_b4).Т.к. понятие блока фундаментально для нашего исследования, дадим строгое его определение.

Определение 4.1.3.Блокомα_i, i ∈N, является непустая последовательность формул вывода {A₁, A₂,..., A_n} и (возможно, пустая) последовательность целей {∂₁, ⅞,..∙, ∂k}:¹⁴

(i) Если ∂есть главная цель алго-вывода, то в этом случае i = 1; Если ∂₁получена по одному из вц-правил, то в этом случае i > 1;

(ii) Каждая цель блока, кроме ∂₁,получена по ц-правилам;

(iii) Последней целью блока является либо противоречие, либо формула из ПЦ, которая унифицируется с некоторой формулой из ПВ.

(iv) Каждая формула из последовательности вывода в α_iлибо является начальной

посылкой, либо получена по ц-правилу из цели, содержащейся в α_i(в этом случае формула является посылкой), либо есть результат применения BMV-правила.

Введенное понятие блока в совокупности с вц-правилами определяет в дальнейшем понятие дерева поиска вывода в нашем исчислении.

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

В качестве примера приведем алго-вывод ((p ⊃q) ⊃p) ⊃p (вертикальная черта обозначает границу между блоком №1 и блоком №2).

последовательность целей (ПЦ). При этом последовательность вывода (ПВ) пуста. Применяя к главной цели ц-правило о_ц, получаем подцель p и добавляем в ПВ формулу (p ⊃q) ⊃p в качестве последней посылки. Поскольку ни одно правило исключения в ПВ неприменимо, продолжаем работать с текущей целью p. Применяем к ней правило —_ц, получаем новую подцель ⊥(противоречие) и добавляем в ПВ формулу —p в качестве последней посылки. Поскольку ни одно правило исключения в ПВ

¹⁴Напомним, что целью может быть цель противоречие, которая не является формулой.

неприменимо, алгоритм осуществляет поиск формул из ПВ, к которым можно применить вц-правила. Т.е. алгоритм ищет сложные формулы из ПВ, к которым не применялись правила исключения. В данном случае имеется одна такая формула (p ⊃q) ⊃p. Таким образом, мы применяем к ней вц-правило ⊃_b4и начинаем строить новый блок №2. При этом формулы (p ⊃q) ⊃p и —p из ПВ, а также цели ((p ⊃q) ⊃p) ⊃p, p и ⊥из ПЦ образуют блок №1.

Итак, по вц-правилу ⊃_b4,примененному к формуле (p ⊃q) ⊃p, мы получаем первую цель блока №2 - формулу (p ⊃q). Применяя ц-правило :_ц к ней, получаем подцель q и добавляем в ПВ формулу p в качестве последней посылки. Т. к. текущая цель - формула q - недостижима, применяем к ней ц-правило — _ц, получаем подцель ⊥и добавляем в ПВ формулу —q в качестве последней посылки. Далее действуем согласно правилам системы BMV и целям алгоритма. При этом формулы 3-11, а также цели p ⊃q, q и ⊥, находящиеся ниже вертикальной черты, образуют блок №2.