<<
>>

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

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

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

Например, Дж. Поллок использует исчисление предикатов второго порядка [Pollock].

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

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

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

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

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

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

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

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

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

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

• Правило Vbприменяется к формуле 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.

Доказано.

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

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

Определение 4.1.3.Блокомαi, i ∈N, является непустая последовательность формул вывода {A1, A2,..., An} и (возможно, пустая) последовательность целей {∂1, ⅞,..∙, ∂k}:14

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

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

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

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

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

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

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

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

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

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

неприменимо, алгоритм осуществляет поиск формул из ПВ, к которым можно применить вц-правила. Т.е. алгоритм ищет сложные формулы из ПВ, к которым не применялись правила исключения. В данном случае имеется одна такая формула (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.

<< | >>
Источник: ШАНГИН ВАСИЛИЙ ОЛЕГОВИЧ. АВТОМАТИЧЕСКИЙ ПОИСК НАТУРАЛЬНОГО ВЫВОДА В КЛАССИЧЕСКОЙ ЛОГИКЕ ПРЕДИКАТОВ. Диссертация на соискание ученой степени кандидата философских наук. Москва - 2004. 2004

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

  1. ЗАКЛЮЧЕНИЕ
  2. Учение о красоте и триада благо-мудрость-красота.
  3. Терминологические и методологические проблемы
  4. Психоанализ
  5. ШАНГИН ВАСИЛИЙ ОЛЕГОВИЧ. АВТОМАТИЧЕСКИЙ ПОИСК НАТУРАЛЬНОГО ВЫВОДА В КЛАССИЧЕСКОЙ ЛОГИКЕ ПРЕДИКАТОВ. Диссертация на соискание ученой степени кандидата философских наук. Москва - 2004, 2004
  6. 2.2. Исторические свидетельства о трактате «О природе космоса и души»
  7. 3.4.1. Учение о душе и видах душ.
  8. Гармоника в контексте мыслительного феномена прото­упорядочивания
  9. Научные исследования в перспективе вопроса о сущности воли
  10. Ответы к экзамену по логике,
  11. Sitz im Lebenпифагорейских псевдоэпиграфов