Конечность алгоритма поиска вывода для натуральных систем негативных и позитивных силлогистик

Кандидат философских наук, кафедра философии естественных факультетов, Московский государственный университет имени .

КОНЕЧНОСТЬ АЛГОРИТМА ПОИСКА ВЫВОДА ДЛЯ НАТУРАЛЬНЫХ СИСТЕМ НЕГАТИВНЫХ И ПОЗИТИВНЫХ СИЛЛОГИСТИК.

Аннотация

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

Ключевые слова: натуральные исчисления, алгоритм поиска вывода, конечность алгоритма, множества Хинтикки, силлогистика.

Keywords: natural deduction calculi, proof searching algorithm, finiteness of algorithm, Hintikka-sets, syllogistics.

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

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

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

Затем докажем утверждение о нижней границе временной сложности алгоритма.

Конечность мы будем понимать стандартно: алгоритм с необходимостью остановится на любом наборе допустимых для него данных. Для теоремы и корректного утверждения о выводимости он предъявит соответствующий вывод, для формулы, не являющейся теоремой или корректным утверждением о выводимости, алгоритм выдаст соответствующее сообщение («Данная формула не является доказуемой!»). Доказательство того, что алгоритм строит выводы только для теорем системы (обосновывает только допустимые в данной системе выводимости) является доказательством метатеоремы о синтаксической непротиворечивости (семантический аспект у нас сознательно не рассматривается, в связи с многообразием семантических интерпретаций для силлогистических систем), о чем говорилось выше.

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

Последовательно проанализируем конечность каждого алгоритмического шага.

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

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

Доказательство.

Докажем данный факт методом возвратной математической индукции по длине вывода.

Индуктивное допущение. Пусть Лемма 1 справедлива для всякого i, на котором применялись правила вывода данной группы, i < n. Покажем, что она справедлива и для n.

Для обоснования индуктивного перехода введем лимитирующую функцию g(A). Пусть начальным значением лимитирующей функции g(A) для данной группы правил вывода будет суммарная пропозициональная сложность всех больших посылок, подпадающих под правила группы АППВ1. Этим значением будет некоторое натуральное число. Укажем, что под лимитирующей функцией мы понимаем натуральнозначную функцию, с необходимостью уменьшающуюся на каждом шаге работы алгоритма, так что в конце некоторого цикла мы обязательно получим натуральное число. Оно будет служить гарантией того, что исследуемый процесс конечен, ведь ни одно натуральное число нельзя уменьшать бесконечно долго, процесс уменьшения с необходимостью остановится, в максимальном случае на единице (см. определение функции оценки пропозициональной сложности φ). Данный метод используется, например, при доказательстве конечности поиска доказательства в некоторых модальных логиках [5, 210 – 225].

Проще говоря, лимитирующая функция g(A) монотонно убывает на каждом шаге работы алгоритма с правилами из группыАППВ1.

В силу ИД и определения лимитирующей функции, g(A) строго уменьшалась на каждом шаге вывода i, на котором применялись правила вывода данной группы, i < n.

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

Приведем следующий пример, иллюстрирующий работу лимитирующей функции g(A).

Пусть мы применили правило удаления дизъюнкции к формулам SaP∨ SaS, SaP, получили в итоге формулу SaS и уменьшили значение лимитирующей функции на двойку (удалили дизъюнкцию и правый дизъюнкт из большей посылки, совместная сложность которых, по нашему определению функции φ, составляет 2).

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

Следовательно, Лемма 1 справедлива для всякого применения каждого правила из группы АППВ1 на любом шаге вывода. Значение g(A) строго уменьшается на каждом шаге вывода, где применялись АППВ1.

Таким образом, процесс применения правил группы АППВ1 строго конечен.

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

Отметим, что в случае с правилами АППВ2, как мы их определили, посылка единственна.

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

Доказательство.

Докажем данный факт методом возвратной математической индукции по длине вывода.

Индуктивное допущение. Пусть Лемма 2 справедлива для всякого i, на котором применялись правила вывода данной группы, i < n.

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

