Модальные логики с оператором разрешимости

• Автор: Золин, Евгений Евгеньевич
• Шифр специальности: 01.01.06
• Научная степень: Кандидатская
• Год защиты: 2002
• Место защиты: Москва
• Количество страниц: 104 с.

Оглавление
Введение

1. Основные определения и факты

2. Логика эпистемической разрешимости

2.1. Транзитивная евклидова логика разрешимости

2.2. Сериальная логика разрешимости

3. Секвенциальная логика арифметической разрешимости

3.1. Аксиоматические системы

3.2. Полнота аксиоматик

4. Секвенциальные рефлексивные логики разрешимости

4.1. Аксиоматические системы

4.2. Метод замыкания
4.3. Полнота аксиоматик
4.4. Полнота посредством обратного перевода
4.5. Неустранимость сечения и интерполяция
4.6. Логика доказательств с оператором сильной разрешимости .
5. Определимые классы шкал
5.1. Определимость классов шкал в [>-языке
5.2. Элементарные эквиваленты для >-формул
5.3. Инфинитарный оператор
5.4. Определимость классов шкал в 3-языке
5.5. Эквиваленты I и II порядка для 3-формул
Библиография

Введение
Актуальность темы. При построении логических исчислений в модальной логике традиционным стал выбор языка с операторами необходимости □ и возможности 0. Однако определенный технический и философский интерес (см. [22]) представляют системы, где в качестве базисного выбирается оператор разрешимости (или неслучайностиJ), подразумеваемая семантика которого определяется равенством >А — ПА V СНА. Это равенство задает перевод О-формул (т. е. формул модального языка с единственным модальным оператором О, или О-языка) в С-формулы (определяемые аналогично). Теперь, если задана С-логика L (т.е. логика в С-языке), то логикой разрешим,ост,и над L (обозначаемой посредством IT) называется множество О-формул, переводы которых являются теоремами логики L.
В работах [22, 23] были предложены различные аксиоматики логик разрешимости над известными нормальными логиками Т, S4 и S5 (определения которых см. ниже). Некоторые семейства логик разрешимости в интервале между Т5” и 85^ изучались в работах [24, 25]. Отметим, что в случае когда логика L содержит Т, а точнее, аксиому рефлексивности ОА —> А, исследование логики разрешимости над L упрощается благодаря тому, что оператор □ выразим через > посредством равенства ОА — А&г О А. Аналогичная картина наблюдается в логике Ver, имеющей
Термин „неслучайность“ (non-contingency) принят в англоязычной литературе; мы будем употреблять термин „разрешимость“, происходящий из рассмотрения доказуемостной интерпретации оператора □ (предложение разрешимо в теории, если в ней доказуемо либо оно, либо его отрицание).
Введение
в числе своих теорем все формулы вида ША: в этой логике □ выражается через > посредством тривиального равенства ПА = Т. В статье [13] построен нетривиальный пример логики, не содержащей Т и отличной от Ver, в которой тем не менее □ выразим через [>.
Систематичное изучение логики разрешимости было начато в работе [17], содержащей первую, достаточно громоздкую аксиоматику минимальной логики разрешимости (т.е. логики КТ). В последующей работе [19] эта аксиоматика была упрощена, а также была аксиоматизирована логика разрешимости над К4.
Определенный интерес к изучению модальной логики связан с возможностью использовать ее в качестве инструмента исследования понятия формальной доказуемости. Эти исследования восходят к работам PL Орлова [6] и К. Гёделя [15]. Формулировка „правильной“ логики доказуемости в арифметике Пеано, известной сейчас как логика Гёделя-Лёба GL, появилась позднее в работе М. Лёба [20], а первое доказательство арифметической полноты логики GL принадлежит Р. Соловэю [30].
Логика Гёделя-Лёба GL является наименьшей по включению логикой доказуемости. Она описывает модальные законы, которым подчиняется предикат доказуемости в „объектной“ теории РА с точки зрения „метатеории“ РА. Если же варьировать „метатеорию“ в классе расширений РА, а „объектную“ теорию — в классе перечислимых расширений РА, то получится семейство логик доказуем,ости (имеющее мощность континуума), полностью описанное Л.Д. Беклемишевым (см. [1], формальное определение логики доказуемости см. там же).
Наряду с доказуемостью, понятие разрешимости в формальной теории является одним из центральных в теории доказательств. Так, первая теорема Гёделя о неполноте утверждает, что существуют неразрешимые в РА предложения. Нам удалось аксиоматизировать лишь минимальную логику арифметической разрешимости — логику GLT. Естественным
Арифметическая разрешимость

условии):
, Л, г , , УжХго В £ (х
<2>) /гс € У% У>В £ Г. >В £{ю| УУ Х
Zxw В £ |ж).
Лемма 3.2.4. (2е*) =$■ (1>).
► Доказательство проведем одновременно для всех го € И7^ индукцией по построению формулы А. При А = ± левая и правая части (1>) ложны. Для А = р утверждение следует из определения [=.
Пусть А= (В -А С). Поскольку множество Г замкнуто, В, С £ Г. Ввиду Г-полноты секвенции го и предположения индукции имеем:
Докажем эквивалентность, помеченную (?).
(=») Если (В -А С) £ |го), то В $. |и?) и С £ (го|, поскольку секвенции =$■ В, (В -А С) и С =Ф- (В С) доказуемы в С.
(У=) Если (В -А С) £ {го|, то невозможно одновременно В £ (гс| и С £ [го), ибо секвенция (В -А С), В => С доказуема в С.
Наконец, пусть А = О В. По предположению индукции для любого ХбИ'Г имеем
(b) ги = В В £ (го|; го ф В УУ В £ |го);
(c) ю |= С УУ С £ (гл>; го [ф С АА С £ [гг?).
Отсюда:
<мр уо В (ь,с) В £ Ы с?
(х) х = В 4А В £ (т[; X ф В УУ В £ |ж).
Отсюда: