Условия выразимости и полноты пропозициональных исчислений

Боков, Григорий Владимирович

Условия выразимости и полноты пропозициональных исчислений тема автореферата и диссертации по математике, 01.01.09 ВАК РФ

Боков, Григорий Владимирович АВТОР

кандидата физико-математических наук УЧЕНАЯ СТЕПЕНЬ

Москва МЕСТО ЗАЩИТЫ

2013 ГОД ЗАЩИТЫ

01.01.09 КОД ВАК РФ

Диссертация по математике на тему «Условия выразимости и полноты пропозициональных исчислений»

Автореферат диссертации на тему "Условия выразимости и полноты пропозициональных исчислений"

ФГБОУ ВПО

МОСКОВСКИЙ ГОСУДАРСТВЕННЫЙ УНИВЕРСИТЕТ ИМЕНИ М. В. ЛОМОНОСОВА

На правах рукописи

Боков Григорий Владимирович УСЛОВИЯ ВЫРАЗИМОСТИ И ПОЛНОТЫ ПРОПОЗИЦИОНАЛЬНЫХ ИСЧИСЛЕНИЙ

01.01.09 — дискретная математика и математическая кибернетика

АВТОРЕФЕРАТ диссертации на соискание учёной степени кандидата физико-математических наук

МОСКВА - 2013

31 0КЇ" 2013

005536780

Работа выполнена на кафедре Математической теории интеллектуальных систем Механико-математического факультета ФГБОУ ВПО "Московский государственный университет имени М. В. Ломоносова".

Научный руководитель: доктор физико-математических наук,

профессор Кудрявцев Валерий Борисович

Официальные оппоненты: Гашков Сергей Борисович,

доктор физико-математических наук, профессор (ФГБОУ ВПО "Московский государственный университет имени М. В. Ломоносова", Механико-математический факультет, кафедра дискретной математики)

Мастихина Анна Антоновна, кандидат физико-математических наук, ассистент (ФГБОУ ВПО "Московский государственный технический университет имени Н.Э.Баумана", кафедра "Высшая математика")

Ведущая организация: ФГБОУ ВПО "Национальный исследовательский университет «МЭИ»"

Защита диссертации состоится 22 ноября 2013 г. в 16 ч. 45 мин. на заседании диссертационного совета Д.501.001.84 при ФГБОУ ВПО "Московский государственный университет имени М. В. Ломоносова" по адресу: 119991, Москва, ГСП-1, Ленинские горы, д.1, ФГБОУ ВПО "Московский государственный университет имени М. В. Ломоносова", Механико-математический факультет, аудитория 14-08.

С диссертацией можно ознакомиться в Фундаментальной библиотеке ФГБОУ ВПО "Московский государственный университет имени М. В. Ломоносова". (Москва, Ломоносовский проспект, д.27, сектор А, 8 этаж)

Автореферат разослан 22 октября 2013 г.

Ученый секретарь диссертационного совета $ /7

Д.501.001.84 при МГУ им М.В. Ломоносова,

д.ф.-м.н., профессор Иванов А.О.

Общая характеристика работы Актуальность темы

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

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

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

В функциональном подходе в качестве логической системы рассматривается пара вида {М, П), где M является множеством объектов системы, а в качестве П берется множество допустимых операций над объектами системы. Примерами таких систем являются множества функций с операцией суперпозиции, множество автоматных функций с операциями композиции и обратной связи, исчисления высказываний, интуиционистская логика, модальные логики, логика доказуемости и другие, где в качестве объектов выступают формулы, а в качестве операций, как правило, высту-

1 Яблонский C.B. Введение в дискретную математику. — М., Наука, 1986.

2Подколзин A.C. Компьютерное моделирование логических процессов. Архитектура и языки решателя задач. — М: ФИЗМАТЛИТ, 2008.

пают операция подстановки и операция modus ponens: если выводимо А и А влечет В, то В выводимо. С таким понятием логической системы (М, П) связан целый ряд задач функционального характера. К ним относятся такие важные проблемы, как задача о выразимости и вариант последней — задача о полноте, а также задача описания структуры решетки замкнутых относительно операций классов и задача базиса, которые, как правило, раскрывают содержательную суть рассматриваемой системы.

Основополагающую роль в решении проблемы выразимости для двузначной логики играет результат Э. Поста3 1941 года. Он изучил отношение выразимости для случая классической логики и полностью описал структуру всех замкнутых (относительно суперпозиций) классов булевых функций, названных впоследствии классами Поста. При переходе от двузначных логик к многозначным обнаружились принципиальные отличия в выразимости одних объектов через другие. Попытка обозрения замкнутых классов функций для многозначной логики натолкнулась на принципиальные трудности, связанные с континуальным обилием замкнутых классов, обнаруженных Ю.И.Яновым и A.A.Мучником4. Аналогичные трудности были обнаружены М.Ф.Раца5 даже в простейшей неклассической логике первой матрицы Яськовского.

Для двузначного случая проблема полноты относительно операции суперпозиции была полностью решена Э. Постом. Им же были предприняты первые шаги по решению данной проблемы для многозначных логик. В качестве одного из основных подходов к решению проблемы полноты выступает подход, впервые осуществленный в работах А.В.Кузнецова и С.В.Яблонского и состоящий в получении критериев полноты в терминах так называемых предполных классов. Основываясь на нем, в 1954 году С.В.Яблонским6 была решена проблема полноты для 3-значной логики.

3Post E.L. Two-valued iterative systems of mathematical logic. 11 Princeton Univ. Press, Princeton, 1941.

