Пропозициональные исчисления и относительные многообразия алгебраических систем

В настоящее время в математической логике большое внимание уделяется исследованию неклассических логик. Необходимым этапом исследования всякой неклассической логики является исследование ее на уровне пропозиционального языка, т. е. языка исчисления высказываний. В связи с этим построены и изучаются различные пропозициональные исчисления. Среди них наибольшее внимание исследователей привлекают интуиционистское и модальные пропозициональные исчисления. В то же время интенсивно изучаются и многие другие пропозициональные исчисления, отличающиеся друг от друга как исходными аксиомами и правилами вывода, так и языком, т. е. исходными пропозициональными связками. В связи с этим в качестве самостоятельного объекта исследования рассматривается пропозициональное исчисление, заданное произвольным набором аксиом и правил вывода в языке с произвольными пропозициональными связками (соответствующие определения можно найти, например в работе [27]).

С другой стороны, традиционными объектами исследования универсальной алгебры являются многообразия алгебр и алгебраических систем. К фундаментальным результатам в этой области относятся теорема Биркгофа [14, стр.337], известная для многообразий алгебраических систем, и теорема Йонссона [29], известная для многообразий алгебр. Всякому многообразию алгебр соответствует множество тождеств, истинных во всех алгебрах этого многообразия. Всякое такое множество называется эквациональ-ной логикой. Эквациональная логика может быть также определена как множество тождеств, замкнутое относительно выводимости в эквациональном исчислении (такая выводимость определяется аксиомами равенства и подстановкой [32]).

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

1) рассматривать пропозициональные и эквациональное исчисления с единой точки зрения и в связи с этим ввести понятие относительного многообразия алгебраических сйстем, более общее, чем обычные понятия многообразий алгебр и алгебраических систем;

2) обобщить некоторые факты (среди которых теоремы Бирк-гофа и Йонссона), известные для многообразий алгебр или алгебраических систем, на относительные многообразия алгебраических систем и использовать эти обобщения в исследовании пропозициональных исчислений;

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

4) использовать в исследовании пропозициональных исчислений выразительные возможности не только пропозиционального языка, но также и того языка исчисления предикатов, атомарным фрагментом которого является пропозициональный язык.

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

В главе I, кторая состоит из шести параграфов (§§ 1−6), подробно описывается точка зрения на пропозициональный язык как на атомарный фрагмент языка исчисления предикатов, лежащая в основе предлагаемого подхода, и вводятся связанные с такой точкой зрения общие понятия, в том числе понятие относительного многообразия алгебраических систем.

