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

ВВЕДЕНИЕ.

ОБОЗНАЧЕНИЯ.

ГЛАВА I. СТРОЕНИЕ УНИВЕРСМЬНЫХ МОДЕЛЕЙ КРШЖЕ

§ I. Суперинтуиционистские и модальные логики.

§ 2. Модели Крипке.

§ 3. Универсальные модели Крипке и овободные алгебры

§ 4. Универсальные модели для ^т.

§ 5. Универсальные модели для Н^т.

§ 6. Оценки функций роста.

§ 7. Универсальные модели финитно аппроксимируемых логик

ГЛАВА 2. НЕРАЗРЕШИМЫЕ ИСЧИСЛЕНИЯ ВЫСКАЗЫВАНИЙ

§ 8. Кодирование полусистем З^э.

§ 9. Леммы о подъеме и спуске.

§ 10, Доказательство теоремы сведения

Теория неклассических логик возникла в начале XX в., когда классическая логика была подвергнута критике с различных позиций. Концепция "интуиционизма", выдвинутая Брауэром (1908), основывалась на конструктивном понимании логических связок, которое не имеет аналога в классической логике. Различные уточнения понятия "конструктивный" привели к логикам, в которых нарушался закон исключенного третьего: интуиционистской логике и ее расширениям С суперинтуиционистским логикам). Исследование этих логик становится актуальной задачей после создания в 30-х гг. теории алгоритмов. (См. Марков [I]).

Другой подход заключается в том, чтобы изучить средствами математической логики связки естественного языка, которые в классической логике не отражаются: необходимость, возможность, контрфактическую импликацию ("если бы., то."), временные связки ("всегда будет", "когда-то было", "вчера", "завтра") и проч. На этом пути возникли модальные логики (Льюис, 10-е - 20-е гг.), временные логики (Прайор, 50-е гг.), релевантные логики (Андерсон-Белнап, 60-е гг.), интенсиональные логики (Монтегю, 60-е гг.) и др.

Постепенно обнаружилось, что неклассические логики различных типов связаны и между собой, и с другими разделами математики. Так, суперинтуиционистские логики с помощью перевода Гёделя - Тар-ского (Оо*/^ [I]-, Мсксп^^То^с [з]) можно трактовать как фрагменты модальных логик; при этом интуиционистскому исчислению высказываний соответствует исчисление Льюиса . Т.наз. квантовые логики (предложенные в 30-х гг. для логического анализа квантовой механики), как недавно выяснилось (Дишкант [I]), можно погрузить в расширения "модальной логики Брауэра". Временные логики (которые являются обобщением модальных) погружаются в модальные ( Tßomoso* [4]), а логики предикатов второго порядка - во временные логики С TßomQ&or) £zj).

В модальной логике отражаются некоторые типы рассуждений теории доказательств ("диагональный метод" Гёделя); при этом необходимость понимается как "доказуемость", а возможность - как "непротиворечивость" (идея такой интерцретадии восходит к Гёделю). В последнее время ведется активное изучение модальных "догик доказуемости" (Кузнецов, Муравицкий £lj; Артемов [i]; So&>\1<у [i]; Мссдогс [i]).

Неожиданная аналогия между модальным исчислением (в формулировке Гёделя) и аксиоматикой топологических пространств по Куратовскому привела Тарского и (независимо) Тана в 1938 г. к топологической интерпретации модальных логик: классические связки интерпретируются по Булю, а связки "необходимо", "возможно" - соответственно, как "внутренность" и "замыкание". Сходная идея лежит в основе "прагматической" семантики Монтегю для интенсиональных логик (1968). Топологическая семантика применима и к суперинтуиционистским логикам, благодаря переводу Гёделя - Тарского; здесь формулам соответствуют открытые подмножества топологических пространств.

Семантика возможных миров, введенная Крипке в 1959 г., связала теорию неклассических логик с теорией частичных порядков и теорией бинарных отношений. Позднее оказалось, что метод вынуж-дения Коэна, применяемый в доказательствах независимости в классических математических теориях, основан на той же идее, что и семантика Крипке ("возможные миры" являются аналогами "вынуждающих условий") - см. Pczf/too [1].

В самое недавнее время (1977-79 гг.) наметились пути для цриложений модальных и суперинтушдаонистских логик в теоретическом программировании. Упомянем здесь о построении программ с помощью интуиционистской логики (см., например, Непейвода [I]) и о модальных "динамических логиках", в которых можно доказывать различные утверждения о программах (о современном состоянии проблем в этой области см. Валиев [I), / Рга& £1], 2]).

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