*Янов Ю.И., Мучник A.A. О существовании fc-значньгх замкнутых классов не имеющих конечного базиса. // ДАН СССР, т. 127, №1, с. 44-46, 1959.

5Раца М.Ф. О функциональной полноте в интуиционистской логике высказываний. // Пробл. ки-берн., т. 39, с. 107-150, 1982.

6Яблонский C.B. О функциональной полноте в трехзначном исчислении. // ДАН СССР, т.95, JV!6, с. 1153-1156, 1954.

Идея решения задачи о полноте в терминах предполных классов впоследствии стала одной из самой главной для fc-значных логик. Так, в 1964 году

A.И.Мальцев на этом пути решил задачу о полноте для четырехзначной логики, а затем рядом авторов С.В.Яблонским7, А.В.Кузнецовым, Розенбер-гом8 и др. были последовательно построены в явном виде все предполные классы для k-значных логик. Завершающее построение при этом провел Розенберг в 1970 году.

Впервые проблема выразимости для пропозициональных исчислений была поставлена Тарским9 в 1946 году па конференции по проблемам математики, посвященной двухсотлетию Принстонского университета. Уже в 1949 году Линиал и Пост10 опубликовали короткую заметку, в которой без доказательства сформулировали гипотезу об алгоритмической неразрешимости проблемы полноты для классического исчисления высказываний. Доказательство данного результата постепенно было восстановлено последующими авторами. Первым в этом направлении был Дэвис11, который в 1958 году опубликовал первый вариант доказательства, далее в 1963 году Синглетари12 и в 1964 — Интема13 завершили доказательство. Независимо от них в 1958 году Харроп14 построил конечную систему аксиом над двумя бинарными связками и конечное множество правил вывода, для которых проблема выразимости алгоритмически неразрешима. Следующим продвижением в этом направлении был отказ от фиксирования логических

7 Яблонский С.В. Функциональное построение в fc-значной логике. /// Труды матем. ин-та им

B.А.Стеклова, Из-во АН СССР, т. 51, с. 5-142, 1958.

8Rosenberg J. La structure des fonctions de plusiers variables sur uii ensemble fini. // Comptes Rendus Acad. Sci. Paris, №260, p. 3817-3819, 1965.

9Address at the princeton university bicentennial conference on problems of mathematics (December 17-19, 1946), by Alfred Tarski. // The Bulletin of Symbolic Logic, vol. 6, num. 1, 2000.

10Linial S., Post E.L., Recursive unsolvability of the deducibility, Tarski's comleteness, and independence of axioms problems of the propositional calculus (abstract). // Bulletin of the American Mathematical Society, vol. 55, p. 50, 1949.

"Davis M., Computability and unsolvability. // McGraw-Hill, New York, pp. 137-142, 1958.

nSingletary W.E., A complex of problems proposed by Post. // Bulletin of the American Mathematical Society, vol. 70, num. 1, pp. 105-109, 1964.

13 Yntema U.K., A detailed argument for the Post-Linial theorems. // Notre Dame Journal of Formal Logic, vol. 5, num. 1, pp. 37-50, 1964.

ilHarrop R. On the existence of finite models and decision procedures. // Proceedings of the Cambridge

Philosophical Society, vol. 54, pp. 1-16, 1958.

связок. Так, в 1963 году Глэдстоун15 обобщил результат Линиала и Поста на случай произвольной конечной системы связок, из которых выразима импликация. При этом он заменил операцию modus ponens на ее синтаксический аналог. Независимо от Линиала и Поста в 1963 году А.В.Кузнецов16 доказал алгоритмическую неразрешимость целого класса задач для пропозициональных исчислений с операцией modus ponens, куда входит проблема эквивалентности, проблема полноты и выразимости.

Впоследствии задача решения проблемы выразимости стала возникать в разнообразных логиках, задаваемых исчислениями, которые необязательно обладают адекватными конечными моделями. К таким логикам относятся интуиционистская логика, модальные логики, логика доказуемости и др. В этом направлении А.В.Кузнецов17 попытался перенести отношения выразимости на случай языка формул той или иной логики путем явного использования правила замены эквивалентным в рассматриваемой логике. М.Ф.Раца18 рассмотрел модальные логики с точки зрения отношения выразимости и доказал, что для многих из них, в том числе для наиболее известных, какими являются логика 54 Люиса и логика Грже-горчика, не существует алгоритма, решающего проблему выразимости в них. Ему же удалось доказать, что для пропозициональной логики доказуемости Геделя-Леба, а также для многих ее расширений алгоритма распознавания выразимости не существует.

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

15 Gladstone M.D. Some Ways of Constructing a Propositional Calculus of Any Required Degree of Unsolvabiiity. // Transactions of the American Mathematical Society, vol. 118, pp. 192-210, 1965.

16Кузнецов A.B. Неразрешимость общих проблем полноты, разрешимости и эквивалентности для исчислений высказываний. // Алгебра и логика, том 2, номер 4, с. 47-66, 1963.

17Кузнецов A.B. О функциональной выразимости в суперинтуиционистских логиках. // Матем. исследования, т. 6, №4, с. 75-122, 1971.

18Раца М.Ф. Алгоритмическая неразрешимость проблемы выразимости в модальных логиках. // Матем. пробл. киберн. т. 2, с. 71-99, 1989.

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