Демонстрация данного факта достаточно проста. По каждому из имеющихся у нас правил, как мы их определили (например, (А∨В)⊢А&B, (A&B)⊢A∨B и др.), каждой подпадающей под него формуле мы можем сопоставить ровно одну формулу, являющуюся заключением соответствующего правила вывода.

Следовательно, максимальное число формул, которые могут получиться по данным правилам вывода, будет равно либо r|A|, где r – число правил группы АППВ2, а |A| – мощность множества А, соответственно, либо (k-1)r|A|, k > 1, где k – число допустимых применений правил из группы АППВ2, увеличивающих количество пропозициональных отрицаний в формуле (напомним, что данное число вводится пользователем или выбирается алгоритмом автоматически; если пользователь вводит число 0 или 1, то доказательство идет с использованием первой альтернативы – r|A|).

Как и при доказательстве Леммы 1, определим лимитирующую функцию h(A) для правил группы АППВ2. Ее начальным значением будет r|A| либо kr|A|. На каждом применении i, i < n h(A) с необходимостью уменьшалась. Она также уменьшится и на n-ном применении любого из правил данной группы ровно на 1.

Таким образом, мы обосновали индуктивный переход.

Лемма 2 справедлива для всякого применения каждого правила из группы АППВ2 на любом шаге вывода. Значение h(A) строго уменьшается на каждом шаге вывода. Т. е., когда будут применены все допустимые правила данной группы, мы в качестве значения h(A) получим некоторое натуральное число, строго меньшее исходного (в максимальном случае – ноль: все формулы из множества А были посылками правил группы АППВ2).

Лемма 3. Множество формул, полученных по синтетическим беспосылочным п. в., конечно.

Докажем данный факт методом возвратной математической индукции по длине вывода.

Индуктивное допущение. Пусть Лемма 3 справедлива для всякого i, на котором применялись правила вывода данной группы, i < n. Покажем, что она справедлива и для n.

Как и при доказательстве предыдущих утверждений, введем лимитирующую функцию f(A∪ В). Под А будем подразумевать множество формул, на котором применяются данные правила вывода. В случае с беспосылочными п. в. оно будет пустым, так как данные правила являются аксиомами (как мы уже говорили выше). Под В будем понимать множество {A1∪A2…∪An}∪A, где {A1∪A2…∪An} = Γ, Γ⊢А.

Максимальным значением лимитирующей функции f(A∪ В) будет количество всех «чистых», т. е. без терминных отрицаний, силлогистических терминов, входящих во все посылки (если таковые имеются) и формулу, которую требуется вывести или доказать. Обозначим данное числовое значение как N. (Заметим, мы таким образом определили наш алгоритм, что данные правила применяются только к «чистым» терминам.) В силу конечности указанных формул, число данных терминов также будет конечным. По определению беспосылочных п. в., количество допустимых применений указанных правил вывода, а также начальное значение f(A∪ В) будут равными N.

По ИД и определению лимитирующей функции, f(A∪ В) строго убывает на каждом шаге вывода i, на котором применялись правила вывода данной группы, i < n. (При каждом применении какого-либо беспосылочного п. в. мы «отрабатываем» еще один термин и тем самым уменьшаем значение лимитирующей функции).

Покажем, что f(A∪ В) убывает и на шаге n. Применив на шаге n беспосылочное п. в., мы отработали еще один термин и уменьшили значение f(A∪ В) на единицу. На шаге n множество формул, полученное по беспосылочным п. в., конечно.

Оно конечно на любом шаге вывода – функция f(A∪ В) строго убывает на любом шаге вывода и в конце применения данных п. в. ее значением будет 0.

Лемма 3 доказана.

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

Доказательство Леммы 4 совершенно аналогично доказательству Леммы 1. Лимитирующую функцию, использующуюся в данном доказательстве, обозначим как h1(A).

Для доказательства Леммы 5 проведем дополнительное построение.

