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

О*

- $ ДО-*4 " УДК 510.64

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

ШРАЙНЕР ПАВЕЛ АЛЕКСАНДРОВИЧ

ИНТЕРПОЛЯЦИЯ И ОПРЕДЕЛИМОСТЬ В ЛОГИКАХ КОНЕЧНЫХ ОБЛАСТЕЙ

01.01.06 — математическая логика, алгебра и теория чисел

Автореферат

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

Новосибирск 1998

10г

Работа выполнена на кафедре алгебры и математической логики Новосибирского государственного университета.

/

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

профессор Л. Л. Максимова

Официальные оппоненты — доктор физико-математических наук

Д. Е. Пальчунов — доктор физико-математических наук А. Г. Пинус

Ведущая организация — Красноярский государственный университет

Защита диссертации состоится 10 декабря 1998 года в 15 часов на заседании диссертационного совета Д 002.23.01 при Институте математики Сибирского отделения РАН по адресу: 630090, Новосибирск, 90, проспект Ак. Копгюга, 4.

С диссертацией можно ознакомиться в библиотеке Институте математики СО РАН

Автореферат разослан б ноября 1998 года

Ученый секретарь

диссертационного совета

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

А.Н.Ряскии

ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ

Актуальность темы. Теория неклассических логик — одна из важных областей современной логики. Особую роль среди многочисленных неклассических логик играет интуиционистская логика, возникшая в связи с критикой классической логики с позиций конструктивизма. На базе этой логики построены интуиционистская математика и конструктивная математика, основанные на конструктивном понимании существования математических объектов (см., например [1], [5]).

Формализация интуиционистской логики в виде исчисления, данная Гейтингом в 1930 году, подтолкнула интерес математиков к формулированию и изучению интуиционистских теорий с позиций классической математики. Основы такого подхода заложены в работах Геделя [17], Маккинси и Тарского [21], Новикова [8]. В данной работе мы также придерживаемся точки зрения классической математики при изучении неклассичсских логик.

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

Доказанная Янковым в 1968 году континуальность семейства суперинтуиционистских логик показывает невозможность эффективного описания всех суперинтуиционистских логик. Поэтому для изучения указанных семейств, как правило, выделяют классы логик, обладающих тем или иным свойством. К таким свойствам относятся, например, полнота по Крипке, разрешимость, дизъюнктивное, экзистенцио-нальное, интерполяционное свойство Крейга и свойство Бета.

Интерполяционная теорема для классической логики предикатов впервые была доказана В. Крейгом [14] в 1957 году. В 1962 году Шютте [27] доказал интерполяционную теорему для интуиционистской логики предикатов синтаксическим методом. Другие доказательства этого факта даны в работах Т. Нагашимы [23], Д. Габбая [16], X. Оно[24]. Д. Габбай в [16] представил семантическое доказательство интерполяционного свойства для некоторых расширений интуиционистской логики предикатов.

Л.Л.Максимова [6] доказала в 1977 году, что непротиворечивых пропозициональных суперинтуиционистских логик, имеющих интерполяционное свойство, только семь. Однако вопрос, поставленный X. Оно в [25], о том, какие предикатные суперинтуиционистские логики имеют интерполяционное свойство, остается открытым. Там же X. Оно полагает, что первым шагом к решению этой проблемы может явиться следующая задача: привести примеры предикатных логик, имеющих интерполяционное свойство. Естествен также и обратный вопрос, т. е. вопрос о примерах логик, не имеющих интерполяционного свойства. При этом можпо отметить, что если предикатная логика имеет интерполяционное свойство, то ее пропозициональная часть тоже должна иметь его и, значит, все логики, имеющие интерполяционное свойство, должны содержаться в классе предикатных расширений вышеупомянутых семи пропозициональных логик.

В 1960 году Г. Крайзель [20] установил, что все пропозициональные суперинтуиционистские логики имеют свойство Бета. Для предикатных супериитуиционистских логик такое утверждение не имеет места. Так, например, Ю. Гуревич в [18] доказал, что классическая логика конечных областей не обладает свойством Бета. Однако примеров логик без свойства Бета, промежуточных между интуиционистской и классической предикатными логиками, до настоящего времени не было известно.

Средствами интуиционистской логики свойство Бета можно вывести из интерполяционного свойства тем же способом, как это сделано в [14]. Отсюда получаем, что отсутствие у логики свойства Бета влечет отсутствие интерполяционного свойства.