Особое внимание в изучении логических систем уделяется выделению систем образующих или базисов рассматриваемых систем. Системы образующих двузначных логик уже давно изучаются многими авторами. Так, Э. Пост19 доказал, что, если ограничиться только рассмотрением операции суперпозиции, то каждая двузначная логика конечно порождена. Л.Хенкин20 показал, что каждая двузначная логика, содержащая классическую импликацию, конечно порождена относительно операции modus ponens. При переходе от двузначных логик к &-значным для к > 3 обнаружились принципиальные отличия этих объектов относительно выводимости или порождения из одних формул других. Так, для случая выводимости относительно суперпозиции Мучник показал, что не каждая А>значная логика конечно порождена, а Янов для каждого к > 3 доказал, что существует fc-значная логика, не имеющая базиса21.

Отдельным самостоятельным направлением в решении общей проблемы выразимости является описание структуры решетки замкнутых классов. Для двузначной логики с операцией суперпозиции решетка имеет счетное число замкнутых классов и ее структура полностью восстанавливается из результата Поста22. Для fc-значной логики это не верно, уже при к > 3 решетка континуальная. Подобные результаты были получены и для неклассических логик, в частности, континуальную надрешетку имеют ин-

туиционистская логика, модальные логики, логика доказуемости .

19Posi E.L. Two-valued iterative systems of mathematical logic. // Princeton Univ. Press, Princeton, 1941.

™Henkin L. Fragments of the propositional calculus. // J. Symb.Logic, vol. 14, pp. 42-82, 1949.

21 Янов Ю.И., Мучник A.A. О существовании к-значных замкнутых классов, не имеющих конечного базиса. /'/ ДАН СССР, т. 127, №1, с. 44-46, 1959.

22Яблонский C.B., Гаприлов Г.П., Кудрявцев В.Б. Функции алгебры логики и классы Поста. — М., Наука, 1966.

23Горбунов ¡i.A., Рыбаков М.Н. Континуальные семейства логик // Логические исследования, т. 14, с. 131-151, 2007.

Цель и задачи диссертационного исследования

Целью работы является исследование пропозиционального исчисления как функционального объекта. В соответствии с целью в работе были поставлены следующие задачи:

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

- найти минимально-достаточные условия, которые нужно наложить на правила вывода, чтобы образованное ими исчисление было конечно порождено;

- изучить вопрос существования и мощности базисов пропозициональных исчислений;

- исследовать размер и структуру решетки замкнутых классов;

- охарактеризовать предполные и дуально-предполные классы этой решетки.

Методы исследования

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

Научная новизна

Результаты работы являются новыми и состоят в следующем:

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

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

вывода. Критерий налагает ограничения как на сами модусные операции, так и на логические связки, из которых строятся формулы.

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

Теоретическое и прикладное значение

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

Апробация работы

Результаты диссертации неоднократно докладывались на семинарах механико-математического факультета МГУ им. М. В. Ломоносова: на семинаре "Кибернетика и информатика" под руководством профессора В. Б. Кудрявцева (2008 - 2013 гг.), на семинаре "Теория автоматов" под руководством профессора В. Б. Кудрявцева (2008 - 2013 гг.).

Результаты докладывались на следующих конференциях:

1. Международная научная конференция студентов, аспирантов и молодых ученых "Ломоносов-2010", Москва, МГУ им. М.В.Ломоносова, 12 — 15 апреля 2010 года.

2. Международная научная конференция студентов, аспирантов и молодых ученых "Ломоносов-2011", Москва, МГУ им. М.В.Ломоносова, 11 — 15 апреля 2011 года.

3. Международная научная конференция студентов, аспирантов и молодых ученых "Ломоносов-2012", Москва, МГУ им. М.В.Ломоносова, 9 — 13 апреля 2012 года.

4. Международная научная конференция студентов, аспирантов и молодых ученых "Ломоносов-2013", Москва, МГУ им. М.В.Ломоносова, 8—13 апреля 2013 года.

5. Научная конференция "Ломоносовские чтения", Москва, МГУ им. М.В.Ломоносова, 14 — 23 ноября 2011 года.

6. Научная конференция "Ломоносовские чтения", Москва, МГУ им. М.В.Ломоносова, 16 — 24 апреля 2012 года.

7. Научная конференция "Ломоносовские чтения", Москва, МГУ им. М.В.Ломоносова, 15 — 24 апреля 2013 года.

8. X международный семинар "Дискретная математика и ее приложения", Москва, МГУ им. М.В.Ломоносова, 1 — 6 февраля 2010 года.

9. X международная конференция "Интеллектуальные системы и компьютерные науки", Москва, МГУ им. М.В.Ломоносова, 5 — 10 декабря 2011 года.

Публикации

Основные результаты диссертации опубликованы в 9 работах автора, представленных в конце автореферата [1-9].

Структура и объем диссертации

Диссертация объемом 91 страница состоит из "Введения", трёх глав и списка литературы, содержащего 51 наименование.

Содержание работы

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

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

Во второй главе рассматриваются общие вопросы структуры решетки замкнутых классов тавтологий: глубина и ширина решетки, предполные и дуально-предполные замкнутые классы, критериальные системы. Основные результаты второй главы представлены теоремами 3-7. Первый раздел главы посвящен размеру решетки, в нем формулируется и доказывается теорема 3 о достаточных условиях континуальности решетки замкнутых классов и теорема 4 о размерах решетки. Во втором разделе представлена с доказательством теорема 5 о числе предполных классов тавтологий. Третий раздел содержит доказательство теоремы 6 об отсутствии дуально-предполных классов пропозиционнальных исчислений. В четвертом разделе рассматриваются критериальные системы тавтологий и доказывается теорема 7 о мощностях критериальных систем.

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

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

