Главная Логика
КАТЕГОРНАЯ ЛОГИКА
|
|
||||||
Секвенциальные импликативные дедуктивные системыСформулируем понятие секвенциальной дедуктивной системы, следуя [Lambek 1988]. Секвенциальная дедуктивная система представляет собой мультиграф, состоящий из класса стрелок (называемых также "секвенциями") и класса объектов (иногда называемых "типами") и двух отображений Начало: {стрелки} -> {объекты}* Конец: {стрелки} —? {объекты} где {объекты}* представляет собой свободный моноид, порожденный классом объектов, его элементами являются последовательности Г - А ... Ап объектов. Заметим, что п может быть равно нулю и в этом случае Г представляет собой пустую последовательность. Стрелка f:-B также называется элементом В. Чтобы получить минимальное секвенциальное дедуктивное исчисление в генценовском стиле (но без структурных правил), введем специальную стрелку
и бинарную операцию на стрелках: ![]() (сечение) Импликативное секвенциальное дедуктивное исчисление GI мы получаем при введении специальных стрелок
и правил
Как и в случае импликативного дедуктивного исчисления, легко видеть, что наше импликативное секвенциальное дедуктивное исчисление GI соответствует системе I. Действительно, мы получаем: а) аксиому I в виде:
б) правило модус поненс в виде:
Если мы теперь введем в нашей системе новую специальную стрелку, выглядящую следующим образом:
то мы получаем секвенциальное импликативное исчисление GIB, соответствующее системе минимальной импликативной логики IB [Карпенко 1993, с.230]. Действительно, с помощью ранее введенных правил нетрудно вывести следующее правило:
Для этого достаточно положить
Аксиому В получаем теперь в виде следующей стрелки:
Действуя подобным же образом, мы можем добавить к секвенциальному импликативному исчислению GIB аксиомы, являющиеся аналогами импликативных аксиом С, W> К :
![]() Нетрудно видеть, что это ведет к добавлению следующих правил (стрелок): (достаточно положить/у = е (е (у (/“)»
|
<< | СОДЕРЖАНИЕ | ПОСМОТРЕТЬ ОРИГИНАЛ | >> |
---|