В соответствии с традиционным определением класс алгебраических систем является многообразием, если он может быть задан тождествами. При этом под тождествами понимаются атомарные формулы языка исчисления предикатов с равенством, т. е. формулы вида или Р («fcj,.(где — термы и Р предикатный символ), а под алгебраическими системами — нормальные модели исчисления предикатов с равенством. Исчисление предикатов с равенством определяется помимо логических аксиом и правил вывода дополнительными аксиомами равенства, и, таким образом, аксиомы равенства тоже участвуют в задании многообразия, образуя основание (фундамент, базу), к которому добавляются тождества. Это основание состоит из квазитождеств, т. е. из формул |, где — тождества (К = = 0,. — при fC=0 квазитождество вырождается в тождество). В рамках предлагаемого подхода разрешается в качестве основания допускать произвольный набор квазитождеств и рассматривать многообразия относительно такого основания (при этом отсутствие аксиом равенства в основании будет означать отсутствие равенства в языке). Такие многообразия и называются относительными многообразиями алгебраических систем (соответствующее точное определение дается в § 4).

Так же, как всякому многообразию алгебр может быть сопоставлена эквациональная логика, представляющая собой множество тождеств, истинных во всех алгебрах этого многообразия, так и всякому относительному многообразию может быть сопоставлена логика в соответствующем основании. Так же, как всякая эквациональная логика представляет собой множество тождеств, замкнутое относительно выводимости в эквациональном исчислении, так и всякая логика в основании Q представляет собой множество тождеств, замкнутое относительно выводимости в исчислении с основанием Q. Исчисление с основанием Q определяется основанием Q таким образом, что тождества из этого основания играют роль аксиом, а квазитождества — роль правил (соответствующее точное определение дается в § 5).

Понятие исчисления с основанием Q представляет собой обобщение, с одной стороны, понятия эквационального исчисления и, с другой стороны, понятия пропозиционального исчисления в общем понимании Харропа [27]. (Здесь нужно заметить, что содержательное понятие пропозиционального исчисления формально может уточняться двумя способами. Первый способ, которому также следует и работа Харропа [27], состоит в том, что пропозициональное исчисление отождествляется с множеством выводимых в этом исчислении формул, а второй способ предполагает неотъемлемой принадлежностью пропозиционального исчисления операцию присоединения следствий [19, стр.212], соответствующую выводимости в этом исчислении. Наши обобщения отталкиваются от понятия пропозиционального исчисления, формально уточненного вторым способом, в то же время ссылка на работу Харропа [27] подчеркивает то обстоятельство, что имеется в виду пропозициональное исчисление, заданное произвольным набором аксиом и правил вывода в языке с произвольными пропозициональными связками.). Исчисление с основанием Q представляет собой пропозициональное исчисление, если сигнатура языка исчисления предикатов содержит единственный и притом одноместный предикатный символ. В этом случае предикатный символ в записи атомарных формул может опускаться, функциональные символы могут рассматриваться как пропозициональные связки, а атомарные формулы и их переменныекак пропозициональные формулы и переменные. Подробно эта ситуация описывается в § 6, где также рассматриваются в качестве примеров следующие хорошо известные пропозициональные исчисления: интуиционистское исчисление Н, нормальное модальное исчисление S4 и слабое модальное исчисление S4l0, которое представляет собой ненормальный аналог исчисления S4 (о нормальных и ненормальных модальных исчислениях см. [8] и [9]).

В первых трех параграфах главы I напоминаются некоторые известные и устанавливаются некоторые новые факты об исчислении предикатов без равенства, необходимые для дальнейшего изложения. В § I наряду с обычной выводимостью в исчислении предикатов рассматривается выводимость с ограничением на применение правила обобщения, подобная той, которая участвует в формулировке теоремы дедукции для исчисления предикатов [16, стр.70], и описывается отвечающая такой выводимости полная семантика. Как затем устанавливается в последних параграфах главы I, такая выводимость в исчислении предикатов соответствует бесподстановочной выводимости в пропозициональном исчислении. В § 2 определяется понятие взаимно точного гомоморфизма (такой гомоморфизм для моделей исчисления предикатов без равенства играет ту же роль, какую для моделей исчисления предикатов с равенством играет изоморфное вложение) и вводится важное для всего последующего изложения понятие нормальной модели исчисления предикатов без равенства, которое представляет собой обобщение хорошо известного понятия нормальной модели исчисления предикатов с равенством С16, стр.91]. В § 3 дается ряд технических определений и вводится ряд понятий, которые часто используются в дальнейшем, а также устанавливаются некоторые связанные с ними результаты.

Большинство утверждений главы I носят подготовительный характер и имеют несложные доказательства. В связи с этим вместо названия «теорема», которое используется в последующих главах, утверждениям главы I присваивается название «предложение» .

Основные результаты главы I опубликованы в работах С 33, 35,36,37] .

В главе 2, которая состоит из пяти параграфов (§§ 7-II), главное место принадлежит обобщениям теорем Биркгофа и Йонссона на относительные многообразия алгебраических систем.

Теорема Биркгофа в формулировке для многообразий алгебр утверждает, что для всякого класса алгебр К.

Ке = Н5Р (К), где К — многообразие алгебр, порожденное классом К (это обозначение следует работе Йонссона [29]), а HSPIK) — класс алгебр, полученный последовательным взятием всевозможных прямых произведений, подалгебр и гомоморфных образов алгебр из К .

Перенос этой теоремы с многообразий алгебр на (обычные) многообразия алгебраических систем имеется в [14, стр.339], а теорема 7.2, доказанная в § 7, представляет собой обобщение теоремы Биркгофа на относительные многообразия алгебраических систем. При этом условие обобщенной теоремы Биркгофа (т.е. теоремы 7,2) требует, чтобы основание Q, в котором рассматриваются относительные многообразия алгебраических систем, удовлетворяло некоторому так называемому С-условию.

Теорема Йонссона [29] утверждает, что в случае, когда всякая алгебра из многообразия К имеет дистрибутивную решетку конгруэнций,.

Ке= PsWSPa (K), где R MS Р (К) — класс алгебр, полученный последователь.

О U> ным взятием всевозможных ультрапроизведений, подалгебр, гомоморфных образов и подпрямых произведений алгебр из К • Обобщение этой теоремы на относительные многообразия алгебраических систем представляет собой теорема 9.1, доказанная в § 9. Условие обобщенной теоремы Йонссона (т.е. теоремы 9.1) требует, чтобы основание Q, в котором рассматриваются относительные многообразия алгебраических систем, удовлетворяло некоторому так называемому col-условию. В § 9 также устанавливаются следствия обобщенной теоремы Йонссона, представляющие интерес в связи с их приложениями к пропозициональным исчислениям. В § 8 проводятся необходимые обобщения известных фактов, связанных с понятиями подпрямого произведения и подпрямой неразложимости.