Пусть Δ+ – некоторое множество терминов. С помощью Примера 3 объясним, как оно конструируется.

Пусть нас есть утверждение о выводимости ~~Sa~M, ~Ma~P⊢~~Sa~P. Таким образом, изначально у нас есть термины ~~S, ~P и ~M. Пусть t = 1 (где t – глубина выбранной эвристики или, в случае, если эвристика не выбрана, максимальное значение, на которое алгоритм может увеличить сложность произвольного термина, оно всегда конечно, по определению алгоритма, но об этом чуть ниже).

Тогда в Δ+ войдут термины: ~~~S, ~~M, ~~P, ~~S, ~P, ~M, ~S, S, P, M. Т. е. мы получили данное множество, приписав к исходным терминам по t негаций, а затем, последовательно уменьшая их число на единицу для каждого термина, вплоть до получения 0, пополнили Δ+ новыми элементами.

Множество Δ+ всегда с необходимостью будет конечным (в силу определения понятия формулы в исследуемых системах, конечности t в каждом случае и, как следствие, конечности числа негаций, применяемых к каждому исследуемому термину).

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

Докажем данный факт методом возвратной математической индукции по длине вывода.

Индуктивное допущение. Пусть Лемма 5 справедлива для всякого i, на котором применялись правила вывода данной группы, i < n.

Покажем, что она справедлива и для n.

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

Отметим, что доказательство Леммы 5 не может быть проведено так же просто, как и доказательство Леммы 2, в силу того, что, во-первых, данные правила не обеспечивают взаимно-однозначного соответствия посылок и заключения, а во-вторых, после пополнения СВ новыми формулами применение данной группы правил продолжается, а не останавливается, как в случае с правилами группы АППВ2

Итак, доказательство Леммы 5.

Так как число аргументных мест в заключении каждого правила группы АСПВ2 с необходимостью, по определению, конечно (число аргументных мест соответствует числу силлогистических метатерминов в схемах заключений) и число всех терминов, принадлежащих множеству Δ+, также конечно, то для каждого правила максимальное число всех возможных вариантов формул, получаемых по нему, будет равно , где p – число аргументных мест в правиле i, а r = | Δ+|. Заметим, что в наших системах p = 2. Отсюда следует, что k будет с необходимостью конечным. Так как число всех правил группы АСПВ2 конечно (пусть для определенности оно равно j), то исходным значением лимитирующей функции (обозначим ее как g2(A)) будет . В нашем случае можно вычислить значение l проще: .

Лимитирующая функция с необходимостью уменьшалась на каждом шаге i, i < n.

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

В итоге мы получим некоторое натуральное число, строго меньше исходного.

Лемма 5 справедлива для всякого применения каждого правила из группы АСПВ2 на любом шаге вывода.

Лемма 6. Если на некотором конечном множестве формул A применяются аналитические силлогистические правила вывода, увеличивающие сложность большей посылки только на некоторую константу ɵi каждое (максимальное значение данной константы ɵi мы, в случае если эвристика не выбрана, приписываем 2), то в результате мы получим только конечное множество формул. Данную группу правил мы сокращенно назвали АСПВ3.

Докажем данный факт методом возвратной математической индукции по длине вывода.

Индуктивное допущение. Пусть Лемма 6 справедлива для всякого i, на котором применялись правила вывода данной группы, i < n. Покажем, что она справедлива и для n.

Доказательство Леммы 6 полностью совпадает с доказательством Леммы 5. Лимитирующую функцию для Леммы 6 обозначим как h2(A).

Таким образом, мы обосновываем индуктивный переход и делаем вывод, что Лемма 6 справедлива для всякого применения каждого правила из группы АСПВ3 на любом шаге вывода.

