Студопедия

Главная страница Случайная страница

Разделы сайта

АвтомобилиАстрономияБиологияГеографияДом и садДругие языкиДругоеИнформатикаИсторияКультураЛитератураЛогикаМатематикаМедицинаМеталлургияМеханикаОбразованиеОхрана трудаПедагогикаПолитикаПравоПсихологияРелигияРиторикаСоциологияСпортСтроительствоТехнологияТуризмФизикаФилософияФинансыХимияЧерчениеЭкологияЭкономикаЭлектроника






Проблема разрешимости.






Определение понятия закона (общезначимой формулы) и логического следования в классической логике предикатов предполагает существование ответов на следующие вопросы:

а) С помощью какой процедуры можно установить, является (или нет) некоторая формула А законом?

б) При каких условиях из формул А1, А2,..., Аn следует формула В?

В классической логике высказываний сами определения логического закона и логического следования содержат указание на проверочную процедуру, позволяющую установить, является ли данная формула законом и следует ли из формул А1, А2,..., Аn формула В. То есть, чтобы установить, является ли формула А законом, необходимо в соответствии с определением тождественно истинной формулы построить таблицу истинности для А и выяснить, принимает ли формула А значение « и » во всех строках таблицы. А для ответа на вопрос, следует ли В из формул А1, А2,..., Аn, необходимо в соответствии с определением логического следования в классической логике высказываний построить общую таблицу истинности для формул А1 & А2 &... & Аn и В и выяснить, имеется ли в таблице строка, в которой формула А1 & А2 &...&, Аn принимает значение « и », а формула В – значение « л ».

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

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

Классическая логика высказываний является разрешимой теорией. Но этого нельзя сказать о классической логике предикатов. Установление в ней общезначимости формулы и логического следования одних формул из других не является в общем случае эффективным, то есть не существует алгоритма решения указанных проблем.

Действительно, чтобы установить общезначимость формулы А, необходимо рассмотреть все модели и все приписывания значений предметным переменным и убедиться, что во всех случаях формула А принимает значение «истина». А для того, чтобы показать, что А1, А2,..., Аn |= В, следут рассмотреть все модели и все приписывания и убедиться в том, что отсутствует ситуация, при которой конъюнкция формул А1 & А2 &... Аn принимает значение «истина», а формула В – значение «ложь». Ясно, что подобный перебор и обзор всех моделй и всех приписываний в общем случае оказывается бесконечным процессом (в отличие от конечности числа строк в таблице истинности логики высказываний), что исключает существование соответствующих алгоритмов. Решение подобных задач в классической логике предикатов может быть только эвристическим, и в ней разработан ряд процедур, позволяющих стандартным и в достаточной мере оптимальным способом подходить к проблеме разрешения.

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

Суть данного метода заключается в том, что тезисы об общезначимости формулы А и следовании формулы В из А1, А2,..., Аn обосновываютя способом рассуждения от противного.

Например, для обоснования тезиса « |= А» показывают, что предположение о ложности А приводит с необходимотью к противоречию. Для обоснования тезиса «А1, А2,..., Аn |= В» показывают, что преположение об истинности формулы А1 & А2 &... Аn и ложности формулы В приводит к противоречию.

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

- Каждый шаг в аналитической таблице представляет собой применение соответствующего аналитического правила;

- шаги эти состоят из строк, в которых записаны результаты применения соответствующих аналитических правил;

- шаги обозначают римскими цифрами (І, П, Ш и т.д.);

- строки - арабскими цифрами (0, 1, 2, 3 и т.д.);

- нумерация строк аналитической таблицы начинается с нуля (0), чем подчеркивается, что построение аналитической таблицы начинается с формулировки антитезиса;

- вся таблица, начиная с первой строки, разбивается на ветви;

- переход от одного шага к другому осуществляется в аналитической таблице с помощью специальных аналитических правил, в основе которых лежат смыслы пропозициональных связок &, Ú, É, º, Ø и кванторов " и $;

- каждому из этих правил, их посылок и результатов применения приписывается индекс Т («истина») и F («ложь»).

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

Если ветвь таблицы содержит формулу С с обоими индексами Т и F, то такая ветвь называется замкнутой. А если все ветви таблицы замкнуты, то таблица также является замкнутой.

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

 






© 2023 :: MyLektsii.ru :: Мои Лекции
Все материалы представленные на сайте исключительно с целью ознакомления читателями и не преследуют коммерческих целей или нарушение авторских прав.
Копирование текстов разрешено только с указанием индексируемой ссылки на источник.