В § 10 устанавливаются условия, при которых относительные многообразия алгебраических систем обладают свойствами многообразий алгебр, а в § II описывается широкий класс пропозициональных оснований, удовлетворяющих сс1-условию (пропозициональные основания — это основания определяющие пропозициональные исчисления). К пропозициональным исчислениям, определяемым основаниями из этого класса, применимы следствия обобщенной теоремы Йонссона, установленные в § 9. В число таких пропозициональных исчислений попадают многие известные пропозициональные исчисления. Среди них есть как исчисления, имеющие в качестве нормальных моделей алгебры (например, исчисления ff-8 и S41), для которых те же следствия могут быть получены с помощью обычной теоремы Йонссона для многообразий алгебр, так и исчисления, для которых такие следствия с помощью обычной теоремы Йонссона получены быть не могут. К числу последних относятся интуиционистское пропозициональное исчисление с произвольными дополнительными связками [ 23] и многочисленные ненормальные модальные пропозициональные исчисления [9] (к которым относится и исчисление .

Основные результаты главы 2 опубликованы в работе [383 .

В главе 3. которая состоит из пяти параграфов (§§ 12−16), изучаются вопросы, связанные с понятием структурной полноты. Понятие структурной полноты и близкие к нему понятия наиболее известны в связи с интуиционистским пропозициональным исчислением ft-fl и их традиционные определения опираются на специфику этого исчисления (см., например, работы [17,18,22]). Точка зрения на пропозициональные исчисления, описанная в главе I, позволяет естественным образом определить эти понятия в общем случае. Эти обобщения согласуются с ранее известными определениями, в том числе с общими определениями Погожельского [31], основанными на ином подходе.

Понятие структурной полноты связано с понятиями допустимости и производности правил. В рамках описанного в главе I подхода правила отождествляются с квазитождествами, и это дает возможность удобно определить в общем случае как понятия допустимости, производности и структурной полноты, так и ряд других близких к ним понятий. Эти определения даются в § 12, где также устанавливается ряд связанных с ними общих результатов. В §§ 13−15 общие определения из § 12 рассматриваются в приложении к исчислениям Н, $ 4 и S&L причем в § 13 показывается, что для интуиционистского пропозиционального исчисления (HI они соответствуют определениям, опирающимся на специфику этого исчисления. Приложение к исчислениям U, S4 и SHjl общих результатов из § 12 позволяет установить некоторые новые для этих исчислений результаты.

Последний параграф главы 3 посвящен обобщению некоторых результатов из работы [22], установленных для интуиционистского пропозиционального исчисления Н, среди которых основное место занимает теорема об алгоритмической распознаваемости структурной полноты табличных логик. Доказанное в § 16 обобщение этой теоремы распространяет ее на произвольное исчисление с конечным основанием, удовлетворяющим сА-условию. В частности, это обобщение распространяет исходную теорему на всякое пропозициональное исчисление, имеющее конечное основание из описанного в § II класса пропозициональных оснований, удовлетворяющих cd-условию (в число таких пропозициональных исчислений попадают и исчисления S4.

Основные результаты главы 3 опубликованы в работе [.37]] .

В главе 4, состоящей из двух параграфов (§§ 17,18), демонстрируется то преимущество описанного в главе I подхода, которое позволяет использовать выразительные возможности не только пропозиционального языка, но также и языка исчисления предикатов, атомарным фрагментом которого является пропозициональный язык. Такой язык исчисления предикатов называется расширенным языком, а логика L называется конечно аксиоматизируемой в расширенном языке, если существует конечно аксиоматизируемая теория в исчислении предикатов, которая в пересечении с множеством атомарных формул дает логику L (эти определения приводятся в § 17).

В § 18 рассматривается введенная Д. П. Скворцовым в [20] с.и. логика бесконечных задач LS. Эта логика, как и близкая к ней логика финитных задач Ю. Т. Медведева [15], представляет собой один из вариантов уточнения идеи А. Н. Колмогорова об интерпретации интуиционистского исчисления как исчисления задач [30]. Из результатов, установленных в [12], следует, что логика LS (как и логика финитных задач Ю.Т.Медведева) не является конечно аксиоматизируемой в пропозициональном языке. Содержание параграфа составляет построение конечной аксиоматики логики LS в расширенном языке, причем определяющие эту аксиоматику формулы приводятся явно. Одним из непосредственных следствий является рекурсивная аксиоматизируемость логики LS в пропозициональном языке, доказанная в работе Д. П. Скворцова [20] другим методом, использующим технически сложную табличную процедуру Крипке.

Результаты главы 4 опубликованы в работе [34] .

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

1. Бродский С. Д., Когаловский С. Р. Замечания о многообразиях алгебраических систем. — Acta Sci.Math., 1981, v. 43, p. 263−266.

2. Будкин А. И., Горбунов В. А. К теории квазимногообразий алгебраических систем. Алгебра и логика, 1975, т.14, № 2, с. 123−142.

3. Горбунов В. А., Туманов В. И. Строение решеток квазимногообразий. В сб.: Труды института математики, том 2. Математическая логика и теория алгоритмов. Новосибирск, 1982, с. 12−44.

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

Введение

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

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

6. Клини С. К.

Введение

в метаматематику. М.: ИЛ, 1957.

7. Кон П. Универсальная алгебра. М.: Мир, 1968.

8. Крипке С. А. Семантический анализ модальной логики. I. Нормальные модальные исчисления высказываний. В кн.: Фейс Р. Модальная логика. М.: Наука, 1974, с. 254−303.

9. Крипке С. А. Семантический анализ модальной логики. П. Ненормальные модальные исчисления высказываний. В кн.: Фейс Р. Модальная логика. М.: Наука, 1974, с. 304−323.

10. Кузнецов А. В. 0 суперинтуиционистских логиках. -Матем. исследования, 1975, т.10, № 2, с. 150−158.

11. Максимова Л. Л., Рыбаков В. В. 0 решетке нормальных модальных логик. Алгебра и логика, 1974, т.13, № 2,с. 188−216.

12. Максимова JI.Л., Скворцов Д. П., Шехтман В. Б. Невозможность конечной аксиоматизации логики финитных задач Медведева. -Докл. АН СССР, 1979, т.245, № 5, с. I05I-I055.

13. Мальцев А. И. Подпрямые произведения моделей. -Докл. АН СССР, 1956, т.109, № 2, с. 264−266.

14. Мальцев А. И. Алгебраические системы. М.: Наука, 1970.

15. Медведев Ю. Т. Финитные задачи. Докл. АН СССР, 1962, т.142, V 5, с. I0I5-I0I8.

16. Мендельсон Э.

Введение

в математическую логику. М.: Наука, 1971.

17. Минц Г. Е. Допустимые и производные правила. Зап. научн. семинаров Ленингр. отд. матем. инст. АН СССР, 1968, т.8, с.189−191.

18. Минц Г. Е. Производность допустимых правил. Зап. науч. семинаров Ленингр. отд. матем. инст. АН СССР, 1972, т.32, с. 85−89.

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

20. Скворцов Д. П. Логика бесконечных задач и модели Крипке на атомных полурешетках множеств. Докл. АН СССР, 1979, т.245, № 4, с. 798−801.

21. Скорняков Л. А. Элементы теории структур. М.: Наука, 1982.

22. Циткин А. И. 0 структурально полных суперинтуиционистских логиках. Докл. АН СССР, 1978, т.241, № I, с. 40−43.

23. Чагров А. В. Неклассические логики и многообразия логических матриц. Школа-семинар «Телави-83п. Тезисы докладов и сообщений. М., 1983, с. 136−138.

24. Шенфилд Дж. Математическая логика. М.: Наука, 1975.

25. Эсакиа Л. JI. 0 многообразии алгебр Гжегорчика. В сб.: Исследования по неклассическим логикам и теории множеств. М.: Наука, 1979, с. 257−287.

26. Frayn Т., Morel А.С., Scott D.S. Reduced direct products. Fund. Math., 1962, v. 51, p. 195−228.27″ Harrop R. Some structure results for propositional calculi. J. Symb. Logic, 1965, v. 30, N 3″ p. 271 — 292.

27. Horn A. The separation theorem of intuitionist proposii i I i.

28. Kolmogoroff A.N. Zer Deutung der intuitionistischen Logic. Math. Zeischr., 1932, v. 35, N I, p. 58−65.

29. Pogorzelski W.A. Structural completeness of the pro-positional calculus. Bull. Acad. Pol. Sci., Ser. Math., Astr. et Phis., 1971, v. 19, p. 34−9-35I.t 1 ' it.

30. Taylor V/. Equational logic. Houston T. Math., 1979, Surv., p. i-iii, 1−69.

31. Шум А. А. Пропозициональные семантические системы. -Семиотика и информатика, 1979, № II, с. 88−116.

32. Шум А. А. Конечная аксиоматика логики бесконечных задач в расширенном языке. В сб.: Математическая логика и математическая лингвистика. Калинин, 1981, с. 165−170.

33. Шум А. А. Псевдоинтуиционистское пропозициональное исчисление. В сб.: Математическая логика, математическая лингвистика и теория алгоритмов. Калинин, 1983, с. 95−108.

34. Шум А. А. 0 выводимости с подстановкой и без подстановки. Школа-семинар «Телави-83И. Тезисы докладов и сообщений». М., 1983, с. 136−138. 107.

35. Шум А. А. Структурная полнота в обобщенных пропозициональных исчислениях. Деп. в ВИНИТИ 5 июня 1984 г., 3640−84 Деп.

36. Шум А. А. О многообразиях алгебраических систем. -Седьмая всесоюзная конференция по математической логике. Тезисы докладов. Новосибирск, 1984, с. 200.