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

pi b V'-i

- 8 ИЮН BOB

МОСКОВСКИЙ ГОСУДАРСТВЕННЫЙ УНИВЕРСИТЕТ им. М. В. ЛОМОНОСОВА

МЕХАНИКО-МАТЕМАТИЧЕСКИЙ ФАКУЛЬТЕТ

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

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

ЯВОРСКИЙ РОСТИСЛАВ ЭДУАРДОВИЧ

ПРЕДИКАТНЫЕ ЛОГИКИ ТЕОРИЙ ПЕРВОГО ПОРЯДКА

Автореферат

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

Москва — 1998

Работа выполнена на кафедре математической логики и теории алгоритмов механико-математического факультета Московского государственного университета им. М. В. Ломоносова.

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

наук, профессор С. Н. Артёмов Официальные оппоненты — доктор физико-математических

наук И. Г. Лысенок — кандидат физико-математических наук В. X. Хаханян Ведущая организация — Институт программных систем

Российской академии наук г. Переславль-Залесский

Защита диссертации состоится " 5 " июня 1998 г. в 16 ч. 05 мин. на заседании диссертационного совета Д.053.05.05 при Московском государственном университете им. М. В. Ломоносова по адресу: 119899, ГСП, Москва, Воробьевы горы, МГУ, механико-математический факультет, аудитория 14-08.

С диссертацией можно ознакомиться в библиотеке механико-математического факультета МГУ (Главное здание, 14 зтаж). Автореферат разослан " 5 " мая 1998 г.

Ученый секретарь диссертационного совета Д.053.05.05 при МГУ доктор физико-математических наук,

профессор В. Н. Чубариков

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

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

PC.

Пусть фиксирована теория Т первого порядка. Интерпретацией предикатного языка в язык теории Т назовем всякое отображение /, сопоставляющее каждому предикатному символу некоторую формулу в языке теории Т с тем же набором свободных переменных, причем / коммутирует с булевыми связками, кванторами и операцией замены переменных. Логикой С(Т) теории Т называется множество предикатных формул ip, таких что при любой интерпретации формула f(<p) выводима в теории Т.

Можно также говорить о логике модели или класса моделей, понимая под этим логику элементарной теории этой модели или класса моделей соответственно.

Согласно теореме Геделя о полноте, множество предикатных формул, истинных во всех моделях при любой интерпретации совпадает с PC, поэтому для классических теорий первого порядка логика С(Т) содержит исчисление предикатов PC.

Логика £(Т) может совпадать с исчислением предикатов либо быть собственным расширением PC. Рассмотрим, например, интерпретации предикатного языка, при которых предикатные символы интерпретируются отношениями на множестве натуральных чисел, выразимыми в арифметике. Как следует из теоремы Гильберта — Бернайса (см. [1], глава IV), такое ограничение не приведет к появлению новых общезначимых схем: множество формул, истинных при любой интерпретации из указанного класса совпадает с PC. Однако если при интерпретации предикатных символов ограничиться только отношениями, выразимыми в терминах порядка на множестве N натуральных чисел, или другим более ограниченным набором, получим новую предикатную логику, являющуюся собственным расширением

'Hilbert D., Bernays Р. Grundlagen der Mathematik, II. — New York, Berlin, Heidelberg, Tokio: Springer-Verlag, 1968.

2Rabin M.O. Decidable Theories// Handbook of Mathematical Logic J. Barwise (ed.). — North-Holland Publishing Company, 1977.

РС. Это можно показать, используя тот факт, что любое определимое в (]М, <) множество либо является конечным, либо имеет конечное дополненнс [2].

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

Аналогичная конструкция рассматривалась раньше в различных работах. Так, В. А. Лифшиц в [3] дает следующее определение: предикатная формула <р называется Т-общезначимой, если ее любая интерпретация выводима в Т; классическая теория Т является геделев-ской относительно классического исчисления предикатов РС, если каждая Т-общезначимая предикатная формула доказуема в РС. Другими словами, Т — геделевская теория, если С(Т) = РС. Им было замечено, что каждая геделевская теория неразрешима, а также доказано, что арифметика Пеано РА и некоторые ее подтеории являются геделевскими теориями.

Предикатные логики расширений классической арифметики рассматривались В.А.Варданяном в [4]. В его исследованиях логика С{Т) арифметической теории Т возникла как безмодальный фрагмент предикатной логики доказуемости теории Т. Им было показано, что для любой степени неразрешимости (1 существует расширение Т арифметики Пеано РА, такое что степени неразрешимости Т и С(Т) равны с1.

Особо важное значение вопрос изучения логик теорий имеет в

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 и некоторый класс Т интерпретаций языка L в язык теории Т. Тогда логика С(Т, L, Т) есть по определению множество формул языка 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Артёмов С.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.

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

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

Доказано, что

• логика С(Т) для арифметически корректных теорий, теории колец, теории полей и теории групп совпадает с исчислением предикатов РС;

• для разрешимых теорий, а именно арифметики сложения Ско-лема вко, арифметики умножения Пресбургера Рге и теории дискретного линейного порядка с минимальным элементом БО (порядковый тип множества натуральных чисел) логики различны, они неразрешимы, и имеет место включение:

РС С £(5Ь) С ЦРгс) С ЦБО) С £/,„, где £/,„ — логика конечных моделей;

