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

• Шрайнер, Павел Александрович
• кандидат физико-математических наук
• 1998

Оглавление диссертации кандидат физико-математических наук Шрайнер, Павел Александрович

Содержание

Введение

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

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

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

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

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

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

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

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

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

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

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

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

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

Введение диссертации (часть автореферата) на тему «Интерполяция и определимость в логиках конечных областей»

Введение

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

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

Интерполяционное свойство для интуиционистской логики предикатов первым доказал К. Шютте [27] синтаксическим методом. Другие доказательства даны в работах Т.Нагашимы [23], Д. Габбая [16], X. Оно[24] . Д. Габбай в [16] дал семантическое доказательство интерполяционного свойства для логик НС^ + Р{х) -н- -1 -*\/хР(х)), НС} + ^Р\/^Р,Н + ^Р\/^Р+(ух^Р(х) -л->\/хР(х)), где Яф — интуиционистская логика предикатов. Ю.Гуревич [18] доказал отсутствие интерполяционного свойства и свойства Бета у классической логики конечных областей с равенством. В данной главе изучается интерполяционное свойство и свойство Бета для интуиционистской логики конечных областей и близких ей логик.

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

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

Приведем необходимые определения и обозначения.

Символ -Ф=>- используем вместо слов "тогда и только тогда".

Суперинтуиционистской предикатной логикой(см. [25]) называем множество формул, содержащее аксиомы интуиционистской логики предикатов и замкнутое относительно правил подстановки, обобщения и модус поненс. Промежуточной предикатной логикой называем суперинтуиционистскую предикатную логику, содержащуюся в классической логике предикатов. Эти определения естественным образом переносятся на пропозициональные логики.

Интуиционистская шкала Крипке —это тройка (РУ, <, {-¿ЛЛ^еи^Ь где Ш — непустое множество миров, И у, — множество предметных переменных мира и) (предметная область мира «;), а < — это частичный порядок на множестве IV. На шкалах Крипке должно быть выполнено условие монотонности областей: если и> < V, то предметная область И и, должна содержаться в предметной области .

Интуиционистская модель Крипке — это четверка (Ж, <, (=)> где тр0]йка (И7, <, {¿Ли}™^) — интуиционистская шкала Крипке, |= — отношение истинности на мирах. На моделях должно быть выполнено условие монотонности предикатов: если и> < -у, <21,... ,ап из предметной области Дд, Р — п-местный предикатный символ, то из ио |= Р(а,1,... , ап) следует V |= Р(ах,... , ап).

Имеет место

Лемма о монотонности. Если ги < v, А — произвольная формула, то т \= А влечет V \= А.

Отношение истинности на формулах определяется следующим образом:

и) |= А&В V) |= А и V) В] V) \= АУ В га |= А или w \= В;

и} \= А ^ В (для всех V > т){у (= А влечет V (= В);

ии [= -1А <£=>- (для всех V > А);

и) \= МхА{х) (для всех г> > га)(для всех а Е Д,) V |= А(а);

и> |= ЗхА(х) существует а из И у, такой, что и) |= А(а);

ии \= а = Ь а, Ь Е и а совпадает с Ь.

Мир, являющийся максимальным в шкале Крипке, будем называть финальным. Мир, не являющийся финальным, называем нефиналъным.

Логика Ь характеризуется классом шкал Крипке К, если все формулы из логики Ь общезначимы во всех шкалах Крипке из класса К, а любая формула, не принадлежащая логике Ь, опровергается на некоторой шкале Крипке из класса К. Понятие кванторной глубины формулы Ф (д.с!.(Ф)) определим следующим образом: д.с1.(Ф) = 0, если Ф — бескванторная формула;

я.а.(УжФ) = я.а.(ЭжФ) = я.а.(Ф) +1;

д.с!.(Ф) = тах^.сЦФх),... , д.с1.(Ф&)), если Ф — булева комбинация формул Фь.. . ,ФА.

Формула Ф находится в нормальной форме, если Ф имеет вид (д^) ... (дпжта)Ф(жь ... ,жп), где д» £ {У,3}, Ф — бескванторная формула.

Для построения контрпримеров к интерполяционному свойству и свойству Бета введем некоторые сокращения и обозначения: х < у = х < у У х = у] х -< у = х < у&\/г(г < х V у < г)]

а = Зх\/у(х < у)&\/х{~< ж)&(3у(х < у) —>• Э2:(ж г))&\/у((х < У V у < ж)&(ж <уУ < у))&,(х — уУ -*{х = у))&\/г(х < у&су < г ж < г)));

/3(Р) = Уж((Р(ж) V -.Р(ж))&(Уг/(ж < у) ^ ^Р{х))Шу{х < у ^ (Р(у) о п?(х)))).