Лемма 7. Если на некотором конечном множестве формул A применяются аналитические силлогистические правила вывода, удаляющие общий (средний) термин из посылок (назовем сокращенно эти правила АСПВ4), то в результате мы получим только конечное множество формул. (Нетрудно заметить, что данные правила являются силлогистическими модусами (в нашем случае – Celarent и Barbara.)

Докажем данный факт методом возвратной математической индукции по длине вывода.

Индуктивное допущение. Пусть Лемма 7 справедлива для всякого i, где применяются АСПВ4, i < n. Покажем, что она справедлива и для n.

Доказательство Леммы 7 полностью совпадает с доказательством Леммы 5.

Лимитирующую функцию для Леммы 7 обозначим как f2(A). (C помощью f2 (A) на каждом шаге вывода мы «отрабатываем» еще один правильный силлогизм).

Таким образом, мы обосновываем индуктивный переход и делаем вывод, что Лемма 7 справедлива для всякого применения каждого правила из группы АСПВ4 на любом шаге вывода.

Лемма 8. Количество допущений в любом выводе, конструируемом нашим алгоритмом, конечно.

Докажем данный факт методом возвратной математической индукции по длине вывода.

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

В качестве начального значения лимитирующей функции h3(В) (под В будем понимать множество {A1∪A2…∪An}∪A, где {A1∪A2…∪An} = Γ, Γ⊢А [Примечание 2]) возьмем мощность множества всех подформул и их отрицаний всех формул множества В. По определению нашего алгоритма ни одно допущение не может выходить за данные рамки: не являться подформулой указанных формул или ее отрицанием.

Таким образом, начальное значение h3(В) будет натуральным числом. На каждом шаге i, где добавлялись новые допущения, i < n, по ИД, значение лимитирующей функции будет строго уменьшаться (добавили еще одно допущение). На шаге n мы также добавили в вывод еще одно допущение и уменьшили значение h3(В) ровно на единицу.

Индуктивный переход обоснован.

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

Лемма 9. Если на некотором конечном множестве формул A применяются синтетические пропозициональные правила вывода (назовем их сокращенно СППВ), то в результате мы получим только конечное множество формул.

Докажем данный факт методом возвратной математической индукции по длине вывода.

Индуктивное допущение. Пусть Лемма 9 справедлива для всякого i, где применяются СППВ, i < n (лимитирующая функция строго убывает на каждом шаге i).

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

Доказательство во многом схоже с доказательством Леммы 8.

В качестве начального значения лимитирующей функции g3(A∪B) (под A, как всегда, будем понимать множество [Примечание 3] формул вывода – в нашем случае множество формул СВ; В есть множество вида {A1∪A2…∪An}∪A, где {A1∪A2…∪An} = Γ, Γ⊢А) возьмем мощность множества всех подформул и их двойных отрицаний формулиз множества В. По определению нашего алгоритма, ни один результат применения СППВ не может выходить за данные рамки: не являться подформулой указанных формул или ее двойным отрицанием. Таким образом, начальное значение g3(A∪B) будет натуральным числом. На каждом шаге i, на котором применялись СППВ, i < n, по ИД, значение лимитирующей функции будет строго уменьшаться (добавили еще один результат применения СППВ). На шаге n мы также добавили в вывод еще один такой результат (здесь мы последовательно рассматриваем все СППВ) и в каждом случае уменьшили значение g3(A∪В) ровно на единицу.

Индуктивный переход обоснован.

Делаем вывод, что Лемма 9 справедлива для всякого применения каждого правила из группы СППВ на любом шаге вывода.

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

Докажем данный факт методом возвратной математической индукции по длине вывода.

Как всегда, определим лимитирующую функцию G(CB∪В) = g(CB)+h(CB)+f(CB∪В)+h1CB)+g2(CB)+f2(CB)+h2(CB)+g3(CB∪В)+h3(B). Множество В определяется стандартно. В силу Лемм 1 – 9 и свойств определенных нами функций, ее значением будет некоторое натуральное число.

Индуктивное допущение. Пусть Теорема 1 справедлива для всякого i, i < n (лимитирующая функция G(CB∪В) строго убывает на каждом шаге i, где применялись правила вывода или добавлялись новые допущения). Покажем, что она справедлива и для n (на шаге n лимитирующая функция с необходимостью уменьшит свое значение).