• логики теорий конечных структур — конечных групп, конечных колец, конечных полон, а также монадпческой логики предикатов совпадают с £/,,,;

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

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

Апробация работы. Результаты, изложенные в диссертации, докладывались на научно-исследовательском семинаре по математической логике (руководители семинара — член-корр. РАН профессор С. И. Адян, профессор В. А. Успенский), на семинаре "Алгоритмические вопросы алгебры и логики" (руководитель семинара — член-корр. РАН профессор С. И. Адян), на семинаре "Логические методы в информатике" (руководитель семинара — профессор

С.Н. Артемов), на международной конференции "Logic Foundations of Computer Science: Logic at Yaroslavl'97" и на 10-м международном конгрессе по логике, методологии и философии науки во Флоренции (1995).

Публикации. Результаты диссертации опубликованы в четырех работах автора, перечисленных в конце автореферата.

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

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

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

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

Определение 1. (см. [8]) Интерпретацией называется отображение / множества формул сигнатуры <т\ в множество формул сигнатуры <Т2, которое каждой формуле сигнатуры 0\ ставит в соответствие формулу сигнатуры о^ с трм же набором свободных переменных, причем / коммутирует с булевыми связками, кванторами и операцией замены свободных переменных.

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

Определение 2. [5] Пусть фиксирована некоторая теория первого порядка Т. Предикатная формула называется Т-общезначнмой, если ее любая интерпретация выводима в Т. Множество таких предикатных формул мы будем называть логикой теории Т и обозначать ЦТ).

Приведем основные признаки включения логик ЦТ).

Пусть Ц обозначает множество предикатных формул, истинных во всех одноэлементных моделях.

Признак 1. Для любой теории Т имеет место включение:

РС С £(Т) С

Признак 2. Если теория является расширением теории Т\ в том же языке, то С{Т\) С ^(Тг).

Признак 3. Если теория Тг является консервативным расширением теории Т\, то С{Т^) С С{Т\).

Признак 4. Пусть существует интерпретация д языка теории Т\ в язык теории, Т<2 такая что для любой формулы (р в языке Т\ из Ту Ь д{<р) следует Г, Ь Тогда С{Т2) С С(Т{).

Признак 5. Пусть теория Т" получена из Т в результате стандартной процедуры расширения с помощью определений. Тогда С(Т') — ЦТ).

Следующее определение заимствовано из [12]. Пусть М\ — модель сигнатуры — (Р"1,... ,Р£к), М.1 — модель сигнатуры о2- Будем говорить, что модель М.\ относительно элементарно определима в модели М2, если существуют такие формулы 5(х), РЦхи ..., хщ),..., Рк(хи..., хПк) сигнатуры сг2, что

• множество К ^ {а | М-ч |= 5(а)} не пусто,

• модель К. сигнатуры с носителем А", в которой предикаты Pi определены формулами Р*(х\,... ,хщ), элементарно эквивалентна

Пусть ТЬ{М.) обозначает элементарную теорию модели М.

Признак 6. Пусть в модели выразима по крайней мере одна константа, п М. \ относительно элементарно определима в М.ч- Тогда £(ГЛ(М2)) С С{ТН(М\)).

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

Теория Т называется арифметически корректной, если все арифметические отношения выразимы в Т, и теоремы Т истинны в стандартной модели арифметики.

12Ершов Ю.Л. Проблемы разрешимости и конструктивные модели. — М.: "Наука", 1980.

Теорема 1. Для любой арифметически коррскной теории Т логика С(Т) совпадает с исчислением предикатов РС.

Следствие 1. Исчисление предикатов РС является логикой истинностной арифметики ТА и всех ее подтеорий в полном арифметическом языке, в частности, арифметики Пеано РА.

Доказательства следующих трех теорем основываются соответственно на признаке 6 и результатах о погружении арифметики в элементарные теории кольца целых чисел, поля рациональных чисел и группы иТ^Ъ) верхних унптреугольных 3x3 матриц над кольцом целых чисел.

Теорема 2. (а) Логика элементарной теории кольца целых чисел совпадает с исчислением предикатов РС. (б) Логика теории колец совпадает с РС.

Теорема 3. (а) Логика элементарной теории поля рациональных чисел совпадает с исчислением предикатов РС. (б) Логика теории полей совпадает с РС.

Теорема 4. (а) Логика элементарной теории группы í7Tз(Z) верхних унптреугольных 3x3 матриц над кольцом целых чисел совпадает с исчислением предикатов РС.

(б) Логика теории групп совпадает с исчислением предикатов РС.

В третьей главе изучены теории классов конечных моделей. Напомним, что £/„, обозначает множество предикатных формул, истинных во всех конечных моделях.

Теорема 5. Пусть теория Т полна относительно класса своих конечных моделей. Тогда логика теории Т содержит £/,>,:

с/ы с ЦТ).

Следующая теорема даст необходимое и достаточное условие обратного включения С(Т) С £/;„. Будем говорить, что алгебра Лин-денбаума с одной переменной ЬА\- для теории Т модельно бесконечна, если для сколь угодно большого натурального п найдется модель М теории Т, в которой определимы п различных подмножеств, то есть существуют формулы Л^х), Л2(.г), .. ., Л„(.г) в языке теории Т, такие что все множества М,- = {а, £ М | М ЛДга)} различны.