Заметим, что если М = (ЦТ, <, [=} — модель Крипке, V —

произвольный мир из множества IV, в мире V истинно предложение а, у' £ V < у', то:

отношение < будет на Д/ иррефлексивным, транзитивным; для любых элементов а^ а,2 из предметной области Д/ либо а\ < аг, либо аг < ах, либо ах = 02;

для любых элементов <21,0.2 из предметной области Д/ либо а\ < а2 в Д/, либо ни в каком мире ии' из < т') не будет выполняться

а\ < а2-

В предметной области Д существует наименьший элемент (остающийся наименьшим во всех мирах IV из таких, что V < ги). Если для элемента а в предметной области Д/, где V < V1, имеется элемент Ь

такой, что а < Ь, то в предметной области найдется элемент а' ("непосредственный последователь элемента а") такой, что а -< апричем этот последователь в предметной области и в предметных областях всех последующих миров один и тот же.

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

(Ф (Р) &Ф (Р')) V®!... (Р (хи ... , хп) Р' (хи ... , хп)),

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

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

, Хп) •<->

С(жь ... ,жп)).

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

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

Теорема 1. Логика Jf¿ не имеет свойства Бета.

Для доказательства этой теоремы нам понадобится

Предложение 1. Пусть М = {]¥, <, {А^}«,^, |=) — модель Крипке, у которой все предметные области нефиналъных миров конечны, IV — произвольный нефиналъный мир из множества ТУ такой, что т \= а. Тогда все элементы предметной области И у, могут быть пронумерованы натуральными числами в порядке возрастания (Ж1 < Х2 < ... < так, что если ги' Е ]¥, т < ио', то в предметной области Иу,/ также выполняется х\ < хч < ... < Хк и для любого элемента х из предметной области не принадлежащего предметной области ВЪ1), имеет место х& <х.

Доказательство предложения 1.