Пусть Е2 = {0,1}, Р2 — множество булевых функций. Число существен-

ных переменных функции / € Р2 обозначим через х(/). На множестве определим оператор замыкания [•] 24, порожденный операцией суперпозиции.

Пусть и — счетный универсум переменных, £ С Р2 — конечное множество функций и X С К — некоторое множество переменных, тогда множество формул над логическими связками из Е и множеством переменных X обозначим через Когда X = II множество Ф%(Х) будем для крат-

кости обозначать через Ф^. Равенство формул 21, ® € Фе будем обозначать через 21 = 58. Зависимость формулы 21 от переменной х обозначим через Щх), зависимость от переменных Х\,..., хп — через Щх\,..., хп).

Каждой формуле 5" е Фе однозначно сопоставим функцию /у € [Е и {я}], где х 6 Рг — тождественная функция. Формулу £ из Фе будем называть тавтологией, если /5(11,..., гт) = 1 при любых значениях ¿1,..., гт из Ез, где т — это арность функции /5. Обозначим через ТЪ множество всех тавтологий в ФеНа множестве формул Фе определим понятие модусной операции. Пусть 5о)1?1| различные формулы из Фе({х1, X,,}), тогда набор

■••! дт')т?о) задает операцию ш : —► Фе, определенную следующим образом:

где £о, ^і,..., є Фе- Множество всех модусных операций на Фе обозначим через Л4е- Множество всех модусных операций ш Є Л4г, которые тавтологии переводят в тавтологии, обозначим через Отъ• Такие операции будем называть допустимыми.

Множество тавтологий ТЬ и множество допустимых операций П образуют алгебраическую систему (ТЬ, П), которую будем называть пропозициональным исчислением. На ТЬ определим оператор замыкания, порожденный операциями из П. Этот оператор будем обозначать через [-]п или

мВо избежание увеличения количества обозначений, операторы замыкания для множеств различной природы имеют одно и тоже обозначение [•].

=6 Э®1, ...,хп Є Фе & = Зі(яі, -,Х„)

просто через [•], когда множество фиксировано. Понятие замкнутого, полного и предполного класса, базиса дается стандартным образом.

Будем говорить, то операция и> = (Зі,..., З™; Зо) Є Ме({хі, —, выводима из множества операций П С если существует такое конечное множество тавтологий М С Тії, что для любых формул 21і,..., 21„ Є Фц из М и ...,21п),г = 1, ...,т, выводима формула Зо(21і, ■■•, 21л)- Выводимость операции и> из множества операций обозначим через Г2 Ь ал

Понятие линейной, монотонной, а-, /3-, 7-, ¿-функции в Р2 определяются стандартным образом. Функция /(¡Ті, ...,хп,у) Є Р2 называется им-пликативной, если для нее выполнено соотношение /(сті, ...,ап,сго) = 0 его < аі, і = 1, ...,п, где &і Є Е2. Множество всех линейных, монотонных и импликативных функций в Р2 обозначим через Ь, М и I соответственно.

Теорема 1 (Критерий конечно-порожденности). Для любого конечного множества логических связок £ С Р2 и произвольного конечного множества допустимых на ТЬ операций Г2 С Оть, существуют такие конечные Сіь, Сім, П/ С Оть, что исчисление (ТЬ, £7) конечно порождено тогда и только тогда, когда выполнено хотя бы одно из условий

1. ЕСІ, 1 є [£] к Ш- Пь;

2. ЪСМ, 1 Є [£] и П Ь Пм;

3. [£]П 1ф% и Г21- 0/; 4- ТЬ = 0.

Теорема 2 (Мощности базисов). Для классического исчисления высказываний (ТЬ, {штр}) с логическими связками £ = {А, V, -і, —»} выполнено каждое из условий

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

2. Существует замкнутый класс тавтологий, имеющий счетный базис;

3. Существует замкнутый класс тавтологий, не имеющий базиса;

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

Определим на множестве Мт. операцию суперпозиции, состоящую из следующих элементарных операций:

Переименование и отождествление переменных. Пусть ш, ы' € .Ме, причем

...,6п) = & О I Ри(£о,£ъ ...,&»»))

-,Т1т) = Т}0<* к.....г,т(па | Рщ-(т,ЛЪ -,Чт))

Будем говорить, что операция о/ получена из операции ш с помощью переименования переменных, если выполнено

РЛЛо^и-^т) = Рш{г]0,Ли-,Г]т)

ДЛЯ любых 77г € ТЬ.

Добавление несущественных переменных. Пусть € Л4-£, причем

Будем говорить, что операция а/ получена из операции и> с помощью добавления несущественных переменных Г]1,...,Т]п, если выполнено

Ры'(£0,£ъ •••,£т,»?1, —,Г]п) = -Ры(£о,6> — >6п) для любых € ТЬ.

Изъятие несущественных переменных. Пусть ш, и' € .Ме, причем

= $0 ^.....{„Ль-Л™ | .....1п))

"/(б,-,6») .....?т($0 |

Будем говорить, что операция а/ получена из операции ш с помощью изъятия несущественных переменных 771, .... т]п, если выполнено

для любых 7}] 6 ТЪ.

Подстановка одной операции в другую. Пусть 6 Мя> причем

£^(6,-,£т) = ¿10 Ае1.....ет(Со | р^-,{т))

Ыт, ••■>%) = т I РьъЫт, -,г?т))

ш(Сь •••> Ст+п-1) = Со Л(ь...,ст(Со I -£ЦС(ьСъ •■•) Ст+п—1))