Данная работа посвящена изучению интерполяционного свойства и свойства Бета для интуиционистской логики конечных областей с равенством характеризуемой всеми интуиционистскими шкалами Крипке, у которых все предметные области конечны, и близкой к ней логики Jjф характеризуемой всеми шкалами Крипке, у которых предметные области всех немаксимальных миров конечны. Поскольку справедливость указанных свойств существенно зависит от наличия в языке символа равенства (см., например, [11]), параллельно рассматривается также логика без равенства. '

Установлено отсутствие свойства Бета, и, следовательно, интерполяционного свойства у логик и 3*^. Логика является первым примером промежуточной логики без свойства Бета. Аналогичные результаты получены для фрагментов логик и Jjl¡ без равенства.

Л.Л.Максимова доказала в [7], что существует континуум предикатных суперинтуиционистскпх логик с равенством, имеющих интерполяционное свойство, и, следовательно, свойство Бета.

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

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

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

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

Комори в [19] построил некоторую модификацию стандартных шкал Крипке и доказал, что интуиционистская логика предикатов полна относительно этих шкал. Мы перенесли его идею на стандартные шкалы Крипке для предикатных суперинтуиционистских логик.

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

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

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

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

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

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

Основные результаты диссертации.

1. Установлено отсутствие свойства Бета и интерполяционного свойства у интуиционистской логики конечных областей. Данный результат верен как для логики с равенством, так и для логики без равенства.

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

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

3. Доказано, что фрагмент интуиционистской логики конечных областей, состоящий из формул первого порядка, не содержащих дизъюнкции и квантора существования, совпадает с аналогичным фрагментом интуиционистской логики предикатов. Этот фрагмент имеет слабый вариант интерполяционного свойства и свойства Бета.

Теоретическая и практическая ценность. Работа носит теоретический характер. Ее методы и результаты могут использоваться специалистами в области неклассических логик и теоретической информатики, для чтения лекций и спецкурсов в Московском, Новосибирском, Красноярском и др. госуниверситетах.

Апробация работы. Основные результаты, полученные в диссертации, докладывались'на:

• заседаниях семинаров "Неклассические логики" и "Алгебра и Логика" кафедры алгебры и математической логики механико-математического факультета НГУ,

в русско-японском коллоквиуме по нестандартным логикам и логическим аспектам информатики N81/95 (Иркутск, 1995),

• международной конференции "Логика, алгебра и информатика", посвященной памяти Елены Расевой (Царшава, 1996),

• международных конференциях "Мальцевские чтения" (Новосибирск, 1996,1998),

• международных научных студенческих конференциях " Студент и научно-технический прогресс" (Новосибирск, 1993,1995,1996),

• логическом коллоквиуме ЬС'98 (Прага, 1998),

• конференциях профессорско-преподавательского состава НГПУ (Новосибирск, 1994,1995,1996,1997,1998).

Публикации. Результаты диссертации опубликованы в шести работах автора [28]—[33].

Структура и объем работы. Диссертация состоит из введения и двух глав, разбитых на 8 параграфов. Список литературы содержит 34 наименования. Общий объем диссертации 89 страниц.

СОДЕРЖАНИЕ РАБОТЫ

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

В главе 1 изучается интерполяционное свойство и свойство Бета для логики конечных областей с равенством J¡d и близкой к ней логики ,7^, а также для их фрагментов без равенства и некоторых расширений.

Предложение Ф (Р) неявно определяет в логике Ь п-местный предикат Р, если в логике Ь доказуема формула

