<<
>>

3.1.Изменение формулировки системы BMV

В целях эффективности автоматического поиска вывода добавим к BMV- правилам следующие правила исключения логических связок:

Несложно показать, что данные правила производны: их добавление не влияет на множество теорем исчисления.

Теперь объясним необходимость введения именно таких правил.

Отсутствие этих правил приводит к следующим затруднениям [Болотов и др.].

Пусть (ситуация «а») в алгоритме необходимо доказать формулу А v В, но в выводе нет ни А, ни В.

Тогда (ситуация «б») в качестве последней посылки в последовательность вывода помещается —(А v В) и теперь необходимо получить не формулу А v В, а противоречие в выводе. Допустим, что противоречие не получено (и вывод, следовательно, не построен).

Значит, (ситуация «в») алгоритм использует формулу —(А v В) в качестве источника для взятия целей и теперь необходимо получить А v В снова, т.е. алгоритм возвращается к ситуации «а».

Значит, в работе алгоритма имеет место цикл.

Во избежании цикла авторы предлагают переходить от ситуации «б» к ситуации «в» только, если этим двум ситуациям не предшествовала ситуация «а», т. е. формула —(А v В) не была помещена в качестве последней посылки тогда, когда необходимо было получить А v В.

В противном случае от ситуации «б» алгоритм переходит не к ситуации «в», а к ситуации «в1»: происходит «выход из алгоритма» и обосновывается выводимость формул — А, —В из —(А v В).

Т.к. алгоритм всегда построит вывод формул —А, —В из формулы —(А v В), отмечается, что формула —(А v В) не может быть источником для взятия целей и не возникнет необходимости получать А v В. Т.е. от ситуации «в1» алгоритм не перейдет к ситуации «а».

Таким образом, цикл в работе алгоритма ликвидирован. Нетрудно видеть, что выводимость формул —Λ, —В из —(Λ V В) в ситуации «ві» есть ничто иное, как вводимое сейчас в системы правило —vh.

Что касается правила —Зи, то объяснение необходимости данного правила сходно с объяснением необходимости правила —vm,учитывая аналогию между V и 3.

Еще раз обращаем внимание, что может быть построен алгоритм поиска вывода в BMV без правил ■'■/„, —Зи [Болотов и др.], [Болотов и др.1].

Однако введение этих правил облегчает поиск вывода. Другими словами, вместо того чтобы переходить от ситуации «а» к ситуациям «в» или «в1», если в выводе имеется формула —(Λ V В) или —3αΛ(α), мы предлагаем применять к этим формулам, соответственно, правило —vи или —3и.

Теперь рассмотрим правила Vbи 3и, т.е. те правила системы, которые приводят к появлению в выводе абсолютных переменных.

В формулировке Vbи 3и переменные γ1,..., γnсуть все свободные переменные, соответственно, из VαA(α, γ1,..., γn) и 3αA(α, γ1,..., γn). Отметим, что β не может принадлежать {γ1,..., γn}, т.к., согласно определению BMV-вывода, ни одна переменная не может ограничивать сама себя (Определение 2.1.3).

Покажем, что система BMV неявно использует сколемовские функции в правилах Vb,3и. (Явно сколемовские термы используются при формулировке правила 3и в системе натурального вывода, предложенной Е.К. Войшвилло [Войшвилло], т.е. в той системе, модификацией которой является BMV.)

Приведем вариант записи данных правил с использованием сколемовских функций σ, σ1и т.д. [Мендельсон, с. 111]: Vb:из Λ(α∕σ(γ1,..., γn)) выводима VαΛ; 3и: из 3αΛ выводима Λ(α∕σ(γ1,..., γn)), где σ - новая сколемовская функция, γ1,..., γn- все свободные переменные в 3αΛ и в VαΛ.

При этом нульместные сколемовские функции обозначаются константами a, b и т.д.

Например, результатом сколемизации формулы 3vVw3xVy3z(Q(v, w, у, z) ⊃P(f(x, У), g(z))) будет Q(a, w, у, σ1(w, y)) ⊃P(f(σ(w), у), g(σ1(w, у))).

Теперь сравним запись с неявным использованием сколемовских термов и

запись с использованием таких термов.

В обоих вариантах множество {γ1,..., γn} совпадает. Подстановка везде правильна.

Различия заключаются в следующем: (1) вариант BMV не использует

функторы для образования сколемовского терма; (2) в случае п = 0 сколемовский вариант использует константы, а вариант BMV - абсолютные переменные. Более того, сколемовский вариант требует, чтобы константы и функторы были новыми, а вариант BMV не требует, чтобы абсолютные переменные были новыми.

Данные различия исчезают, если отметить содержательную трактовку (полностью верную для правила Зи и частично верную для правила Vb)абсолютной переменной как константы, обозначающей некий объект, для которого выполняется А в записи A(α∕β, γ1,..., γn) или A(α∕β): «Переменная β в этом случае ... абсолютно ограничена в том смысле, что должна теперь рассматриваться как имя какого-то вполне определенного объекта, удовлетворяющего условию А» [Бочаров и Маркин, с. 133].

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

Что же касается первого различия в записях A(α∕β, γ1,., γn) и A(α∕σ(γι,..., γn)), то содержательно они обозначают одно и тоже: выбор значения для объекта, обозначенного в одном случае как «β - абс., γ1,..., γn- отн.», а в другом - как «σ(γι,..., γn)>>, ограничивает значения для остальных свободных переменных γι,..., γn.

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

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

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

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

Другой важной проблемой при поиске вывода является отслеживание переменных, которые ограничивают сами себя (непосредственно или по транзитивности).

Проиллюстрируем необходимость запрета на самоограничение переменной примерами из [Бочаров и Маркин, с. 135]: именно данный запрет, а не требование правильной подстановки не позволяет вывести в системе из A(y, y) формулу VxA(x, y) и из 3xB(x, y) формулу B(y, y). Отмечается, что «при таком переходе переменная y ограничивает сама себя».

Далее авторы пишут: «Надо только учитывать, что ситуация, когда переменная ограничивает сама себя, может возникнуть не только прямым образом, как это было в приведенных примерах, но и косвенно. Здесь имеется в виду то обстоятельство, что отношение «x ограничивает y» является транзитивным, то есть для него верно соотношение: «если α ограничивает β, а β ограничивает γ, то α ограничивает γ». В силу этого в системе не проходит доказательство формулы Vx3yP(x, y) ⊃ 3yVxP(x, y).

Пусть запись β

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

Еще по теме 3.1.Изменение формулировки системы BMV:

  1. Формулировка мыслительного феномена не-места и описание раннепифагорейского дуализма
  2. Предварительная формулировка мыслительного феномена прото-упорядочивания одинакового
  3. Зиновьев А.А.. Восхождение от абстрактного к конк­ретному (на материале «Капитала» К.Маркса). — M.,2002. —321 с., 2002
  4. Проблема интерпретации учения ранних пифагорейцев
  5. Потомство единого: к феномену повторения единиц
  6. Акусмы как мыслительный феномен
  7. Анализ космологических фрагментов Филолая
  8. Эстетизация (трактовки) воли
  9. Психология
  10. Цели, основные понятия и композиция исследования
  11. Введение
  12. 3.3. Онтологические предпосылки самопознания.
  13. Физиология
  14. Пребывание — исхождение — возвращение (μονή ~~ πρόοδος* — Επιστροφή).
  15. Воля господина в трактовке Гегеля
  16. Виды возвращения.
  17. ЗАКЛЮЧЕНИЕ
  18. Учение о красоте и триада благо-мудрость-красота.