где

если 0 < < г — 1, Сз = ^"-»+11 если г<j<i + ^n — 1,

^ если г + т<^<т + п — 1. Будем говорить, что операция о; получена из операций а>1 и и>2 с помощью подстановки, если Р«(Со,С1.....Ст+п-1) — это предикат

Зх е Фе(РШ1(Со,Сь "^¿-ь^Сг+т, Ст+п-1) А Ри2(х, Си ■■■, Сг+т-О)

Сужение. Пусть и = ($и ..., 5о> € о/ = (0Ь ..., 0т; 0О) 6 Ме

и сг: X —> Фе — некоторая подстановка. Будем говорить, что операция ш' получена из операций ш сужением с помощью подстановки сг, если выполнено

&i = aSi, г = 0,1, ...,т.

Множество всех операций в М^, полученных из операций множества Я С с помощью суперпозиции, обозначим через [П]. Не сложно проверить, что [П] является оператором замыкания на Л4е.

Введем на множестве формул Фе отношение <. Пусть 21 6

Фе({хь ...,а:п}) и 05 € Фе, тогда положим

Я < В ^ ЗСг,..., Сп е Фе (*(£!,..., О = ®)

Формулы 21, ® £ ФЕ({а;1,.... хп}) будем называть совместными и писать 21 ~ 58, если существуют такие £1,..., <£„, 3)ь ..., Эп £ Фе, что

а(сь...,е„) = «(3)1, ...,©„)

Теорема 3. Для любого конечного множества логических связок ЕСР2 и произвольного множества допустимых на ТЬ операций П С Оть если найдется такая тавтология 21 € ТЬ, что для любой операции ш 6 [П], где ш = (З1, найдется такое г £ т, что & ф. 21, то решетка

замкнутых классов исчисления (ТЬ, П) континуальная.

Следствие 1. Для любого конечного множества логических связок Е С Рг и произвольного множества допустимых на ТЬ операций Г2 С Оть, если Г) не содержит констант и найдется такая тавтология 21 £ ТЬ, что для любой операции ш 6 О, где ш = (Зъ..., &о), найдется такое г £ Ш, что & ф- 21, то решетка замкнутых классов исчисления (ТЬ, П) континуальная.

Теорема 4 (Размеры решетки замкнутых классов). Существуют такие множества логических связок ЕС Р2 и множества допустимых на ТЬ операций П С Оть, что исчисление (ТЬ, П) имеет конечную, счетную и континуальную мощность решетки замкнутых классов тавтологий соответственно.

Теорема 5 (Число предполных классов). Существуют такие множества логических связок ЕСР2и множества допустимых на ТЬ операций О ^ Оть, что исчисление (ТЬ, Г2) не имеет предполных классов тавтологий, имеет конечное, счетное и континуальное множество предполных классов тавтологий соответственно.

Замкнутый класс тавтологий С} С ТЬ называется дуально-предполным,

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

Рассмотрим произвольное множество логических связок Е С Р2. из которых выразима импликативная функция —>. Обозначим формулу, выражающую эту функцию, через х\...хп —> у. Для краткости будем писать х —* у вместо ¿с^л; —> у. Операцию, заданную схемой

Хх, --ч Хп, Х\...Хп > у

обозначим через штр и назовем обобщенной операцией modus ponens.

Теорема 6. Исчисление (Th, {wmp}) не имеет дуалъно-предполных классов.

Теорема 7 (Мощность критериальной системы). Существуют такие множества логических связок Е С Р2 и множества допустимых на Th операций Г2 С 0Th, что исчисление (Th, Г2) не имеет критериальной системы, имеет конечную, счетную и континуальную критериальную систему соответственно.

Каждую формулу из Фк можно представлять в виде ориентированного дерева, листьям которого приписаны переменные из U, а внутренним вершинам — элементы множества s. Каждой позиции в этом дереве соответствует, с одной стороны, элемент множества EUli, с другой — подформула из Ф^. Введем функции для задания символа и подформулы данной формулы в данной позиции. Позиции в формуле будем задавать словами над множеством N. Отображение ф сопоставляет каждой формуле 5 в Фг отображение : N* —► Е U U U {-L}, где ± — символ, не принадлежащий EUlX и — символ в позиции а. Отображение Т] сопоставляет каждой

формуле £ € Фе отображение щ : М* —* Фни{±}, где щ{а) — подформула в позиции а.

Рассмотрим произвольную модусную операцию ш = гДе

■Si € Фе(Хп), i = l,...,m, и Хп = {xi,..., хп}. Разрешающим уравнением

аргумента операции ...,£m) будем называть уравнение:

—ii?m t= ïo = dp-

В данном разделе будем требовать, чтобы каждое переменное, содержащееся в формуле So также содержалось в одной из формул i = 1,..., m.

