Интуиционистские версии конечнозначных логик тема автореферата и диссертации по математике, 01.01.06 ВАК РФ

ВВЕДЕНИЕ.

ГЛАВА I. Интуиционистские версии конечнозначных пропозициональных логик.

§ I. Синтаксис и семантика интуиционистских версий конечнозначных пропозициональных логик.

§ 2. Пропозициональные исчисления.

§ 3. Корректность пропозициональных исчислений.

§ 4. Полнота пропозициональных исчислений.

§ 5. Интуиционистские версии произвольных конечнозначных логик.

ГЛАВА II. Алгебраический подход к семантике интуиционистских версий конечнозначных пропозициональных логик.

§ 6. ип -версии псевдобулевых алгебр и п -алгебры.

§ 7. Интуиционистская версия логики Д.А.Бочвара и псевдобочваровы алгебры.

§ 8. Алгебраический подход к семантике интуиционистских версий произвольных конечнозначных логик.

ГЛАВА III. Интуиционистские версии конечнозначных логик предикатов.

§ 9. Синтаксис и семантика интуиционистских версий конечнозначных логик предикатов.

§ 10. Исчисления предикатов.

§ II. Корректность исчислений предикатов.

§ 12. Полнота исчислений предикатов.^

§ 13. Применение интуивдонистской версии логики Д.А.Бочвара к анализу парадоксов теории множеств.УЗ

§ 14. Интуиционистские версии более широкого класса логик предикатов. ^

§ 15. Ультрапроизведения «-структур Крипке. ^

ГЛАВА 1У. Секвенциальные исчисления и аналитические таблицы.

§ 16. Секвенциальные исчисления.

§ 17. Аналитические таблицы.

§ 18. Корректность систем аналитических таблиц и секвенциальных исчислений.

§ 19. Полнота систем аналитических таблиц и секвенциальных исчислений.

§ 20. Квазисеквенциальные исчисления.

§ 21. Секвенциальные и квазисеквенциальные исчисления для пропозициональных логик.

Интуиционистские версии конечнозначных логик представляют собой сравнительно новый вид неклассических логик. Они исследовались в работах Руссо [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 - 21714. 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. North- Holl.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.