Модальные логики, основанные на α-пространствах

• Автор: Мурзина, Вета Федоровна
• Шифр специальности: 01.01.06
• Научная степень: Кандидатская
• Год защиты: 2003
• Место защиты: Новосибирск
• Количество страниц: 94 с.

Содержание
Введение
1 Логики а-пространств
1.1 Основные понятия
1.1.1 Топологические пространства Ершова
1.1.2 Модальные логики и шкалы Крипке
1.1.3 Канонические модели
** 1.1.4 Финитно модельное свойство и фильтрации
1.2 Теорема о корректности
1.3 Логические исчисления Ьа и Ь'
1.4 Канонические модели для Ь°иЬ'
1.5 Разрешимость исчислений Ь°, 1/
2 Модальная логика строго линейно упорядоченных /-шкал
. . 2.1 Постановка задачи
2.2 1Ф и структура канонической модели
2.3 Теорема о полноте
2.4 Финитная аппроксимируемость Ы
3 Временная логика строго линейно упорядоченных /-пространств
3.1 Теорема о корректности
3.2 Канонические модели для и ЬТо
3.3 Теорема о полноте
3.4 Финитная аппроксимируемость ЬЛ, ЬЛо

Введение
Теория неклассических логик - одна из важных областей современной логики. Особую роль играют модальные и временные логики. Хотя изучение логических свойств модальностей началось ещё во времена Аристотеля, теория модальных логик является сравнительно новым разделом математической логики: в начале 20-го века К.Льюис сформулировал первые модальные исчисления, а стремительный рост в этой области начался в 40-е - 50-е гг, благодаря работам С.Крипке, К.Льюиса, Дж.МакКинси, Б.Ионссона, А.Тарского и др. Временная логика, как независимая область исследования, возникла благодаря работам Прайора [23] .
Модальная логика по сравнению с классической логикой, отличается большим разнообразием синтаксиса и семантики: кроме обычных логических связок используются различные модальности типа необходимости и возможности. Этим можно объяснить широкое применение модальных и временных логик, например, в информатике, теории искусственного интеллекта, математической лингвистике. Здесь можно упомянуть различные работы, связанные с методами представления знаний [31], [17], логикой стрелок [30]. Теория временных логик также является особенно важной в связи с развитием параллельных вычислений (см.,например, [22]).
В последнее время неклассические логики широко применяются к изучению геометрических структур (например, модальные логики подмножеств действительной плоскости [28], интервальные временные логики [9]) и топологических пространств. Так, например, в [8]
В.Б. Шехтманом в языке с оператором локальной и универсальной истинности построена система аксиом и доказана финитная аппроксимируемость логики произвольного связного, плотного в себе сепарабельного метрического пространства. Также в [8] построена система аксиом для логики рациональной прямой и логики класса всех линейных порядков в языке с временными операторами и операторм локальной истинности.
Применение модальной логики к изучению топологических пространств можно объяснить тем, что модальные логики высказываний можно исследовать с точки зрения их топологической (окрестностной) семантики. Топологическая интерпретация модальности была дана в работах Дж. МакКинси и А.Тарского [21], где была доказана топологическая полнота широко известной модальной логики S4, и позднее в [24]. В окрестностной семантике ’’необходимость” (□) интерпретируется как ” локальная истинность” [24]: если рассматривать точки топологического пространства X как возможные миры, в которых формулы истинны или ложны, то формула ПА истинна в х £ X , если А истинна в некоторой окрестности мира х.
Кроме того, известно, что невозможно многие топологические структуры определить в языке первого порядка. Таким образом, возникает необходимость использовать язык второго порядка. Хотя при аксиоматизации топологических пространств в языке модальной логики строятся более слабые исчисления, они, как правило, являются разрешимыми.
В данной работе исследуются полимодальные логики, связанные с топологическими пространствами Ершова (а-пространствами, /-пространствами, /о-пространствами). При этом рассматривается следующий вопрос: построение логики, описывающей данный класс топологических пространств, и исследование её свойств.
Понятие /-пространства было введено Ю.Л.Ершовым [2], [3], с целью развить теорию вычислимых функционалов. Кроме того, пространства Ершова можно рассматривать как топологический подход к теории областей Ершова-Скотта (domain theory), см. [13], которая является одним из важных разделов современной математики. Теория областей Ершова-Скотта возникла в 70-е гг. независимо в работах Ю.Л.Ершова ([12], [1]) и Д.Скотта [25]. Скоттом теория областей введена как теория программных языков и наиболее развилась в теоретической информатике. В [13] Ю.Л.Ершовым доказано, что введенное Д.Скоттом понятие 5-domain и понятие полного /о-пространства эквивалентны.
В данной работе модальные логики, связанные с пространтвами Ер-
такой, что то -< у и уТхо- Так как х -< уТхо, то по свойству. (М II) 4 выполнено х < то, и предложение 1.4.4 доказано.
Теорема 1.4.5 Формула Л выводима в исчислении I/ тогда и только тогда, когда А истинна во всех й-моделях.
Доказательство Необходимость следует из того, что аксиомы исчисления общезначимы в шкалах, удовлетворяющих условиям (МІ), (МІГ).
Достаточность следует из теоремы 1.4.3 и следствия 1.1.15.
1.5 Разрешимость исчислений Ьп и I/
Цель этого раздела — доказать теорему о финитной аппроксимируемости исчисления Ьа. Из этой теоремы сразу следует разрешимость исчислений и I/.
Отметим, что нельзя аппроксимировать исчисление Ьп конечными а-моделями, так как в любой конечной о-модели истинна формула □<Л «—> СЦА
Теорема 1.5.1 Для любой формулы А исчисления Ь°, формула А выводима в ІД тогда и только тогда, когда А истинна в любой конечной Т-модели.
Доказательство По теореме 1.4.2 любая выводимая в Ь° формула истинна во всех Т-моделях. Обратное утверждение для Ьп доказывается методом фильтраций.
Пусть формула Ао невыводима в исчислении Тогда по следствию 1.1.15 она опровергается в канонической модели Мдля Ьп. Пусть Ф -множество формул, содержащее ДиЬ(До) и {/3}, замкнутое относительно подформул и удовлетворяющее следующим условиям:
(1ф) П*йА Є Ф П^А Є Ф,
(2Ф) П<А Є Ф => ПА Є Ф,
(Зф) Є Ф ==>• □ <А и □ СЦЛ Є Ф.
Заметим, что множество Ф конечно.
Построим фильтрацию М/о через Ф.