Теорема 6. Пусть Г — произвольная теория первого порядка, тогда

£(Т) С С¡¡п <=>■ LAXT модельно бесконечна.

Поскольку Cfin существенно неразрешима [12], из включения С(Т) С £/,,, следует неразрешимость С(Т).

Следствие 2. Пусть Т теория первого порядка, такая что LA)p модельно бесконечна. Тогда логика С(Т) неразрешима.

Применяя теорему 5 вместе с теоремой G получаем следующую серию результатов.

Теорема 7. £/ш является логикой следующих теорий:

а) логики одноместных предикатов PC1 (множества общезначимых формул в языке, содержащем только одноместные предикатные символы);

б) теории класса всех конечных полей;

в) теории класса всех конечных циклических групп.

То же имеет место и для других теорий, рассмотренных Ю.Л. Ершовым в [12].

Следствие 3. Сцп является логикой следующих теорий: а) теории класса всех конечных колец; б) теории класса всех конечных абелевых групп; в) теории класса всех конечных групп.

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

Пусть Рге обозначает арифметику сложения Пресбургера, Sko — арифметику умножения Сколема и DO — теорию дискретного линейного порядка с минимальным элементом (порядковый тип множества натуральных чисел). Разрешимость D0 была установлена М. Раби-ным [2]. Основным результатом параграфа 4.1 является следующая теорема о включении.

Теорема 8. Имеет место строгое включение:

PC С C(Sko) С С(Рге) С C{DO) С Cfin. Из этой теоремы и существенной неразрешимости Сцп получаем:

Следствие 4. Логики C(Sko), С(Рге) и C{DO) неразрешимы.

В параграфе 4.2 понятие логики теории обобщается на случай до-казуемостных расширений теорий, что позволяет определить предикатную модальную логику Са(Т) арифметической теории Т.

Предикатный модальный язык получается добавлением модального оператора □ к языку РС. Интерпретацию / предикатного модального языка в язык теории Та доопределим таким образом, чтобы /(□Л) ^ Ш/(Д) для любой предикатной модальной формулы Л, и для

любого предикатного символа Р{х,\,..., хд.) формула /(Р(х[......г*))

не содержала вхождений □.

Предикатной модальной логикой £п(Х') арифметической теории Т назовается множество предикатных модальных формул, таких что для любой интерпретации / имеет место Та Ь 1(<р)-

Следствие 5. Пусть Т обозначает одну из следующих теорий: Бко, Рге или БО. Тогда предикатная модальная логика СП(Т) неразрешима.

Получены следующие результаты:

Теорема 9. Пусть каждая формула в языке теории Т доказуемо эквивалентна в РА некоторой Арформуле. Тогда СП{Т) аксиоматизируема над С(Т) следующими аксиомами А1- АЗ и правилами вывода Ш Г?3:

А1) -* (.') (□<г- -> п'-')-

А2) □ (□^ -> Пу.

АЗ) г] —> где 1) не содержит вхождений □.

Г12) т) *

ф 0<р \/х(р

Пусть QGL обозначает предикатный вариант модальной логики Геделя — Леба GL. Из теорем 8 и 9 получаем

Следствие 6. QGL С Ca{Sko) С Са(Рге) С Ca{DO).

Пятая глава посвящена изучению теории, для которых логика С(Т) оказывается разрешимой. Таковыми, в частности, являются теория равенства Eq и теория Т< плотного линейного порядка без максимального и минимального элементов. Для указанных логик изучен вопрос о конечной аксиоматизируемости.

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

Теорема 10. Логика теории равенства разрешима.

Теорема 11. Логика C(Eq) не может быть аксиоматизирована никаким множеством схем ограниченной валентности.

Аналогичный результат имеет место и для теории Т< плотного линейного порядка:

Теорема 12. Логика С(Т<) разрешима, но не может быть аксиоматизирована никаким множеством схем ограниченной валентности.

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

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

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

РАБОТЫ ПО ТЕМЕ ДИССЕРТАЦИИ

1) Yavorsky R.E. Logical Schemes for First Order Theories// Lecture Notes in Comuter Science. — 1997. — Vol. 1234. — P. 410-418.

2) Яворский Р.Э. Предикатные логики разрешимых фрагментов арифметики//Вестник Московского Университета. Сер. 1. Математика. Механика. — 1998. — N 2. — С. 11-15.

3) Яворский Р.Э. Системы аксиом и модели для теорий первого порядка с оператором доказуемости// Вестник Московского Университета. Сер. 1. Математика. Механика. — 199G. — N 1. — С. 12-16.

4) Yavorsky R.E. On provability extensions of arithmetical theories// 10th International Congress LMPS, Florence. Volume of abstracts. — 1995. — P. 67.