Дискретно-непрерывная математика (стр. 63 )

имеются различные тавтологии из которые не являются тав-

тологиями например, формула

(Для справедливости заметим, что уже после публикации статьи [Карпенко 1993] мы обратили внимание на матричную логику (см. [Rescher 1969]). Здесь вначале определяется системаоперации которой задаются на множестве рациональных чисел из отрезка [0, 1] следующим образом:

Логическая матрица для логики есть матрица для без истинностного значения '/2. Здесь как раз и появляется формула

которая имеет место в но не в )

8.4. Модальные логики

Класс модальных логик устроен даже сложнее, чем класс суперин­туиционистских логик (si-логик), хотя что может быть сложнее континуума? Здесь мы рассмотрим наиболее интересные льюисовские модальные системы и определим важную тенденцию развития современной логики.

8.4.1. К. И. Льюис и К. Гёдель

В [Lewis 1912] (1883-1964) строит новую теорию логи­ческого следования взамен теории материальной (классической) импликации, изложенной в «Principіа Mathematica». Исходным мо­тивом Льюиса было избавиться от так называемых парадоксов ма­териальной импликации. Под последними в первую очередь рас­сматривались формулы

которые содержательно означали следующие принципы: «Истина имплицируется из чего угодно» и «Противоречие имплицирует все что угодно». В классической С2 и интуиционистской Int логиках эти принципы общезначимы. В итоге материальная импликация была заменена Льюсом на строгую импликацию →, определение которой потребовало введения модальных операторов (возможно) и (необходимо):

В работе [Lewis 1918] уделено внимание проблеме исчислений, в которых подобные формулы не выводимы, а введенное там ис­числение получило в дальнейшем обозначение S3.

Развитие современной модальной логики можно датировать

началом 30-х годов XX века, когда вышла книга [Lewis and Lang-

forrd 1932], содержащая формулировки модальных логических сис-

тем S1 — S5, в дальнейшем названных лыоисовскими, и двухстра-

ничная статья К. Гёделя [Godel 1933], в которой приводится

формулировка льюисовских систем S4 и S5 в стиле, ныне называе-

мом гёделевым, и утверждается погружаемость интуиционистской

логики Int в S4 переводом, при котором интуиционистские связки

интерпретируются соответствующими классическими, но при этом

используется усиливающий оператор который навешивается на

пропозициональные переменные и усиливает импликацию.

Работа Гёделя имела фундаментальное значение для дальней­шего развития логики. Во-первых, оказалось, что исчисление, строящееся как ограничение классической логики (отбрасывание ряда неприемлемых формул), на самом деле может оказаться рас­ширением последнего: льюисовские системы строятся как расши­рение классической логики С2, т. е. к аксиоматизации С2 добавля­ются характеристические аксиомы для модальных операторов.

(Напомним, что подобный метод аксиоматизации был затем использован при ак­сиоматизации многозначных логик (см. выше раздел 6.3).

Во-вторых, погружаемость одних логических систем в другие оз­начала сходство способов рассуждения различных логических сис­тем, а также обладание порой весьма важными одинаковыми свой­ствами. В данном случае последнее означало то, что si- логики и модальные логики стали изучаться параллельно. Систематическое исследование тесной связи между модальными логиками и si-логиками было начато в классической работе Дж. Маккинси и А. Тарского [McKinsey and Tarski 1948].

8.4.2. Некоторые модальные логики

В обзоре [Bull andSegerberg 1984] отмечается, что за последние го­ды появилось астрономическое число модальных логик, при этом имеются в виду логики, которые получили «персональное» обозна­чение. В этой работе приводится список из 15- модальных логик. В [Chagrov and Zakhaiyaschev 1997] приводится список из 30 нормальных модальных логик, причем 5 из них задают клас­сы логик. Некоторые из этого списка будут полезными для нас.

Модальная логика является нормальной т. т.т., когда она вклю­чает все тавтологии С2 и аксиому

и замкнута относительно подстановки для переменных, modus ponens и правила Гёделя: если то Логика называется квазинормалъной, если она не удовлетворяет правилу Гёделя. Рассмотрим еще несколько модальных аксиом:

Логика S4 есть КТ4; логика S5 есть есть логика Гжегорчика Grz (в первоначальной аксиоматике она представлена в [Grzegorchyk 1967]). Логика Grz вызвала особый интерес, поскольку является наибольшим нормальным расширени­ем модальной логики S4, в которое погружается интуиционистская логика Int посредством перевода Гёделя-Тарского-Мак-Кинси. есть логика Гёделя-Лёба GL - логика доказуемости, в которой оператор необходимости понимается как формальная до­казуемость в некоторой аксиоматической теории подобной ариф­метике Пеано РА. Логика GL полна относительно арифметической интерпретации: модальная формула А доказуема в GL т. т.т., когда А есть

РА -тавтология [SoJovay 1976].

Заметим, что в [Dummett and Lemmon 1959] по характеристи­ческой матрице Яськовского для Int построена характеристическая матрица для S4. Очень простая континуальная характеристическая матрица для S5 сконструирована А. Прайором [Prior 1957].

В качестве истинностных значений берутся все 1-0-последовательности счетной длины, т. е. булевы вектсгоа, состоящие из вхождений 1 - «истина» и 0 - «ложь» (а их континуум — перациями являются покомпонентные булевы операции (подробно об этом см. в разделе 10.5), а операторы возможности и необ­ходимости определяются следующим образом:

Строгое доказательство того факта, что эта модель является точной моделью для S5, дано в [Massey 1972].

В [Fine 1974] доказывается континуальность множества рас­ширений S4 (однако, это уже после результата Янкова о контину­альности класса si-логик [Янков 1968]). Результаты, аналогичные тому, что между Int и любой si - логикой находится континуум ло­гик [Кузнецов 1971], справедливы и в модальном случае. Так, кон­тинуален любой интервал между модальной логикой L и ее собст­венным расширением при и во многих других случаях.

Оказывается, континуальность классов логик является не ис­ключением, а нормой. См. об этом специальную статью и [Горбунов и Рыбаков 2007].

8.4.2.1. Табличность и предтабличность

Как и в случае с интуиционистской логикой Int, одним из первых вопросов для новых логических систем является вопрос об их таб-личности. Логика является табличной, если она характеризуется конечными моделями (шкалами, алгебрами, матрицами и т. д.). Дж. Дугунджи [Dugundji 1940], используя метод К. Гёделя для Int (см. выше), показал, что люисовские системы, включая S1 - S5, яв­ляются бесконечнозначными логиками, т. е. не имеют конечной ха­рактеристической матрицы. кроггс [Scroggs 1951] дока­зал, что логика S5 является предтабличной, т. е. любое ее собственное (нормальное) расширение характеризуется конечной матрицей с единственным выделенным значением. Напомним, что именно таким образом была получена четырехзначная логика V2 (см. выше раздел 5.4.3.1).

Понятия табличности и предтабличности тесно связаны и по­следнее понятие в явном виде введено [Кузнецов 1971] для того, чтобы на этом пути подойти к решению проблемы разрешимости табличности. Если имеется простое описание всех предтабличных логик в некотором классе расширений, то мы име­ем эффективный критерий табличности для этого класса. Конечно, хотелось бы иметь алгоритм, который по исчислению выдавал бы, является логика конечнозначной или нет.