<<
>>

Заключение

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

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

Для обеспечения корректности системы наряду с понятием вывода (доказательства) в системе (Определение 2.1.3) вводится понятие завершенного вывода (завершенного доказательства), т.е. такого вывода (доказательства), в неисключенные посылки и заключение которого не входит ни одна абсолютно ограниченная переменная данного вывода (доказательства).[21]

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

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

Отметим, что в системе У.Куайна (а значит, в предложенном им доказательстве теоремы о семантической непротиворечивости) существенным образом используется алфавитный порядок, заданный на множестве используемых в языке переменных.

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

Куайном, не обобщается на систему BMV.

В связи с этим вводится понятие пассивной переменной в BMV-выводе (доказательстве), т.е. такой абсолютно ограниченной переменной в BMV-выводе (доказательстве), которая не ограничивает относительно ни одну абсолютно ограниченную переменную данного BMV-вывода (доказательства).[22]

Показывается, что в произвольном алго-выводе всегда найдется пассивная переменная (Лемма 2.2.4).

Далее предлагается алгоритм поиска вывода в данном исчислении, который является модификацией алгоритма поиска натурального вывода, разработанного ВА. Бочаровым, AΕ. Болотовым и AΕ. Горчаковым.

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

Понятие вывода (доказательства) в системе BMV предполагает, что в выводе (доказательстве) ни одна переменная не ограничивает сама себя. Переменная ограничивает другую переменную согласно формулировкам правил Vb, ∃h.

Экспликация отношения ограничения показывает, что данное отношение, заданное на множестве переменных вывода (доказательства), обладает свойствами иррефлексивности (ни одна переменная не ограничивает сама себя) и транзитивности (если переменная x ограничивает переменную у и переменная у ограничивает z, то переменная x ограничивает переменную z).

Таким образом, отношение ограничения, заданное на множестве переменных вывода (доказательства), является отношением строгого (частичного) порядка.

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

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

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

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

Показывается конечность ветвления для произвольного блока в произвольном дереве поиска вывода (Лемма 4.3.1).

Опираясь на представление алгоритмического натурального вывода в виде древовидной структуры, выделяется некоторая нить данного дерева, множество формул в которой образует множество Хинтикки (модельное множество).

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

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

Поскольку всякий алгоритмический вывод есть вывод в системе BMV, из утверждения о семантической полноте алгоритма следует утверждение о семантической полноте системы BMV (Теорема 4.3.8).

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

a. теорема о семантической полноте системы BMV тривиально следует из теоремы о семантической полноте алгоритма поиска вывода в системе BMV. Однако остается невыясненной возможность прямого, а не косвенного доказательства теоремы о семантической полноте системы BMV (например, установлением факта, что все, что доказуемо в стандартном гильбертовском исчислении, имеет завершенное доказательство в системе BMV).

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

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

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

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

Еще по теме Заключение:

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