Введение к работе
Актуальность темы. Теория неклассических логик — одна из важных областей современной логики. Особую роль среди многочисленных неклассических логик играет интуиционистская логика, возникшая в связи с критикой классической логики с позиций конструктивизма. На базе этой логики построены интуиционистская математика и конструктивная математика, основанные на конструктивном понимании существования математических объектов (см., например [1], [5]).
Формализация интуиционистской логики в виде исчисления, данная Гейтингом в 1930 году, подтолкнула интерес математиков к формулированию и изучению интуиционистских теорий с позиций классической математики. Основы такого подхода заложены в работах Геделя [17], Маккинси и Тарского [21], Новикова [8]. В данной работе мы также придерживаемся точки зрения классической математики при изучении неклассичсских логик.
Позднее возникли и изучались расширения интуиционистской логики. Классы формул, содержащие интуиционистское исчисление и замкнутые относительно выводимости, получили название суперинтуиционистских логик.
Доказанная Янковым в 1968 году континуальность семейства суперинтуиционистских логик показывает невозможность эффективного описания всех суперинтуиционистских логик. Поэтому для изучения указанных семейств, как правило, выделяют классы логик, обладающих тем или иным свойством. К таким свойствам относятся, например, полнота по Крипке, разрешимость, дизъюнктивное, экзистенцио-нальное, интерполяционное свойство Крейга и свойство Бета.
Интерполяционная теорема для классической логики предикатов впервые была доказана В. Крейгом [14] в 1957 году. В 1962 году Шютте [27] доказал интерполяционную теорему для интуиционистской логики предикатов синтаксическим методом. Другие доказательства этого факта даны в работах Т. Нагашимы [23], Д. Габбая [16], X. Оно[24]. Д. Габбай в [10] представил семантическое доказательство интерполяционного свойства для некоторых расширений интуиционистской логики предикатов.
Л.Л.Максимова [6] доказала в 1977 году, что непротиворечивых пропозициональных суперинтуиционистских логик, имеющих интерполяционное свойство, только семь. Однако вопрос, поставленный X. Оно в [25], о том, какие предикатные суперинтуиционистские логики имеют интерполяционное свойство, остается открытым. Там же X. Оно полагает, что первым шагом к решению этой проблемы может явиться следующая задача: привести примеры предикатных логик, имеющих интерполяционное свойство. Естествен также и обратный вопрос, т. е. вопрос о примерах логик, не имеющих интерполяционного свойства. При этом можпо отметить, что если предикатная логика имеет интерполяционное свойство, то ее пропозициональная часть тоже должна иметь его и, значит, все логики, имеющие интерполяционное свойство, должны содержаться в классе предикатных расширений вышеупомянутых семи пропозициональных логик.
В 1960 году Г. Крайзель [20] установил, что все пропозициональные суперинтуиционистские логики имеют свойство Бета. Для предикатных супериптуиционистских логик такое утверждение не имеет места. Так, например, Ю. Гуревич в [18] доказал, что классическая логика конечных областей не обладает свойством Бета. Однако примеров логик без свойства Бета, промежуточных между интуиционистской и классической предикатными логиками, до настоящего времени не было известно.
Средствами интуиционистской логики свойство Бета можно вывести из интерполяционного свойства тем же способом, как это сделано в [14]. Отсюда получаем, что отсутствие у логики свойства Бета влечет отсутствие интерполяционного свойства.
Данная работа посвящена изучению интерполяционного свойства и свойства Бета для интуиционистской логики конечных областей с равенством Jfdi характеризуемой всеми интуиционистскими шкалами Крипке, у которых все предметные области конечны, и близкой к ней логики J*id, характеризуемой всеми шкалами Крипке, у которых предметные области всех немаксимальных миров конечны. Поскольку справедливость указанных свойств существенно зависит от наличия в языке символа равенства (см., например, [11]), параллельно рассматривается также логика без равенства. '
Установлено отсутствие свойства Бета, и, следовательно, интерполяционного свойства у логик Jjd и Jyd. Логика Jjd является первым примером промежуточной логики без свойства Бета. Аналогичные результаты получены для фрагментов логик Jfj и JJd без равенства.
Л.Л.Максимова доказала в [7], что существует континуум предикатных суперинтуипионистских логик с равенством, имеющих интерполяционное свойство, и, следовательно, свойство Бета.
В данной работе доказано, что любая промежуточная пропозициональная логика имеет континуум предикатных расширений с равенством, не имеющих свойства Бета и не содержащихся в классической логике предикатов. Доказано также, что любая пропозициональная логика, содержащаяся в логике Даммета, имеет континуум предикатных расширений с равенством, промежуточных между интуиционистской и классической логиками предикатов и не имеющих свойства Бета.
Доказано существование континуума предикатных логик без равенства, не имеющих свойства Бета. При этом построен континуум таких логик, не содержащихся в классической логике предикатов, и континуум логик, промежуточных между интуиционистской и классической логиками.
Хорошо известно, что классическая логика предикатов не является полной относительно моделей с конечными предметными областями. Как следует, например, из первого параграфа первой главы диссертации, интуиционистская логика предикатов также не является полной относительно шкал Крипке с конечными предметными областями. Более того, при переходе к моделям с конечными предметными областями классическая и интуиционистская логики теряют многие "хорошие" свойства, такие, например, как интерполяционное свойство и свойство определимости по Бету.
Заметим, что многие приложения логики, такие, например, как Пролог или реляционные языки запросов баз данных, имеют дело с конечными структурами.
Комори в [19] построил некоторую модификацию стандартных шкал Крипке и доказал, что интуиционистская логика предикатов полна относительно этих шкал. Мы перенесли его идею на стандартные шкалы Крипке для предикатных суперинтуиционистских логик.
В данной работе доказано, что фрагмент интуиционистской логики конечных областей, состоящий из формул первого порядка, не содержащих дизъюнкции и квантора существования, совпадает с аналогичным фрагментом интуиционистской логики предикатов. Получено также наличие у этого фрагмента слабого варианта интерполяционного свойства и свойства Бета.
Можно отметить, что данный результат заведомо не может быть перенесен на случай классической логики предикатов в связи с тем, что фрагмент классической логики предикатов в языке без дизъюнкции и квантора существования эквивалентен классической логике в полном языке, так как в этой логике дизъюнкция и квантор существования выразимы через остальные связки.
Цель работы. Изучить интерполяционное свойство и свойство Бета для предикатной логики конечных областей Jfj, характеризуемой всеми интуиционистскими шкалами Крипке, у которых все предметные области конечны, а также для близких к ней логик.
Исследовать вопрос о числе и расположении предикатных суперинтуиционистских логик, не имеющих свойства Бета.
Методы исследования. В диссертации использованы семантические методы теории неклассических логик, теории моделей классической и интуиционистской логик первого порядка и синтаксические методы теории доказательств.
Научная новизна рабохы. Все результаты диссертационного исследования являются новыми и снабжены подробными доказательствами.
Основные результаты диссертации.
-
Установлено отсутствие свойства Бета и интерполяционного свойства у интуиционистской логики конечных областей. Данный результат верен как для логики с равенством, так и для логики без равенства.
-
Построен первый пример логики, промежуточной между интуиционистской и классической логиками предикатов и не имеющей свойства Бета. Доказано, что для любой пропозициональной су-перинтуиционистской логики существует континуум предикатных
расширений, не содержащихся в классической логике предикатов и не имеющих ни свойства Бета, ни интерполяционного свойства. Для любой пропозициональной логики, содержащейся в логике Даммета, доказано существование континуума предикатных расширений, промежуточных между интуиционистской и классической логиками предикатов и не имеющих ни свойства Бета, ни интерполяционного свойства.
3. Доказано, что фрагмент интуиционистской логики конечных областей, состоящий из формул первого порядка, не содержащих дизъюнкции и квантора существования, совпадает с аналогичным фрагментом интуиционистской логики предикатов. Этот фрагмент имеет слабый вариант интерполяционного свойства и свойства Бета.
Теоретическая и практическая ценность. Работа носит теоретический характер. Ее методы и результаты могут использоваться специалистами в области неклассических логик и теоретической информатики, для чтения лекций и спецкурсов в Московском, Новосибирском, Красноярском и др. госуниверситетах.
Апробация работы. Основные результаты, полученные в диссертации, докладывались'на:
заседаниях семинаров "Неклассические логики" и "Алгебра и
Логика" кафедры алгебры и математической логики механико-
математического факультета НГУ,
в русско-японском коллоквиуме по нестандартным логикам и логическим аспектам информатики NSL'95 (Иркутск, 1995),
международной конференции "Логика, алгебра и информатика", посвященной памяти Елены Расевой (Варшава, 1996),
международных конференциях "Мальцевские чтения" (Новосибирск, 1996,1998),
международных научных студенческих конференциях " Студент и научно-технический прогресс" (Новосибирск, 1993,1995,1996),
логическом коллоквиуме LC98 (Прага, 1998),
конференциях профессорско-преподавательского состава НГПУ (Новосибирск, 1994,1995,1996,1997,1998).
Публикации. Результаты диссертации опубликованы в шести работах автора [28]-[33].
Структура и объем работы. Диссертация состоит из введения и двух глав, разбитых на 8 параграфов. Список литературы содержит 34 наименования. Общий объем диссертации 89 страниц.