Обозначим его через £р. Это уравнение разрешимо, если существуют такие формулы 2ii,...,2l„ € Фе, что &(21ь 6 Th и Ç(Qtu ...,Шп) =

Пара (х, Л) € Vp тогда и только тогда, когда найдется такое слово /3, что либо ipSo{/3) = х и фзр(0) =±, либо фз„(/?) =_L и ^,(/3) = х. Для а ф Л пара (ж, a) G Vp тогда и только тогда, когда найдется такое слово 0, что либо ФМ = х и ФгР{0а) 6 X", либо е X" и ^,(0) = s.

Пара ((ж, а), (у,0)) £ Ер тогда и только тогда, когда найдется такое слово 7, что либо а = Л и тогда ■ф^'уР) = г, ^,(7) = 2/, либо ¡3 — Л и тогда Vso(7) = я. фзр{1&) = у-

Определим отношение эквивалентности ~р на множестве вершин Ур разрешающего графа Gp. Отношение ~р строится конструктивно. Для каждого (ж, а) 6 Vp положим (х, а) ~р (х, а), a для (х,а), (у,0) е Vp положим (ж, а) (у,/?) тогда и

только тогда, когда найдутся такие эквивалентные вершины

(*',<*')> (у',Р') 6 что либо ((a/.ûO.foa)), ((¡ЛР')Лу,Р)) €

либо ((х, а), (х\ а')), ((г/, /?), (у',/3')) € Ер. Не сложно проверить, что эквивалентные вершины принадлежат одной связной компоненте графа Gp.

Аргумент £р операции будем называть перестановочным,

если его разрешающее уравнение £р имеет решение и найдутся такие неэквивалентные вершины (х,а),(у,Р) G Vp разрешающего графа Gp из одной компоненты связности, не содержащей циклов, такие различные переменные z\,...,zq-i е Хп, не принадлежащие Зо и Зр, и такие различные h,...,ig е {1,...,ш}\{р}, что

x,zi е zi,z2 6 ... 2Н,уе 16

Сужение а/ = {©1,..., ©т'; ©о) операции ш будем называть правильным, если 01,..., 0т' разрешимы в тавтологиях, ©* ф. <3j для любых 1 < г < ] < т' и [М]{ш} = [М]{ы.} для любого М = {2I € ТЬ | < 21, г = {1,..., т'}}.

Теорема 8. Для любой полной системы логических связок Е и любой модусной операции ш е Оть> имеющей правильное сужение с перестановочным аргументом, проблема выразимости исчисления (ТЬ, {а;}) алгоритмически не разрешима.

Теорема 9. Для любой полной системы логических связок Е и любой модусной операции и> € Отъ, имеющей правильное сужение с перестановочным аргументом, существует такое множество М С ТЬ, что проблема полноты исчисления (ТЬ, {о;}) алгоритмически не разрешима, если М — полно в ТЬ.

Благодарности

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

Публикации автора по теме диссертации

1. Боков Г. В. Проблема полноты в исчислении высказываний. // Интеллектуальные системы, т. 13, вып. 1-4, 2009, с. 165-181.

2. Боков Г. В. Критерий конечной порожденности пропозициональных исчислений. // Дискрет. Матем., т. 25, вып. 3, 2013, с. 63-81.

3. Боков Г. В. Об алгоритмической неразрешимости проблемы выразимости пропозициональных исчислений. // Интеллектуальные системы, т. 17, вып. 1-4, 2013, с. 271-292.

4. Боков Г. В. О конечной порожденности исчисления'высказываний с произвольными операциями вывода // Интеллектуальные системы, т. 17, вып. 1-4, 2013, с. 267-270.

5. Боков Г. В. О проблеме полноты в исчислении высказываний. // Материалы X Международного семинара «Дискретная математика и ее приложения» (Москва, МГУ, 1-6 февраля 2010 г.) / Отв. Ред.: В. В. Кочергин; под общ. ред.:0. М. Касим-Заде. М.: Механико-математический факультет МГУ, 2010, с. 345-348.

6. Боков Г. В. Об алгебраических свойствах исчисления высказываний. // Материалы Международного молодежного научного форума «ЛОМОНОСОВЫМ» / Отв. ред. И.А. Алешковский, П.Н. Костылев, А.И. Андреев, A.B. Андриянов. [Электронный ресурс] — М.: МАКС Пресс, 2010. - URL: http://www.lomonosov-msu.ru/archive/Lomonosov_2010/index.htm

7. Боков Г. В. Обобщение теоремы Хенкина на случай к-значных логик. // Материалы Международного молодежного научного форума «ЛОМОНОСОВ-2011» / Отв. ред. А.И. Андреев, A.B. Андриянов, Е.А. Антипов, М.В. Чистякова. [Электронный ресурс] — М.: МАКС Пресс, 2011. - URL: http://www.lomonosov-msu.ru/archive/Lomonosov_2011/1257/5161_7cbd.pdf

8. Боков Г. В. Об алгоритмически разрешимых случаях проблемы выразимости в пропозициональных исчислениях. // Материалы Международного молодежного научного форума «ЛОМОНОСОВ-2012» / Отв. ред. А.И. Андреев, A.B. Андриянов, Е.А. Антипов, К.К. Андреев, М.В. Чистякова. [Электронный ресурс] — М.: МАКС Пресс, 2012. - URL: http://www.lomonosov-msu.ru/archive/Lomonosov_2012/1793/5161_a567.pdf

9. Боков Г. В. Алгоритмическая разрешимость проблемы выразимости автоматно-отделимых подалгебр термов. // Материалы Международного молодежного научного форума «ЛОМОНОСОВ-2013» / Отв. ред. А.И. Андреев, A.B. Андриянов, Е.А. Антипов, К.К. Андреев, М.В. Чистякова. [Электронный ресурс] — М.: МАКС Пресс, 2013. - URL: http://www.lomonosov-msu.ru/archive/Lomonosov_2013/2193/5161_30ee.pdf

Отпечатано в отделе оперативной печати Геологического ф-та МГУ Тираж !00 экз. Заказ № Н9

Текст научной работы диссертации и автореферата по математике, кандидата физико-математических наук, Боков, Григорий Владимирович, Москва

ФГБОУ ВПО

МОСКОВСКИЙ ГОСУДАРСТВЕННЫЙ УНИВЕРСИТЕТ ИМЕНИ М.В. ЛОМОНОСОВА

МЕХАНИКО-МАТЕМАТИЧЕСКИЙ ФАКУЛЬТЕТ

оаоН5 \ЬЫ

Боков Григорий Владимирович УСЛОВИЯ ВЫРАЗИМОСТИ И ПОЛНОТЫ ПРОПОЗИЦИОНАЛЬНЫХ ИСЧИСЛЕНИЙ

01.01.09 — дискретная математика и математическая кибернетика

ДИССЕРТАЦИЯ

на соискание учёной степени кандидата физико-математических наук

Научный руководитель: доктор физико-математических наук, академик, профессор В. Б. Кудрявцев

МОСКВА - 2013

Оглавление

Введение 2

Основные понятия диссертации 12

1 Проблема базиса 19

1.1 Критерий конечно-порожденности..............................19

1.2 Мощность базисов................................................44

2 Структура решетки замкнутых классов тавтологий 52

2.1 Глубина и ширина решетки......................................-52

2.2 Предполные классы..............................................58

2.3 Дуально-предиолные классы....................................63

2.4 Критериальные системы..........................................65

3 Проблема полноты и выразимости 67

3.1 Алгоритмическая неразрешимость проблемы выразимости . 67

3.2 Алгоритмическая неразрешимость проблемы полноты .... 82

Заключение 84

Литература 86

Введение

Общая характеристика работы Актуальность темы

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

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

в качестве П берется множество допустимых операций над объектами системы. Примерами таких систем являются множества функций с операцией суперпозиции [24], множество автоматных функций с операциями композиции и обратной связи [7], исчисления высказываний [15], интуиционистская логика [34], модальные логики [21], логика доказуемости [40, 11] и другие, где в качестве объектов выступают формулы, а в качестве операций, как правило, выступают операция подстановки и операция тоЛ/,5 ропет1. С таким понятием логической системы (М, О) связан целый ряд задач функционального характера. К ним относятся такие важные проблемы, как задача о выразимости и вариант последней — задача о полноте, которые, как правило, раскрывают содержательную суть рассматриваемой системы. Выразимость между объектами в логической системе означает возможность получения одних из них через другие посредством заранее определенного набора правил, в частности, посредством суперпозиций. Проблема выразимости состоит в описании всех таких пар конечных множеств объектов логической системы, для которых все элементы одного множества можно выразить через элементы другого множества. Зачастую не всегда для рассматриваемой логической системы удается решить проблему выразимости для произвольных объектов. Для таких систем принято рассматривать частный случай проблемы выразимости, а именно, проблему полноты. Проблема полноты состоит в описании таких множеств объектов рассматриваемой системы, отправляясь от которых можно получить посредством заранее определенного набора правил все объекты данной системы.

Основополагающую роль в решении проблемы выразимости для двузначной логики играет результат Э. Поста 1921 года [37]. Он изучил отношение выразимости для случая классической логики и полностью описал структуру всех замкнутых (относительно суперпозиций) классов булевых функций, названных впоследствии классами Поста [27]. На основе данного описания замкнутых классов уже нетрудно построить алгоритм распозна,-вания выразимости в классической логике высказываний, позволяющий по любой булевой функции, заданной формулой или таблицей, и любой

хТо есть, если выводимо а и а влечет в, то в выводимо.

конечной системе таких функций распознавать, выразима ли эта функция через эту систему посредством суперпозиции. При переходе от двузначных логик к многозначным обнаружились принципиальные отличия в выразимости одних объектов через другие. Попытка обозрения замкнутых классов функций для многозначной логики натолкнулась на принципиальные трудности, связанные с континуальным обилием замкнутых классов, обнаруженных Ю.И.Яновым и А.А.Мучником [28]. Аналогичные трудности были обнаружены М.Ф.Раца [17] даже в простейшей неклассической логике первой матрицы Яськовского [35]. В этой связи, хотя для любой конеч-нозначной логики существует алгоритм для распознавания выразимости, основанный на переборе всех функций от данных переменных, выразимых через данную систему, однако такой перебор в большинстве случаев является громоздким и поэтому соответствующий алгоритм практически не реализуем.

Для двузначного случая проблема полноты относительно операции суперпозиции была полностью решена Э. Постом [37]. Им же были предприняты первые шаги по решению данной проблемы для многозначных логик. В качестве одного из основных подходов к решению проблемы полноты выступает подход, впервые осуществленный в работах А.В.Кузнецова и С.В.Яблонского [25, 26] и состоящий в получении критериев полноты в терминах так называемых предполных классов. Принцип определения критериев зависит от свойств структуры замкнутых подмножеств рассматриваемого множества. Основным понятием в данном подходе служит понятие критериальной системы [6]. Основываясь на нем, в 1954 году С.В.Яблонским [25[ была решена проблема полноты для 3-значной логики. Решение было сведено к описанию всех предполных классов в ней, при этом было показано, что множество предполных классов образует критериальную систему. Сами предполные классы при этом были явно описаны. Из этого описания вытекал алгоритм распознавания полноты для конечных систем. Идея решения задачи о полноте в терминах предполных классов впоследствии стала одной из самой главной для /с-значных логик. Так, в 1964 году А.И.Мальцев на этом пути решил задачу о полноте для четырех-

значной логики, а затем рядом авторов С.В.Яблонским, А.В.Кузнецовым, Л о Чжу-каем, Розенбергом и др. были последовательно построены в явном виде все предполные классы для k-значных логик [26, 12, 3, 38]. Завершающее построение при этом провел Розенберг в 1970 году.

Впервые проблема выразимости для пропозициональных исчислений была поставлена Тарским в 1946 году на конференции по проблемам математики, посвященной двухсотлетию Принстонского университета [41]. Уже в 1949 году Линиал и Пост [36] опубликовали короткую заметку, в которой без доказательства сформулировали гипотезу об алгоритмической неразрешимости проблемы полноты для классического исчисления высказываний. Доказательство данного результата постепенно было восстановлено последующими авторами. Первым в этом направлении был Дэвис [29], который в 1958 году опубликовал первый вариант доказательства, далее в 1963 году Синглетари [39] и в 1964 — Интема [42] завершили доказательство. Независимо от них в 1958 году Харроп [32] построил конечную систему аксиом над двумя бинарными связки и конечное множество правил вывода, для которых проблема выразимости алгоритмически неразрешима. Следующим продвижением в этом направлении был отказ от фиксирования логических связок. Так, в 1963 году Глэдстоун [30] обобщил результат Линиала и Поста на случай произвольной конечной системы связок, из которых выразима импликация. При этом он заменил операцию m.odus ponens на ее синтаксический аналог. Независимо от Линиала и Поста в 1963 году Кузнецов [9] доказал алгоритмическую неразрешимость целого класса задач для пропозициональных исчислений с операцией modus ponens, куда входит проблема эквивалентности, проблема полноты и выразимости.

сматриваемой логике. Общая проблема выразимости в данной логике ставится следующим образом. Требуется указать алгоритм, который по любой формуле и любой конечной системе формул языка этой логики позволял бы распознавать, выразима ли эта формула через эту систему, используя лишь правило замены эквивалентным в этой логике и ослабленное правило подстановки. М.Ф.Раца [18, 19] рассмотрел модальные логики с точки зрения отношения выразимости и доказал, что для многих из них, в том числе для наиболее известных, какими являются логика 54 Люиса [21] и логика Гржегорчика [31], не существует алгоритма, решающего проблему выразимости в них. Ему же удалось доказать, что для пропозициональной логики доказуемости Геделя-Леба, а также для многих ее расширений алгоритма распознавания выразимости не существует [20].

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

Особое внимание в изучении логических систем уделяется выделению систем образующих или базисов рассматриваемых систем. Системы образующих двузначных логик уже давно изучаются многими авторами. Так, Э. Пост [37] доказал, что, если ограничиться только рассмотрением операции суперпозиции, то каждая двузначная логика конечно порождена. Л.Хенкин [33] показал, что каждая двузначная логика, содержащая классическую импликацию, конечно порождена относительной операции modus ponens. При переходе от двузначных логик к к-значным для к > 3 обнаружились принципиальные отличия этих объектов относительно выводимости или порождения из одних формул других. Так, для случая выво-

димости относительно суперпозиции [28] Мучник показал, что не каждая /с-значная логика конечно порождена, а Янов для каждого к > 3 доказал, что существует /с-значная логика, не имеющая базиса.

Отдельным самостоятельным направлением в решении общей проблемы выразимости является описание структуры решетки замкнутых классов. Для двузначной логики с операцией суперпозиции решетка имеет счетное число замкнутых классов и ее структура полностью восстанавливается из результата Поста [27]. Для /с-значной логики это не верно, уже при к > 3 решетка континуальная [6]. Подобные результаты были получены и для неклассических логик, в частности, континуальную надрешетку имеют интуиционистская логика, модальные логики, логика доказуемости [2].

Цель и задачи диссертационного исследования

- найти минимально-достаточные условия, которые нужно наложить па правила вывода, чтобы образованное ими исчисление было конечно порождено;

- изучить вопрос существования и мощности базисов пропозициональных исчислений;

- исследовать размер и структуру решетки замкнутых классов;

- охарактеризовать предполные и дуально-предполные классы этой решетки.

Методы исследования

Научная новизна

Результаты работы являются новыми и состоят в следующем:

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

Теоретическое и прикладное значение

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

Апробация работы

Результаты докладывались на следующих конференциях:

3. Международная научная конференция студентов, аспирантов и молодых ученых "Ломоносов-2012", Москва, МГУ им. М.В.Ломоносова. 9 — 13 апреля 2012 года.

5. Научная конференция "Ломоносовские чтения", Москва, МГУ им. М.В.Ломоносова, 14 — 23 ноября 2011 года.

6. Научная конференция "Ломоносовские чтения", Москва, МГУ им. М.В.Ломоносова, 16 — 24 апреля 2012 года.

7. Научная конференция "Ломоносовские чтения", Москва, МГУ им. М.В.Ломоносова, 15 — 24 апреля 2013 года.

Публикации

Основные результаты диссертации опубликованы в 9 работах автора [43]-[51|.

Структура и объем диссертации

Диссертация состоит из "Введения", "Основных понятий диссертации", трёх глав, в которых раскрыты основные результаты, заключения и списка литературы. Объем диссертации 91 страница. Список литературы содержит 51 наименование.

Содержание работы

В "Основных понятиях диссертации" даются формально основные определения, использующиеся на протяжении всей работы.

Первая глава работы посвящена исследованию проблеме базиса и доказательству критерия конечной порожденности пропозиционального исчисления. Основные результаты первой главы представлены теоремами 1-2. В первом разделе главы изучается вопрос конечной порожденности пропозиционального ис