Введение к работе
Актуальность темы. Предикатным языком будем называть язык первого порядка, содержащий счетный набор предикатных символов любой валентности, без функциональных символов, констант и равенства. Исчисление предикатов в этом языке будем обозначать PC
Пусть фиксирована теория Т первого порядка. Интерпретацией предикатного языка в язык теории Т назовем всякое отображение /, сопоставляющее каждому предикатному символу некоторую формулу в языке теории Г с тем же набором свободных переменных, причем / коммутирует с булевыми связками, кванторами и операцией замены переменных. Логикой С(Т) теории Т называется множество предикатных формул ip, таких что при любой интерпретации формула f(
Можно также говорить о логике модели или класса моделей, понимая под этим логику элементарной теории этой модели или класса моделей соответственно.
Согласно теореме Геделя о полноте, множество предикатных формул, истинных во всех моделях при любой интерпретации совпадает с PC, поэтому для классических теорий первого порядка логика С(Т) содержит исчисление предикатов PC.
Логика С(Т) может совпадать с исчислением предикатов либо быть собственным расширением PC. Рассмотрим, например, интерпретации предикатного языка, при которых предикатные символы интерпретируются отношениями на множестве натуральных чисел, выразимыми в арифметике. Как следует из теоремы Гильберта — Бернайса (см. [1], глава IV), такое ограничение не приведет к появлению новых общезначимых схем: множество формул, истинных при любой интерпретации из указанного класса совпадает с PC. Однако если при интерпретации предикатных символов ограничиться только отношениями, выразимыми в терминах порядка на множестве N натуральных чисел, или другим более ограниченным набором, получим новую предикатную логику, являющуюся собственным расширением
'Hilbert D., Bernays P. Grundlagen der Mathematik, II. — New York, Berlin, Heidelberg, Токіо: Springer-Verlag, 1968.
2Rabin M.O. Decidable Theories// Handbook of Mathematical Logic J. Barwise (ed.). — North-Holland Publishing Company, 1977.
PC. Это можно показать, используя тот факт, что любое определимое в (N, <) множество либо является конечным, либо имеет конечное дополнение [2].
Таким образом, предикатная логика теории Т описывает логические законы, действующие в рамках теории Т.
Аналогичная конструкция рассматривалась раньше в различных работах. Так, В. А. Лифшиц в [3] дает следующее определение: предикатная формула ip называется Т-общезначимой, если ее любая интерпретация выводима в Т; классическая теория Т является геделев-ской относительно классического исчисления предикатов PC, если каждая Т-общезначимая предикатная формула доказуема в PC. Другими словами, Т — геделевская теория, если С(Т) = PC. Им было замечено, что каждая геделевская теория неразрешима, а также доказано, что арифметика Пеано РА и некоторые ее подтеории являются геделевскими теориями.
Предикатные логики расширении классической арифметики рассматривались В.А.Варданяном в [4]. В его исследованиях логика С(Т) арифметической теории Т возникла как безмодальный фрагмент предикатной логики доказуемости теории Т. Им было показано, что для любой степени неразрешимости d существует расширение Т арифметики Пеано РА, такое что степени неразрешимости Г и С(Т) равны d.
Особо важное значение вопрос изучения логик теорий имеет в
3Лифшпц В.А. Дедуктивная общезначимость и классы сведения// Записки научных семинаров ЛОМИ им. В.А. Стеклова АН СССР. — 1967. — Т. 4. — С. 69-77.
4Варданян В.А. Предикатная логика доказуемости без доказуемости// Интенсиональные логики и логическая структура теории. — Тбилиси, 1988. — С. 65-69.
5Плнско В.Е. Некоторые варианты понятия реализуемости для предикатных формул// Изв. АН СССР. Сер. Матем. — 1978. — Т. 42, N 3. — С. 636-653.
6Плиско В.Е. Конструктивная формализация теоремы Теннен-баума и ее применения// Мат. заметки. — 1990. — Т. 48, вып. 3. — С. 108-118.
7Плиско В.Е. Об арифметической сложности некоторых предикатных логик// Мат. заметки. — 1992. — Т. 52, вып. 1. — С. 94-104.
контексте конструктивной математики. Свойства предикатных логик конструктивных арифметических теорий подробно были изучены В.Е.Плиско в [5,6,7]. В частности, им было доказано, что для любой конструктивной арифметической теории Т имеет место 1-своднмость множества геделевых номеров формул теории Г к множеству геделевых номеров Т-общезначнмых формул, и что структура конструктивных арифметических теорий с отношением включения С изоморфна структуре предикатных логик этих теорий с отношением с.
Определение предикатной логики теории первого порядка является частным случаем более общего понятия, введенного С. Н. Арте-мовым и Ф. Монтагна в [8]. Пусть заданы теория Г, язык L н некоторый класс J- интерпретаций языка L в язык теории Т. Тогда логика С(Т,L, J-) есть по определению множество формул языка L, выводимых в теории Т при любой интерпретации из класса Т. Выбирая в качестве L различные расширения пропозиционального или предикатного языков одноместными или двуместными модальностями, при соответствующем выборе класса интерпретаций Т можно получить в качестве С{Т,Ь,Т) пропозициональные н предикатные логики доказуемости, интерпретируемости, консервативности и другие (см., например, [9,10,11]), а также так называемые доказуемост-ные расширения арифметических теорий, изученные в [8]. Если же в качестве L взять предикатный язык, а в качестве Т — класс всех его интерпретаций в язык теории Т, то (Т, L, Т) совпадает с предикатной логикой С(Т), которая и является объектом нашего изучения.
Цель работы — найти логики классических теории первого порядка, ответить на вопрос о разрешимости этих логик и существовании конечной аксиоматизации для них, а также описать отношение включения между ними.
8Artemov S., Montagna F. On first-order theories with provability operator// Journal of Symbolic Logic. — 1994. — Vol. 59, 4. — P. 1139-1153.
9Артёмов C.H. Арифметически полные модальные теории// "Семиотика и информатика". — М. 1979-1980 — Вып. 14. — С. 115-133.
10Boolos G. The Unprovability of Consistensy; An Essay in Modal Logic. — Cambridge: Cambridge University Press, 1979.
"Solovay R. Provability interpretations of modal logic// Israel J. Math. — 1976. — V.25. — P. 287-304.
Методы исследования. В диссертации использована техника интерпретируемости теорий первого порядка, аппарат теории моделей, а также разработанные автором методы доказательства включения предикатных логик теорий первого порядка.
Научная новизна работы. Все основные результаты диссертации являются новыми.
Доказано, что
логика (Г) для арифметически корректных теорий, теории колец, теории полей и теории групп совпадает с исчислением предикатов PC;
для разрешимых теорий, а именно арифметики сложения Ско-лема Sko, арифметики умножения Пресбургера Pre и теории дискретного линейного порядка с минимальным элементом DO (порядковый тип множества натуральных чисел) логики различны, они неразрешимы, и имеет место включение:
PC С C(Sko) С С{Рге) С C(DO) С /,„,
где Cfin — логика конечных моделей;
логики теорий конечных структур — конечных групп, конечных колец, конечных полей, а также монадпческой логики предикатов совпадают с /,„;
для теории равенства и теории плотного линейного порядка без минимального и максимального элементов логики оказываются рарешпмымн, но не могут быть аксиоматизированы никаким множеством схем ограниченной валентности.
Теоретическая и практическая ценность. Работа носит теоретический характер. Ее методы и результаты могут быть полезны специалистам в области математической логики и теоретической информатики.
Апробация работы. Результаты, изложенные в диссертации, докладывались на научно-исследовательском семинаре по математической логике (руководители семинара — член-корр. РАН профессор С. И. Адян, профессор В. А. Успенский), на семинаре "Алгоритмические вопросы алгебры и логики" (руководитель семинара — член-корр. РАН профессор С. И. Адян), на семинаре "Логические методы в информатике" (руководитель семинара — профессор
С.Н. Артёмов), на международной конференции "Logic Foundations of Computer Science: Logic at Yaroslavl'97" и на 10-м международном конгрессе по логике, методологии и философии науки во Флоренции (1995).
Публикации. Результаты диссертации опубликованы в четырех работах автора, перечисленных в конце автореферата.
Структура и объем работы. Диссертация состоит из введения, пяти глав, разбитых на одиннадцать параграфов, заключения и приложения. Список литературы содержит 24 наименование. Общий объем диссертации 68 страниц.