Интерполяция и определимость в логиках конечных областей

Теория неклассических логик — одна из важных областей современной логики. Особую роль среди многочисленных неклассических логик играет интуиционистская логика, возникшая в связи с критикой классической логики с позиций конструктивизма. На базе этой логики построены интуиционистская математика и конструктивная математика, основанные на конструктивном понимании существования математических объектов (см., например [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. Существует континуум промежуточных предикатных логик без равенства, не имеющих свойства Бета.

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

В параграфе 2.1 рассматривается исчисление? которое получено из исчисления Кз для интуиционистской логики предикатов, приведенного в [26, 27], отбрасыванием правил, содержащих дизъюнкцию и квантор существования. Для рассматриваемого исчисления доказывается теорема об элиминации сечения.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Имеет место.

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

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

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

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

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

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

3. Драгалин А. Г. Математический интуиционизм.

Введение

в теорию доказательств. — М.: Наука, 1979. — 256 с.

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

5. Клини С. К., Весли P.E. Основания интуиционистской математики. — М.: Наука, 1978. — 271 с.

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

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

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

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

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

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, N 4. — 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.

24. Ono H. 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/3weisen-Kalkiile der Pradikatenlogik// Mathematische Annalen. — 1950. — Vol. 122. — P. 47−65.

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

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. Continua of superintuitionistic predicate logics without Beth’s property// Logic colloquium'98: Abstracts. — Prague, 1998. — P. 111. ~.H //iL.