Какое бы правило мы ни применили на шаге n и какое бы допущение ни добавили бы в СВ на данном шаге (снова применяем разбор случаев), из доказательства Лемм 1 – 9 следует, что G(CB∪В) с необходимостью уменьшит свое значение на некоторую натуральную величину.

Индуктивный переход обоснован.

На любом шаге вывода множество СВ∪В -- и множество СВ, соответственно, так как множество В фиксировано для каждого случая – будет конечным. (В итоге мы получим некоторое натуральное число как значение G(CB∪В), в максимальном случае – 0).

Теорема 1 справедлива для всех случаев обращения нашего алгоритма к СВ и для любых манипуляций нашего алгоритма с СВ: применения правил вывода той или иной группы, добавления допущений.

Теорема 1 наглядно демонстрирует тот факт, что множество всех шагов, совершаемых нашим алгоритмом применительно к СВ (с допущением конечности стека целей – сокращенно СЦ – и конечности ветвления СЦ), всегда будет конечным, так как функция G(CB∪В) с необходимостью убывает на каждом шаге вывода, и поэтому с необходимостью наступит момент, когда алгоритм больше не сможет выполнить никакое действие по отношению к СВ.

Теоремы, доказывающие конечность СЦ (по сути, работа с формулами СЦ уже по определению конечна, так как в самом описании используемых при данной работе процедур оговаривается, что сложность каждой последующей формулы должна быть строго меньше предыдущей; таким образом, конечность является «непосредственным» свойством СЦ) и конечность ветвления СЦ, гарантирующая конечность общего числа шагов алгоритма, уже доказаны в [4, 112 – 120].

Построенный мною алгоритм и алгоритм для классической логики высказываний, приведенный в [4], в данной сфере работают совершенно идентично, так как в их основу положен алгоритм для КЛВ, построенный , , [1].

Так как силлогистические правила, применяемые в моем алгоритме, касаются только работы с формулами СВ, а работа с СЦ и добавление новых допущений после введения цели-противоречия (собственно ветвление СЦ) никак не задействуют особенности силлогистических систем и идентичны работе алгоритма Болотова, Бочарова, Горчакова, пусть и сформулированы другими словами (без явного постулирования меток и т. п.), то теоремы о конечности СЦ и конечности ветвления СЦ будем считать доказанными.

Итак, конечность алгоритма доказана.

Примечания:

1.  Пропозициональная сложность измеряется количеством бинарных связок в формуле; количество унарных связок (в нашем случае – пропозиционального отрицания) не учитывается.

2.  Т. е. мы каждому утверждению о выводимости можем сопоставить только конечное множество формул, являющихся допущениями, сформированными по данному утверждению.

3.  Здесь корректнее было бы употребить термин «список», т. е. некоторым образом (в нашем случае – по времени добавления) упорядоченная последовательность формул. Натуральный субординатный вывод – это, по сути, многоуровневый список).

Список литературы:

1.  , , Горчаков поиска вывода в классической пропозициональной логике// Труды научно-исследовательского семинара логического центра института философии РАН. Москва, ИФРАН, 1996 год.

2.  Красненкова поиска вывода для систем негативной силлогистики. Диссертация на соискание ученой степени кандидата философских наук. Специальность 09.00.07 – Логика. М., 2009. На правах рукописи.

3.  О проблеме доказательства непротиворечивости и полноты алгоритма поиска вывода для натуральных систем негативной силлогистики.«Седьмые смирновские чтения по логике. Материалы международной научной конференции 22 – 24 июня 2011 г.». Москва: изд-во «Современные тетради», 2011 г.

4.  Логика и компьютер. Выпуск 5. Пусть докажет компьютер. Москва, «Наука», 2004.

5.  Heuerding A., Seyfried M., Zimmermann H. Efficient loop-check for backward proof search in some non-classical propositional logics // Proc. TABLEAUX'96, 1996. P. 210 – 225.