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

• Автор: Федоришин, Богдан Романович
• Шифр специальности: 01.01.06
• Научная степень: Кандидатская
• Год защиты: 2002
• Место защиты: Красноярск
• Количество страниц: 96 с.

ОГЛАВЛЕНИЕ
ВВЕДЕНИЕ

1 СИНТАКСИС И СЕМАНТИКА ДОПУСТИМЫХ

ПРАВИЛ ВЫВОДА В НЕСТАНДАРТНЫХ ЛОГИКАХ

1.1 Семантика Крипке: необходимые предварительные сведения .

1.2 Теория допустимых правил вывода

2 САМОДОПУСТИМОСТЬ КВАЗИХАРАКТЕРИСТИЧЕСКИХ ПРАВИЛ ВЫВОДА ДЛЯ КОНЕЧНЫХ

МОДАЛЬНЫХ /4-АЛГЕБР

2.1 Самодопуетимость правил вывода в нестандартных логиках..

2.2 Строение жесткого фрейма

2.3 Класс жестких (Уггг-фреймов глубины
3 ФИНИТНАЯ АППРОКСИМИРУЕМОСТЬ В СУПЕРИНТУИЦИОНИСТСКИХ ЛОГИКАХ ПО ДОПУСТИМОСТИ
3.1 Финитная аппроксимируемость модальных логик над К
по допустимости
3.2 Отсутствие финитной аппроксимируемости
суперинтуиционистских логик по допустимости
3.3 Финитная аппроксимируемость суперинтуиционистских логик по допустимости
4 НАСЛЕДОВАНИЕ ДОПУСТИМЫХ ПРАВИЛ
ВЫВОДА ДЛЯ ЛОГИКИ КА

4.1 Наследование допустимых правил вывода для
4.2 Критерий наследования допустимости правил вывода КА
4.3 0 логиках над А"4 с отсутствием наследования допустимости КА
5 ЯВНЫЙ БАЗИС ДЛЯ ДОПУСТИМЫХ ПРАВИЛ ВЫВОДА В ЛОГИКЕ ОЬ
5.1 Явный базис в интуиционистской логике Н и
5.2 Описание явного базиса для допустимых правил логики ОЬ
ЗАКЛЮЧЕНИЕ
ЛИТЕРАТУРА
РАБОТЫ АВТОРА ПО ТЕМЕ ДИССЕРТАЦИИ

ВВЕДЕНИЕ
Разработка теории для допустимых правил восходит к исследованиям Новикова, который рассматривал наряду с понятием производного правила(допустимого правила) понятие сильного производного правила вывода, Новиков [29] в своей работе затронул дедуктивные аспекты производных правил вывода в интуиционистской логике. Общепринятое понятие допустимого правила появилось в работе Лоренцена [95], который высоко оценил значимость введенного понятия. Наблюдение Лоренцена заключалось в том, что допустимым правилом для логики А является правило вывода относительно которого логика А замкнута. По сути допустимость правил вывода позволяет нам получать более эффективный вывод формул в данном языке. Таким образом введение допустимого правила позволило смотреть на дедуктивные свойства логических систем с новой точки зрения. В работах Маслова [22, 23, 24] исследовалась возможность применения производных и допустимых правил вывода в различных сферах деятельности; по его мнению — первый тип правил связан с уже развитой теорией, а второй с теорией, которая находится в процессе конструирования.
В исследованиях польской логической школы [126] была подмечена связь допустимого правила для алгебраической логики А и соответственно квазитождества истинного на свободной алгебре счетного ранга из многообразия логики А. Рассмотрение допустимости на алгебраическом языке стало поворотным моментом в исследовании, поскольку в таком случае появилась возможность применить аппарат универсальной алгебры на очень высоком уровне. Более того установление допустимости в нестандартных логических системах таких как Н, К4, 54, Огг, ОЬ и 55 означает получение серьезных результатов в основаниях математики. Сближение математической

Доказательство, (а)Предположим противное. Пусть в F существует ближайший потомок с для root{F). Тогда в F осуществим склеивание следующим образом: Si(F) - с склеим с максимальным элементом фрейма F из Sli(F) - с. В результате получили фрейм Fu который является р-морфным образом F. Далее, в Fi —root(Fi) не существует рефлексивного корня, поскольку ||.9/2(Fi —root(Fi))\ = 2 и Fi -root(Fi) С F. По Определению 2.3 в F должен существовать сгусток С такой, что С- — С = Fj — root(Fx), но root{F)- - root(F) ф F - root(Fi). Противоречие. Таким образом, пришли к выводу, что в F не существует ближайшего потомка для i'oot(F).
(b) Предположим, что в Sli(F) существует антицепь А1 такая, что ||Л'|| = п, где п ^ |JА||, и А1 не имеет ко-покрытия. Рассмотрим в F подфрейм с-. Далее склеим во фрейме с- подмножество А" С А, где ||Л"|| — п, с некоторым элементом из А" (причем если ||Л|| = ||Л'||, то склеиваний не производим). Полученный в результате фрейм F-і является р-морфным образом с-, и, как видно, F2 — root(F2) не имеет рефлексивного корня, поскольку ||Д|| > 2 и F-2 — root(F2) С F. Но по предположению А! не имеет ко-покрытия, а по Определению 2.3 должен существовать сгусток С в F такой, что С-— С = F2—root(F-i). Противоречие. Осталось показать единственность ко-покрытия. Предположим, что в Sl[F) существует антицепь А"' такая, что в F существует по меньшей мере два ко-покрытия для А"'. Далее, в Sl2(F) склеим все ко-покрытия для А'" с единственным. В результате имеем р-морфный образ F:i фрейма F. Фрейм F3 — root(F3) не имеет рефлексивного корня, поскольку из доказанного следует, что 52(F) имеет по меньшей мере три минимальных элемента и F3 — root(F3) С F, так как склеивали несравнимые элементы из одного и того же слоя, но F не имеет сгустка С со свойством С- — С = F3 — root(F3). Противоречие