В предметной области Бу, и в предметных областях всех последующих миров существует наименьший элемент, который занумеруем числом 1. Если мощность предметной области больше 1, то в предметной области Иу, существует элемент ж, отличный от элемента х\. Так как х\ — наименьший элемент, то х\ < ж, а, следовательно, существует и непосредственный последователь элемента х\, его занумеруем числом 2. Заметим, что для любого элемента х из предметной области И^ (ад < ад'), отличного от элемента Х{ (г = 1,2), имеет место Х{ < х. Таким образом, если мощность предметной области < 2, то предложение 1 имеет место.

Предположим, что для любого мира ии Е , у которого мощность предметной области не больше чем к (к > 2), и ад |= ск, мы умеем нумеровать элементы так, что х\ < х^ < ... , причем эта нумерация сохраняется на предметных областях последующих миров и для любого элемента х из предметной области Д/ (ад < ад'), отличного от всех а^ (г = 1,... , к), выполняется < х.

Возьмем произвольный мир ад из множества Ж такой, что мощность предметной области Vш больше чем к. Тогда по предположению индукции первые к элементов предметной области Иги можно пронумеровать, причем эта нумерация сохраняется на предметных областях последующих миров и для любого элемента х из предметной области Д/ (ад < ад'), отличного от всех Х{ (г = 1,... ,к), имеет место Х{ < х. Так как мощность предметной области не меньше чем к , то в предметной области существует элемент ж, отличный от всех Х{ (г = 1,... , к) и, следовательно, х& < х. Значит, в предметной области существует непосредственный последователь для его занумеруем числом к + 1. Во всех последующих мирах непосредственный последователь для один и тот же и, следовательно, нумерация сохраняется; для любого элемента а из предметной области (ад < ад') либо а < Хк, либо < а (из определения непосредственного последователя). В первом случае по предположению индукции элемент а совпадает с одним из Х{ (г £ {1,... ,&})• Поэтому если а отличен от всех Х{ (г = 1,... , к + 1), то Х{ < а. Таким образом мы пронумеруем все элементы конечных предметных областей. ■

Лемма 1. Предложение а&/3(Р) неявно определяет предикат Р в логике Jfc|l.

доказательство, Заметим, что если в мире и> выполняется предложение а и мощность предметной области конечна, то предложение (3(Р) определяет, что Р не содержит наименьшего элемента предметной области и непосредственный последователь элемента х принадлежит Р тогда и только тогда, когда х не принадлежит Р, т. е. {х\и) \= Р(х)} = | к— четное}. Таким образом, предложение се&/3(Р) неявно определяет предикат Р в логике Jf¿. Ш

В работе [18] доказана следующая

Лемма. 1. Пусть Ф — предложение сигнатуры {<}, д.сЦФ) = п, М 1; Ш.2 — конечные линейные порядки мощности не меньше чем 2п. Тогда М\ удовлетворяет Ф тогда и только тогда, когда М2 удовлетворяет Ф.

2. Не существует предложения Ф сигнатуры {<} такого, что произвольный конечный линейный порядок М удовлетворяет Ф тогда и только тогда, когда мощность М четная.

3. Не существует формулы С(х) сигнатуры {<} такой, что если М конечный порядок а\ < ... < ап, то {х\М |=С(х)} =

| к — четное}.

Доказательство теоремы 1. Допустим, что логика Jf¿ имеет свойство Бета. Как было замечено в лемме 1, предложение ск&/3(Р) определяет неявно предикат Р в логике Jf¿. Тогда предложение «&/3(Р) должно определять предикат Р в логике явно и, значит, существует формула С(х) сигнатуры {<} такая, что в логике доказуема формула а&(3(Р) —\/ж(Р(ж) -н- С(х)). Возьмем любой конечный линейный порядок М, Р = {х | х — четное}. Это модель логики Jf¿. Тогда в М истинны формулы а и (3(Р). В силу истинности формулы се&/3 (Р) в М, множество элементов М, на которых формула С (ж) истинна, совпадает со множеством четных элементов

этой области, что противоречит пункту 3 вышеприведенной леммы из [18]. Следовательно, логика Jf¿ не имеет свойства Бета. ■

Введем некоторые определения.

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

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

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

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

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

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

(Ф (Р) &Ф (Р')) V®! • • • Чхп (Р(хи... ,хП)^Р'(х!,..., хп)) ,

где Р' — новый п-местный предикатный символ. Следовательно, в логике Ь доказуема формула

(Ф(Р)&Ф(Р')) №ь • • • , *п) ++ Р'(ХЬ . . . , О).

Отсюда следует, что в логике Ь доказуема формула

(Ф (Р) &ф (Р')) (Р (хи ... , О Р' (хи ... , хп)).

Следовательно, в логике Ь доказуема формула

(Ф (Р) кР (хъ ... , хп)) (Ф (Р') ^Р'{х!,..., хп)).

Если логика Ь имеет слабое интерполяционное свойство, то для формулы

(Ф (Р) кР (хи . . . , хп)) (ф (Р') ^Р'(х!,..., хп))

должен существовать интерполянт С. Причем, в формулу С входят лишь те предикатные символы, которые входят и в формулу Ф (Р) кР (#1,... , жп), и в формулу Ф (Р') —> Р' (ж 1,... , жте), то есть все предикатные символы формулы С содержатся во множестве предикатных символов предложения Ф(Р), отличных от Р. При этом в логике Ь доказуемы формулы (Ф (Р) кР (жь ... , жп)) ->- С и С ->• (Ф (Р') Р'(ЖЬ... ,!„)).

Если формула С содержит свободные переменные у\,... ,ут не входящие в множество {жх,... , жп}, свяжем их квантором всеобщности, применив правило введения квантора всеобщности справа и слева, к формулам (Ф (Р) кР (жх,... , жп)) —> С и С —> (Ф (Р') —>•' Р' (ж1,... , жп)) соответственно. Применение правила введения квантора всеобщности справа возможно, так как в формулу Ф (Р) кР (жх,... , хп) входят свободно только переменные из множества {ж15...,жп}. Получим, что в логике доказуемы формулы (Ф (Р) кР (жх,... , жп)) —>■ С'(жх,... , хп) и С'(хх,...,жп) -)> (Ф(Р') Р'(жх,... ,жп)), где С'(хи... ,хп) = \/у1... УутС(жх,... , жп, ух? • • • ) 2/т)- При этом все свободные переменные формулы С' содержатся во множестве {жх,... , жп}.

Отсюда следует, что в логике Ь доказуема формула Ф (Р) —» (Р(жх,... , хп) С'(жх,... ,жп)). Подставляя Р вместо Р', получаем, что в логике Ь доказуема формула Ф (Р) —»■ (С'(жх,... ,жп) —>■ Р(жх,... ,жп)). Следовательно, формула Ф (Р) —» (Р(жх,... ,жп) О С"(жх,... , жп)) доказуема в логике Ь.

Применив перестановку, введение квантора всеобщности слева, перестановку, получаем, что в логике Ь доказуема формула Ф (Р) —> \/жх... \/жп(Р(жх,... , хп) С'(Жх, ... , хп)).

Получили, что предложение Ф(Р) явно определяет п-местный

предикат Р в логике Ь. Ш

Список литературы диссертационного исследования кандидат физико-математических наук Шрайнер, Павел Александрович, 1998 год

Литература

[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. — С. 324421.

[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.

[2.0] 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. 192200.

[28] Шрайнер П. А., Ганусова О. Г. Автоматическая проверка наличия интерполяционного свойства Крейга у некоторых суперинтуиционистских пропозициональных логик// Материалы 34 международной научной студенческой конференции. Математика. Новосиб. ун-т. — Новосибирск, 1996. — С. 18-19.

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

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

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

[32] 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.

[33] 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 Science" (Helena Rasiowa in memoriam). — Warsaw, 1996. — P. 68-69.

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

H //

■iL