Интуиционистские версии конечнозначных логик

Интуиционистские версии конечнозначных логик представляют собой сравнительно новый вид неклассических логик. Они исследовались в работах Руссо [I, 2*1, Жирара [3 1, Вудраф-фа [41 и некоторых других йвторов [б, 6 1. Одним из аргументов в пользу изучения интуиционистских версий конечнозначных логик является возможность их приложения к другим областям математической логики. Например, в работе Г з! интуиционистская версия трехзначной логики применялась для получения интересных теоретико-доказательственных результатов.

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

В литературе интуиционистские версии конечнозначных логик обычно определяются путем подробного описания их синтаксиса или семантики. Попытки уточнить понятие интуиционистской версии без использования конкретных синтаксических или семантических построений были сделаны автором в статьях [6−10 1. Представляется естественным, что интуиционистская версия конечно-значной логики L должна отвечать следующим требованиям: (I) совокупность теорем интуиционистской версии включается в множество теорем логики L* - (2) для интуиционистской версии логики L имеют место аналоги дизъюнктивного и экзистенциального свойств- (3) интуиционистская версия логики L связана с интуиционистской логикой таким же специфическим соотношением, каким сама логика Z. связана с классической. В [ 9, 101 последнее требование уточняется следувдим образом: интуиционистская версия логики L содерсит изоморф (в смысле [ II ]) интуиционистской логики (Определяемые в диссертации интуиционистские версии отвечают указанным требованиям) .

Обязательной частью всех упомянутых работ по интуиционистским версиям является описание подходящей семантики и построение полных относительно нее исчислений. В статьях [4 — 81 рассматривались интуиционистские версии трехзначных пропозициональных логик, а именно: логики Д. А. Бочвара [ill — в [б -8*1, логики С. Холдена [12] - в [4, 6, 8^, логики К. Се-герберга [13] - в [41 .В работах [4−81 вводилась В [ill Д. А. Бочвар показал, что введенная им трехзначная логика содерсит изоморф.классической. Этот результат можно распространить, на весьма обширный класс логик, используя, например, рассуждения, аналогичные проделанным в данной диссертации. семантика типа моделей Крипке, а в [ 7, 8] еще и алгебраическая семантика (псевдобочваровы алгебры). Исчисления гильбертов-ского типа имеются в работе 4 ] .В [5−8] синтаксис задается в виде аналитических таблиц (аналогично [ 14 ]), а в? 8] еще и в виде исчисления трехчленных секвенций.

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

Интуиционистские версии конечнозначных логик предикатов рассматриваются в [з, 10, 15] .В статье Жирара [з] описывается алгебраическая семантика интуиционистской версии трехзначной логики, функционально эквивалентной логике Я. Лукасеви~ ча [ 16 3, и строится полное относительно этой семантики секвенциальное исчисление. В статье [ з] найдена связь между введенной в ней интуиционистской версией и некоторыми фактами обычной теории доказательств. В статьях [ 10, 15] рассматриваются интуиционистские версии широкого класса логик предикатов.

Данная диссертация посвящена решению следующих задач: (а) определить подходящую семантику для интуиционистских версий произвольных конечнозначных пропозициональных логик и широкого класса конечнозначных логик предикатов, найти алгоритм построения полных относительно этой семантики исчислений- (б) установить наличие у интуиционистских версий аналогов некоторых известных свойств интуиционистской логики- (в) определить, как связаны между собой интуиционистские версии конечнозначных логик и интуиционистская логика.

Интуиционистские версии конечнозначных логик рассматриваются в диссертации с точки зрения классической теоретико-множественной метаматематики. Использование неконструктивных методов в метаматематике интуиционистской логики имеет достаточно богатую традицию. В этой связи мокно упомянуть известные монографии П. С .Новикова [ 17 1, М. Фиттинга? 181, Е. Расевой и Р. Сикорского^.191, А. Г. Драгалина [ 20 3 .В работе используются некоторые теоретико-модельные методы (аппарат ультрапроизведений). Идея применения «метода разверток» для доказательства теорем о полноте относительно семантики типа моделей Крипке принадлежит Д. П. Скворцову. В диссертации этот метод применяется также для исследования алгебраической семантики интуиционистских версий. Способ построения аналитических таблиц из последней главы близок к описанному в книге М.Фиттинга.

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

Е 6 — 10, 15 ] .

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

Основные результаты работы.

I) Предложены общие эффективные способы построения полных относительно естественной сешнтики исчислений для интуиционистских версий конечнозначных логик.

В пропозициональном случае для интуиционистских версий широкого класса истинностно полных (Црасширяющих логик С 21 3 1 строятся секвенциальные исчисления и исчисления гиль-бертовского типа, а для интуиционистских версий произвольных конечнозначных логик — так называемые квазисеквенциальные исчисления и исчисления квазигиль б ертов ского типа (в смысле L 21 3) — семантика алгебраическая и типа моделей Крипке.

В случае логик предикатов исчисления гильбертовского типа В этот класс входят функционально полные логики Э. Поста 22 3, Тво к —логики, введенные С. В. Яблонским [ 23 3 и рассмотренные’им с точки зрения алгебры — кзначных логик, ко-нечнозначные логики Я. Лукасевича [ 24 3, логики, соответсву-ющие конечным алгебрам Г. Мои сила [25 3, трехзначная логика Д. А. Бочвара [ II3 и ее конечнозначные обобщения Р. Ш. Григолии и В. К. Финна [ 26 3, трехзначные логики Г.-Д.Эббингхауза [273 и К. Сегерберга [13 3 «& М^ -логики, применяемые в работе В. К. Финна [28 3 для формализации индуктивных рассуждений. и секвенциальные исчисления для интуиционистских версий широт кого класса допустимых логик, а исчисления квазигильбертов-ского типа и квазисеквенциальные — для еще более широкого класса ¿-гбдопустимых логиксемантикой служат и.-стук-туры Крипке — обобщение интуиционистских моделей Крипке. В работе определены ультрапроизведения /*. -структур Крипке — обобщение ультрапроизведений из работ [ 29, 30 1 — доказаны аналоги теоремы Лося об ультрапроизведении и теоремы компактности А. И. Мальцева Е 31, 32], а также теорема о полноте в сильной форме.

Секвенции в данной работе имеют в отличие от Ц I ] только два членасечение является допустимым правилом.

Чтобы выяснить соотношение результатов данной работы и работ других авторов рассмотрим отдельно случаи пропозициональной логики и логики предикатов. В первом случае заметим, что в статье Руссо [II исследовались интуиционистские версии ко-нечнозначных логик с единственным выделенным значением, в то время как в данной диссертации никаких дополнительных ограничений на множество выделенных значений не накладываетсякроме того для каждой фиксированной конечнозначной логики совокупность интуивдонистских версий, подлежащих рассмотрению в диссертации, оказывается шире, чем в упомянутой выше работе т.

Класс допустимых логик включается в класс истинностно полных^{-расширяющих} логик [213. Среди указанных выше примеров истинностно полных € -расширяющих логик только для логик из работы [ 261 не ясно, являются ли все они допустимыми. Остальные могут служить примерами допустимых логик.

Руссо [ I 3 1.

В диссертации установлена связь между семантикой интуиционистских версий типа моделей Крипке и алгебраической семантикой, чего не было сделано в работах Ц X — 5 3 • Алгебры из статей [ 2, 3 3 можно рассматривать как частные случаи алгебр, изучаемых в диссертации.

Что касается логики предикатов, то из известных автору работ других математиков только в статье Жирара £зЗ рассматривалась интуиционистская версия одной трехзначной логики предикатов, причем в [ зЗ отсутствовали исчисления гильбертов-ского типа и семантика в стиле Крипке.

2) Доказано, что для построенных в диссертации интуиционистских версий имеют место аналоги дизъюнктивного и экзистенциального свойств (аппарата из Ц I 3 недостаточно, чтобы дать формулировку этим аналогам). В пропозициональном случае установлена разрешимость, финитная аппроксимируемость и бесконеч-нозначность интуиционистских версий.

3) Получены результаты о погружении интуиционистской логики в каждую из построенных интуиционистских версий и о погружении каждой такой версии в интуиционистскую логику. В диссертации (также как в [ I 3) интуиционистская версия однозначно определяется способом упорядочения множества истинностных значений V исходной конечнозначной логикив [ I 3 У образует цепь, в-которой наибольшим элементом является выделенное значениев диссертации V образует нижнюю полурешетку, в которой одно из невыделенных значений предшествует одному из выделенных.

— II.

Аналогичные результаты отсутствуй в работах [ I — 5 ]).

Обозначения. В диссертации используется обычная теоретико-множественная символика. Дня индексированных семейств употребляются обозначения типа { - е х или < | I е: IУ, в зависимости от того, какого рода обозначения в данном контексте обычно приняты в литературе. Символом И. обозначается графическое равенство слов, знак & читается «означает по определению», И и ?7 суть обозначения для истинностных значений «истина» и «ложь», соответственно.

Иногда бывает удобно сокращенно записать некоторое выражение метаязыка. В этом случае используется логическая символика. Чтобы избежать возможных коллизий, применяются следующие обозначения для логических связок в метаязыке: 11 — отрицание, 8с — конъюнкция, V/ - дизъюнкция, — импликация, <=> - эквиваленция, V — квантор всеобщности, 31 -квантор существования.

1. Rousseau G. Sequents in many-valued logic 1. — Fund. Math., 197o, 67, pp. 125 — 151.

2. Rousseau G. Post algebras and pseudo-Post algebras. -Fund. Math., 1970, 67, pp. 133 14−5.

3. Girard J.Y. Three-valued logic and cat-elimination: The actual meaning of Takeuti’s conjecture. Diss. Math., Warszawa, 1976, 136, pp. 1 — 49.

4. Woodruff P.W. On constructive nonsense logic. In: Modality, morality and other problems of sense andnonsense. Lund, 1973, pp. 192 — 205. «.

5. Szomolanyi J. On the intuitionistic logic based onthree-valued logic. In: Zbornik filosofickej fakultytuniverzity Komenskeho. 7−8, Bratislava, 1976 1977, pp. 113 — 126.

6. Аншаков 0. M. О конструктивных вариантах некоторых трехзначных логик. В кн.: Релевантные логики и теория следования. (Материалы II Советско-финского коллоквиума по логике. Москва, декабрь 3 — 7, 1979 г.). — М., 1979, с.7−10.

7. Аншаков О. М. О некоторой конструктивизации пропозициональной логики Д. А. Бочвара. В кн.: Семиотика и информатика. — М., ВИНИТИ, 1980, вып. 15, с. 61 — 73.

8. Аншаков, 0.М. О некоторых конструктивизациях пропозициональной логик Д. А. Бочвара и С.Холдена. В кн.: Исследования по неклассическим логикам и формальным системам. — М., «Наука», 1983, с. 335 — 359.

9. Аншаков О. М. Интуиционистские версии конечнозначных пропозициональных логик. Деп. в ВИНИТИ 12 июля 1983 г. Р 3859−83 Деп. 123 с. (РЖ Мат. 11 А 91 Р 11, 1983).

10. Аншаков О. М. Интуиционистские версии конечнозначных логик предикатов. Деп. в ВИНИТИ 10 октября 1983 г# Р 5539−83 Деп. 84 с. (РЖ Мат. № I, 1984, I, А 66).

11. Бочвар Д. А. Об одном трехзначном исчислении и его применении к анализу парадоксов классического расширенного функционального исчисления. Матем. сборник, 1938, т. 4, Р 2, с. 287 — 308.

12. Hallden S. The logic of nonsense. Uppsala, 194−9.

13. Segerberg K. A contribution to nonsense logic. Theoria, 1965, 31, PP- 199 — 21 714. Smullyan R.M. First-order logic. N.Y., Springer Verl., 1968.

14. Аншаков О. М, Секвенциальные исчисления для интуиционистских версий конечнозначных логик. Деп. в ВИНИТИ 10 октября 1983 г. W 5538−83 Деп. 68 с. (РЖ Мат. I, 1984, I, А 67).I.

15. Lukasiewicz J. О logice trowartosciowej. Ruch. filozoficz.1.ow, 1920, 5, PP. 169 171.

16. Новиков П. С. Конструктивная математическая логика сточки зрения классической. М.: «Наука», 1977, 328 с.

17. Fitting М.С. Intuitionistic logic, model theory and forcing. Amsterdam London. NorthHoll.publ. со., 1969.

18. Pa сева E., СикорскийР. Математика метаматематики. -М.: «Наука», 1972, 591 с.

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

Введение

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

20. Анша ков О.М., Рычков С. В. О многозначных логических исчислениях. Докл. АН СССР, 1982, т.264, № 2 с.267−270.

21. Lukasiewicz J., Tarski A. Investigations into the sentential calculus. In: A.Tarski. Logic, Semantics, Metamathematics. Oxford, 1956″ PP. 38−59.

22. Moisil G.C. Notes sur les logiques non chrisippiennes. Ann. sei. Univ. Iassy. 1941, 27, pp. 86 96.

23. Финн B.K. О машинно-ориентированной формализации правдоподобных рассуждений в стиле Ф.БэконаД.С.Милля. В кн.: Семиотика и информатика, вып. 20. М., ВИНИТИ, 1983 с. 35 — 101.

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

25. Кейслер Г., Чэн Ч. Ч. Теория моделей. М.: «Мир», 1977, 614 с.

26. Plonka J. On distributive quasi-lattices. Fund. Math., 1967, 60, N 2, pp. 191 -200.

27. Bochvar D.A. Some aspects of the investigation of reification paradoxes. Acta Phil. Fennica, 1982, 35, pp. 229 — 238.

28. Новиков П. С. О логических парадоксах. Докл. АН СССР, 1947, т. 56, № 5, с. 451 — 453.

29. Бочвар Д. А. Об антиномиях, основанных на группах определений предикатов, каждое из которых непротиворечиво в отдельности. Матем. сборник (новая серия), 1960, т. 52(94), № 1, с. 641 — 646.