Допустимые и выводимые правила вывода в нестандартных логиках

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

1 ПРЕДВАРИТЕЛЬНЫЕ СВЕДЕНИЯ О ДОПУСТИМЫХ ПРАВИЛАХ ВЫВОДА В НЕСТАНДАРТНЫХ ЛОГИКАХ
1Л Модальные, временные и суперинтуиционистские логики
1.2 Семантика Крипке
1.3 Допустимые и выводимые правила вывода
2 ДОПУСТИМОСТЬ ПРАВИЛ ВЫВОДА ДЛЯ НЕКОТОРОГО КЛАССА 54-ЛОГИК, НЕ ОБЛАДАЮЩИХ СВОЙСТВОМ ВЕТВЛЕНИЯ
2Л Предварительные сведения
2.2 Алгоритмический критерий допустимости правил вывода для некоторого класса 54-логик, не обладающих свойством ветвления
3 ДОПУСТИМОСТЬ ПРАВИЛ ВЫВОДА ДЛЯ ЛОГИКИ £ С ОПЕРАТОРОМ ” ЗАВТРА”
3.1 Предварительные сведения
3.2 Свойства логики £
3.3 Условие допустимости правил вывода в логике £
4 СТРУКТУРНО-ПОЛНЫЕ 54-ЛОГИКИ
4.1 Структурно-полные 54-логики: необходимые предварительные сведения
4.2 Описание структурно-полных 54-логик ширины 2, порожденных конечным корневым фреймом с двухэлементным первым слоем
4.3 О ширине структурно-полных табличных 54-логик

ЗАКЛЮЧЕНИЕ
ЛИТЕРАТУРА
РАБОТЫ АВТОРА ПО ТЕМЕ ДИССЕРТАЦИИ

Актуальность темы. Теория нестандартных систем логического вывода сформировалась в начале двадцатых-тридцатых годов 20-го века в работах Лукасе-вича, Льюиса, Гедели и Тарского, как результат анализа поведения аксиоматических систем оснований математики и парадоксов материальной импликации. Однако нестандартные логики по сравнению с классической логикой, отличаются большим разнообразием синтаксиса и семантики. Поэтому к концу 20-го века возникло много новых направлений исследований, связанных с применением идей и методов нестандартной логики в программировании, информатике, теории искусственного интеллекта, представлении знаний и других областях знаний (см., например, [40, 41, 54, 80, 83, 99]).
Большое влияние на становление теории нестандартных систем логического вывода оказано классической теорией доказательств, одним из центральных моментов которой являются правила вывода, поскольку от них зависит эффективность доказательств. Первыми работами, непосредственно посвящёнными изучению правил вывода, были работы Лося (1955), Тарского (1956) и Сушко (1958). При исследовании правил вывода естественно возник вопрос о том какие правила можно присоединять к логическим системам, сохраняя при этом множество доказуемых теорем системы. Такой класс правил, получивших название допустимых правил вывода, был определен II. Лоренценом [71] в 1955 году. Оказалось, что это в точности допустимые правила вывода - правила, относительно которых данная логика замкнута. Несколько ранее проблема допустимых правил вывода для интуиционистской логики изучалась U.C. Новиковым, который наряду с понятием производного правила вывода (допустимого правила вывода) рассматривал понятие сильного производного

в логике //. Предположим, что модели с вышеописанными свойствами не существует. Тогда правило вывода г допустимо в логике у. В самом деле, предположим противное. Пусть правило вывода г не допустимо в логике у. Тогда по лемме 2.2 существует /л-модель с вышеописанными свойствами, что противоречит условию доказываемого утверждения. Ясно, что существование модели Л4, удовлетворяющей условиям (а)-(г) леммы 2.2, можно проверить за конечное число шагов, так как таких моделей ограниченной мощности - конечное число. Теорема доказана.
Следствие 2.1. Суперинтуиционистская логика у, наименьший модальный напарник т(уі) и наибольший модальный напарник сг(уі) логики уі над 54 разрешимы относительно допустимости правил вывода.
Доказательство. По теоремам 9.68, 9.70 [42] соответственно получаем, что сг(уі) = у2 © бгг, т{уі) = у2. Следовательно, в силу теоремы 2.2 логики о(у{), т(^х) разрешимы относительно допустимости правил вывода. В силу разрешимости по допустимости логики <т(у) по теореме 3.2.2 [90] получаем, что логика уі разре-шима относительно допустимости правил вывода. Следствие доказано.
3 ДОПУСТИМОСТЬ ПРАВИЛ ВЫВОДА для ЛОГИКИ £ С ОПЕРАТОРОМ ”ЗАВТРА”
В данной главе исследуется нетранзитивная временная логика С с оператором ’’Завтра”. Данная логика интересна тем, что из каждого элемента ,С-фрейма достижим только один элемент, то есть в данной логике оператор □ совпадает с оператором
О. Исходя из этого свойства при изучении допустимых правил вывода необходимо было использовать технику, отличную от ранее использовавшейся.