(Ф (Р) кФ (Р')) .-> V®!... Ухп (Р (хь..., Хп) Р' (*1,..., *„)) ,

где Р' — новый п-местный предикатный символ.

Предложение Ф(Р) явно определяет п-местный предикат Р в логике Ь, если существует формула С(х\,..., хп) такая, что все предикатные символы формулы С содержатся во множестве предикатных символов предложения Ф(Р), отличных от Р, и в логике Ь доказуема формула

Ф(Р) -> V*!. • • Чхп{Р{хи ...,!„)+♦ С{хъ ..., х„)).

Логика Ь имеет свойство Бета, если предложение, неявно определяющее предикат в логике Ь, определяет его в логике Ь явно.

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

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

Логика Ь имеет интерполяционное свойство, если для всякой формулы (Л -> В), принадлежащей логике Ь, существует формула С такая, что формулы (Л —> С) и (С —> В) принадлежат логике Ь, причем в формулу С входят лишь те предикатные символы и свободные предметные переменные, которые входят и в А, и в В.

Однако нам понадобится понятие слабого интерполяционного свойства:

Логика Ь имеет слабое интерполяционное свойство, если для всякой формулы (А —> В), принадлежащей логике Ь, существует формула С такая, что формулы (А —> С) и (С —В) принадлежат логике Ь, причем в формулу С входят лишь те предикатные символы, которые входят и в А, и в В.

Очевидно, что наличие у логики интерполяционного свойства влечет наличие слабого интерполяционного свойства.

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

Лемма 2. Если логика обладает слабым интерполяциоппым свойством, то она обладает свойством Бета.

Из отсутствия у интуиционистской логики конечных областей Л ¡а свойства Бета, в виду леммы 2, получается

Следствие 1. Логика Jf(l не имеет ни слабого, ни сильного интерполяционного свойства.

Построена в явном виде формула, у которой нет интерполянта в логике

Имеет место

Следствие 2. Если логика Ь содержится в классической логике конечных областей и содержит интуиционистскую логику конечных областей то Ь не имеет ни слабого, ни сильного интерполяционного свойства, ни свойства. Бета.

Там же доказана

Теорема 2. Существует континуум предикатных суперинтуиционистских логик с равенством, не имеющих свойства Бета.

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

В параграфе 1.3 показано отсутствие свойства Бета у логики 3^, характеризуемой всеми шкалами Крипке, у которых все предметные области всех немаксимальных миров конечны. Логика является первым примером промежуточной логики без свойства Бета. Контрпример к свойству Бета для логики построен в явном виде.

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

Следствие 4. Если логика Ь содержится в логике и содержит логику 3то Ь не имеет ни интерполяционного свойства, ни свойства Бета.

Л. Л. Максимова доказала в [7], что существует континуум предикатных суперинтуиционистских логик с равенством, имеющих интерполяционное, свойство и, следовательно, свойство Бета.

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

В параграфе 1.5 рассматриваются фрагменты логик 3^ и без равенства (обозначаемые, соответственно, 3^ и

Л. Л. Максимовой [22] было доказано, что если суперинтуиционистская предикатная логика имеет интерполяционное свойство, то ее естественные расширения с равенством также его имеют. Д. Е. Тишков-ский [11] построил бесконечное семейство расширений интуиционист-

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

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

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

Следствие 8. Существует континуум промежуточных предикатных логик без равенства, не имеющих свойства Бета.

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

В параграфе 2.1 рассматривается исчисление ^.J{Л^v^_+^-J-}, которое получено из исчисления для интуиционистской логики предикатов, приведенного в [26, 27], отбрасыванием правил, содержащих дизъюнкцию и квантор существования. Для рассматриваемого исчисления доказывается теорема об элиминации сечения.

Комори в [19] определил некоторую модификацию стандартных шкал Крипке и доказал, что интуиционистская логика предикатов полна относительно этих шкал. В параграфе 2.2 доказана следующая

Теорема 9 (полноты).

Если формула ^ не содержит дизъюнкцию и квантор существования, то следующие условия эквивалентны:

1. Формула Г доказуема в интуиционистской логике предикатов.

2. Формула ^ выводима в исчислении .

3. Формула истинна во всех моделях Крипке с конечными предметными областями.

Для доказательства этой теоремы идея Комори перенесена на стандартные шкалы Крипке для предикатных суперинтуиционистских логик.

Следствие 9. Для любой предикатной логики Ь без равенства, содержащей интуиционистскую логику предикатов и содержащейся в интуиционистской логике конечных областей ,7^, фрагмент логики Ь без дизъюнкции и квантора существования совпадает с аналогичным фрагментом интуиционистской логики предикатов.

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

К. Шютте в работе [27] доказал, что интуиционистская логика предикатов имеет интерполяционное свойство, а также указал следующие факты:

1. Если в формулу не входил знак дизъюнкции, то он не входит и в интерполянт.

2. Если в формулу не входил квантор всеобщности, то он не входит и в интерполянт.

3. Если формула не содержала ни квантора всеобщности, ни квантора существования, то интерполянт также не содержит кванторов.

Однако в данном случае стандартное доказательство интерполяционного свойства не проходит.

Имеет место

Теорема 11. Исчисление ^./{^'"^'-'-^имеет свойство Бета.

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

Теорема 12. Фрагменты логик и без дизъюнкции и квантора существования имеют слабое интерполяционное свойство и свойство Бета.

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

Литература

[1] Гейтинг А. Интуиционизм. — М.: Мир, 1965.

[2] Гильберт Д., Бернайс П. Основания математики. Логические исчисления и формализация арифметики. — М.: Наука, 1979.

[3] Драгалин А. Г. Математический интуиционизм. Введение в теорию доказательств. — М.: Наука, 1979.

[4] Ершов Ю. Л., Палютин Е. А. Математическая логика. — М.: Наука, 1979.

[5] Клини С. К., Весли Р. Е. Основания интуиционистской математики. — М.: Наука, 1978.

[6] Максимова Л. Л. Теорема Крейга в суперинтуиционистских логиках и амальгамируемые многообразия псевдобулевых алгебр// Алгебра и логика. — 1977. — Т. 16, вып. 6. — С. 643-081.

[7] Максимова Л. Л. Интерполяция в суперинтуиционистских логиках предикатов с равенством// Алгебра и Логика. — 1997. — Т. 36, вып. 5. — С. 543-561.

[8] Новиков П. С. Конструктивная математическая логика с точки зрения классической. — М.: Наука, 1977.

[9] Расева Е., Сикорский Р. Математика метаматематики. — М.: Наука, 1972.

[10] Такеути Г. Теория доказательств. — М.: Мир, 1978.

[11] Тишковский Д. Е. Интерполяционное свойство и суперинтуиционистские предикатные логики// Сиб. мат. журнал. — 1998. — Т. 39, вып. 1. — С. 172-180.

[12] Шютте К. Интерполяционная теорема для интуиционистской логики предикатов// Математическая теория логического вывода. — М.: Наука, 1967. — С. 285-295.

[13] Шютте К. Полные системы модальной и интуиционистской логики //в кн. Фейс Р. Модальная логика. — М.: Наука, 1974. — С. 324— 421.

[14] Craig W. Three uses of the Herbrand — Gentzen theorem in relating model theory and proof theory// J. of Symbolic Logic. — 1957. — Vol. 22. — P. 269-285.

[15] Ehrenfeucht A. An application of games to the completeness problem for formalized theories// Fund. Math. — 1961. — Vol. 49, N 2. — P. 129-141.

[16] Gabbay D. Semantic proof of Craig's interpolation theorem for intuitionistic logic and its extensions. 1, 2// Logic Colloquium'69, ed. by R.O. Gandy, C.M.E.Yates, North-Holland, Amsterdam, 1971. — P. 391-410.

[17] Godel K. Eine Interpretation des intuitionistischen Aussagen-kalkiilus. — Ergebnisse math. Kolloquiums, 1933. — Vol. 4. — P. 39-40.

[18] Gurevich Yu. Toward logic tailored for computational complexity// Computation and proof theory: Lecture Notes in Math. — 1984. — Vol. 1104. — P. 175-216.

[19] Komori Yu. Predicate logics without the structure rules// Studia Logica. — 1986. — Vol. 45, N4. — P. 393-404.

[20] Kreisel G. Explicit definability in intuitionistic logic// J. of Symbolic Logic. — 1960. — Vol. 25, N 3. — P. 389-390.

[21] Mckinsey J., Tarski A. Some theorems about the sententional calculu of Lewis and Heyting// J. of Symbolic Logic. — 1948. — Vol. 13. — P. 1-15.

[22] Maksimova L. Interpolation in predicate logic with equality // 10th international congress of logic, methodology and philosophy of science: Abstracts. — Florence, Italy, 1995. — P. 154.

[23] Nagashima T. An extension of the Craig-Schutte interpolation theorem// Ann. Japan Assoc. Phil. Sci.. — 1966. — Vol. 3. — P. 12-18.

[21] Ono II. Craig's interpolation theorem for the intuitionistic logic and its extensions — A semantic approach// Studia Logica. — 1986. — Vol. 45, N 1. — P. 19-33.

[25] Ono H. Some problems in intermediate predicate logics// Rept. math, log. — 1987. — Vol. 21. — P. 55-67.

[26] Schiitte K. Schlu/Jweisen-Kalkiile der Pradikatenlogik// Mathematischc Annalr.n. — 1950. — Vol. 122. — P. 47-65.

[27] Schiitte K. Der Interpolationssatz der intuitionistischen Pradikatenlogik// Mathematische Annalen. — 1962. — Vol. 148, N 3. — P. 192200.

Работы автора по теме диссертации

[28] Шрайнер П. А. Отсутствие интерполяции в некоторых предикатных суперинтуиционистских логиках// Алгебра и логика. — 1996. — Т. 35, вып. 1. — С. 105-117.

[29] Шрайнер П. Л. Промежуточная предикатная логика без свойства Бета// Алгебра и логика. — 1998. — Т. 37, вып. 1. — С. 107-117.

[30] Шрайнер П. А. О фрагменте предикатной интуиционистской логики, полном относительно шкал Крипке с конечными областями. Препринт N 36, Издательство НИИ МИОО НГУ, 1998. — 21 с.

[31] Schreiner P. A. Failure of interpolation property and Beth's property in some predicate superintuitionistic logics// NSL'95: Abstracts. University of Irkutsk. — Irkutsk, 1995. — P. 74-75.

[32] Schreiner P. A. Some predicate superintuitionistic logics without interpolation property and Beth's property// Technical report Institute of Informatics, Warsaw University, "Logic, Algebra and Computer Sciencc" (Helena Rasiowa in memoriam). — Warsaw, 1996. — P. 68-69.

[33] Schreiner P. A. Continua of superintuitionistic predicate logics without Beth's property// Logic colloquium'98: Abstracts. — Prague, 1998. — P. 111.

Подписано в печать 4.11.98 Формат 60x84/16

Заказ №68 Усл.печ.л. 1.

Тираж 100

Отпечатано на полиграфическом участке издательства НИИ МИОО НГУ, 14Б(03)

630090, Новосибирск 90, ул. Пирогова 2



НОВОСИБИРСКИЙ ГОСУДАРСТВЕННЫЙ УНИВЕРСИТЕТ

На правах рукописи УДК 510.64

ШРАЙНЕР ПАВЕЛ АЛЕКСАНДРОВИЧ

ИНТЕРПОЛЯЦИЯ И ОПРЕДЕЛИМОСТЬ В ЛОГИКАХ

КОНЕЧНЫХ ОБЛАСТЕЙ

01.01.06 — математическая логика, алгебра и теория чисел

Диссертация на соискание ученой степени кандидата физико-математических наук

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

Новосибирск 1998

Содержание

Введение 3

1 Логики конечных областей 13

1.1 Отсутствие свойства Бета у интуиционистской логики конечных областей............................................13

1.2 Расширения логики не имеющие интерполяционного свойства......................................22

1.3 Отсутствие свойства Бета у логики Jjd....................29

1.4 Континуальные семейства суперинтуиционистских логик

без свойства Бета............................................38

1.5 Логики без равенства........................................42

2 Фрагмент интуиционистской логики конечных областей без дизъюнкции и квантора существования 51

2.1 Элиминация сечения в исчислении

2.2 Полнота исчисления относительно шкал Крип-

ке с конечными областями................. 72

2.3 Интерполяция и свойство Бета............... 77

Библиография 86

Введение

Теория неклассических логик — одна из важных областей современной логики. Особую роль среди многочисленных неклассических логик играет интуиционистская логика, возникшая в связи с критикой классической логики с позиций конструктивизма. На базе этой логики построены интуиционистская математика и конструктивная математика, основанные на конструктивном понимании существования математических объектов (см., например [1], [5]).

Формализация интуиционистской логики в виде исчисления, данная Гейтингом в 1930 году, подтолкнула интерес математиков к формулированию и изучению интуиционистских теорий с позиций классической математики. Основы такого подхода заложены в работах Геделя [17], Маккинси и Тарского [21], Новикова [8]. В данной работе мы также придерживаемся точки зрения классической математики при изучении неклассических логик.

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

Доказанная Янковым в 1968 году континуальность семейства суперинтуиционистских логик показывает невозможность эффективного описания всех суперинтуиционистских логик. Поэтому для изучения указанных семейств, как правило, выделяют классы логик, обладающих тем или иным свойством. К таким свойствам относятся, например, полнота по Крипке, разрешимость, дизъюнктивное, экзистенцио-нальное, интерполяционное свойство Крейга и свойство Бета.

Интерполяционная теорема для классической логики предикатов впервые была доказана В. Крейгом [14] в 1957 году. В 1962 году Шютте [27] доказал интерполяционную теорему для интуиционистской логики предикатов синтаксическим методом. Другие доказательства этого факта даны в работах Т.Нагашимы [23], Д. Габбая [16], X. Оно[24]. Д. Габбай в [16] представил семантическое доказательство интерполяционного свойства для некоторых расширений интуиционистской логики предикатов.

Л. Л. Максимова [6] доказала в 1977 году, что непротиворечивых пропозициональных суперинтуиционистских логик, имеющих интерполяционное свойство, только семь. Однако вопрос, поставленный X. Оно в [25], о том, какие предикатные суперинтуиционистские логики имеют интерполяционное свойство, остается открытым. Там же X. Оно полагает, что первым шагом к решению этой проблемы может явиться следующая задача: привести примеры предикатных логик, имеющих интерполяционное свойство. Естествен также и обратный вопрос, т. е. вопрос о примерах логик, не имеющих интерполяционного свойства. При этом можно отметить, что если предикатная логика имеет интерполяционное свойство, то ее пропозициональная часть тоже должна иметь его и, значит, все логики, имеющие интерполяционное свойство, должны содержаться в классе предикатных расширений вышеупомянутых семи пропозициональных логик.

В 1960 году Г. Крайзель [20] установил, что все пропозициональные суперинтуиционистские логики имеют свойство Бета. Для предикатных суперинтуиционистских логик такое утверждение не имеет места. Так, например, Ю. Гуревич в [18] доказал, что классическая логика конечных областей не обладает свойством Бета. Однако примеров логик без свойства Бета, промежуточных между интуиционистской и классической предикатными логиками, до настоящего времени не было известно.

Средствами интуиционистской логики свойство Бета можно вывести из интерполяционного свойства тем же способом, как это сделано в [14]. Отсюда получаем, что отсутствие у логики свойства Бета влечет отсутствие интерполяционного свойства.

Данная работа посвящена изучению интерполяционного свойства и свойства Бета для интуиционистской логики конечных областей с равенством Jf¿, характеризуемой всеми интуиционистскими шкалами Крипке, у которых все предметные области конечны, и близкой к ней логики характеризуемой всеми шкалами Крипке, у которых предметные области всех немаксимальных миров конечны. Поскольку справедливость указанных свойств существенно зависит от наличия в языке символа равенства (см., например, [11]), параллельно рассматривается также логика без равенства.

Установлено отсутствие свойства Бета, и, следовательно, интерполяционного свойства у логик и Логика является первым примером промежуточной логики без свойства Бета. Аналогичные результаты получены для фрагментов логик Jfd и без равенства.

Л.Л.Максимова доказала в [7], что существует континуум предикатных суперинтуиционистских логик с равенством, имеющих интерполяционное свойство, и, следовательно, свойство Бета.

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

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

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

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

Комори в [19] построил некоторую модификацию стандартных шкал Крипке и доказал, что интуиционистская логика предикатов полна относительно этих шкал. Мы перенесли его идею на стандартные шкалы Крипке для предикатных суперинтуиционистских логик.

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

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

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

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

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

Основные результаты диссертации:

1. Установлено отсутствие свойства Бета и интерполяционного свойства у интуиционистской логики конечных областей. Данный результат верен как для логики с равенством, так и для логики без равенства.

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

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

3. Доказано, что фрагмент интуиционистской логики конечных областей, состоящий из формул первого порядка, не содержащих дизъюнкции и квантора существования, совпадает с аналогичным фрагментом интуиционистской логики предикатов. Этот фрагмент имеет слабый вариант интерполяционного свойства и свойства Бета.

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

Основные результаты, полученные в диссертации, докладывались

на:

• заседаниях семинаров "Неклассические логики" и "Алгебра и Логика" кафедры алгебры и математической логики механико-математического факультета НГУ,

• русско-японском коллоквиуме по нестандартным логикам и логическим аспектам информатики ЫБЬ'Эб (Иркутск, 1995),

• международной конференции "Логика, алгебра и информатика", посвященной памяти Елены Расевой (Варшава, 1996),

• международных конференциях "Мальцевские чтения" (Новосибирск, 1996,1998),

• международных научных студенческих конференциях " Студент и научно-технический прогресс" (Новосибирск, 1993,1995,1996),

• логическом коллоквиуме ЬС'98 (Прага, 1998),

• конференциях профессорско-преподавательского состава НГПУ (Новосибирск, 1994,1995,1996,1997,1998).

Результаты диссертации опубликованы в шести работах автора [28]-[34].

Приведем более подробные формулировки результатов работы.

В главе 1 изучается интерполяционное свойство и свойство Бета для логики конечных областей с равенством Jfd и близкой к ней логики а также для их фрагментов без равенства и некоторых расширений.

Предложение Ф(Р) неявно определяет в логике Ь п-местный предикат Р, если в логике Ь доказуема формула

(Ф (Р) &Ф (Р')) V®! • • • \/хп (Р (Х1, . . . , О О Р' (хъ . . . , Хп)) ,

Р/ V

— новый п-местныи предикатный символ.

Предложение Ф(Р) явно определяет п-местный предикат Р в логике

если существует формула С(х\,... , хп) такая, что все предикатные символы формулы С содержатся во множестве предикатных символов предложения Ф(Р), отличных от Р, и в логике Ь доказуема формула

Ф(Р) ->• ... \/жп(Р(жь ... , хп) С(х1,... , хп)).

Логика Ь имеет свойство Бета, если предложение, неявно определяющее предикат в логике Ь, определяет его в логике Ь явно.

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

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

Логика Ь имеет интерполяционное свойство, если для всякой формулы (А —5), принадлежащей логике Ь, существует формула С такая, что формулы (А —у С) и (С В) принадлежат логике X, причем в формулу С входят лишь те предикатные символы и свободные предметные переменные, которые входят и в А, и в В.

Однако нам понадобится понятие слабого интерполяционного свойства:

Логика Ь имеет слабое интерполяционное свойство, если для всякой формулы (А —В), принадлежащей логике существует формула С такая, что формулы (А —^ С) и (С —» 5) принадлежат логике Ь, причем в формулу С входят лишь те предикатные символы, которые входят и в А, и в В.

Очевидно, что наличие у логики интерполяционного свойства влечет наличие слабого интерполяционного свойства.

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

Лемма 2. Если логика обладает слабым интерполяционным свойством, то она обладает свойством Бета.

Из отсутствия у интуиционистской логики конечных областей 3^^ свойства Бета, в виду леммы 2, получается

Следствие 1. Логика не имеет ни слабого, ни сильного интерполяционного свойства.

Построена в явном виде формула, у которой нет интерполянта в логике Зfd■

Имеет место

Следствие 2. Если логика Ь содержится в классической логике конечных областей и содержит интуиционистскую логику конечных областей 3^^ то Ь не имеет ни слабого, ни сильного интерполяционного свойства, ни свойства Бета.

Там же доказана

Теорема 2. Существует континуум предикатных суперинтуиционистских логик с равенством, не имеющих свойства Бета.

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

В параграфе 1.3 показано отсутствие свойства Бета у логики <7^, характеризуемой всеми шкалами Крипке, у которых все предметные области всех немаксимальных миров конечны. Логика Jjd является первым примером промежуточной логики без свойства Бета. Контрпример к свойству Бета для логики построен в явном виде.

Обозначим через «7^ логику, характеризующуюся классом шкал Крипке, основанных на натуральном ряде Л/", с конечными предметными областями. Тогда справедливо

Следствие 4. Если логика Ь содержится в логике «7^ и содержит логику Jfd) то Ь не имеет ни интерполяционного свойства, ни свойства Бета.

Л. Л. Максимова доказала в [7], что существует континуум предикатных суперинтуиционистских логик с равенством, имеющих интерполяционное свойство и, следовательно, свойство Бета.

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

В параграфе 1.5 рассматриваются фрагменты логик Jfc^ и Jjd без равенства (обозначаемые, соответственно, «7^ и ).

Л. Л. Максимовой [22] было доказано, что если суперинтуиционистская предикатная логика имеет интерполяционное свойство, то ее естественные расширения с равенством также его имеют. Д. Е. Тишков-ский [11] построил бесконечное семейство расширений интуиционистской логики предикатов с равенством, обладающих интерполяционным свойством, чьи фрагменты без равенства не имеют указанного свойства.

В данном параграфе доказано, что логики 3^ и 3*^ не имеют свойства Бета и, следовательно, не имеют интерполяционного свойства. Получены следующие два следствия.

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

Следствие 8. Существует континуум промежуточных предикатных логик без равенства, не имеющих свойства Бета.

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