Секвенциальные импликативные дедуктивные системы

Сформулируем понятие секвенциальной дедуктивной системы, следуя [Lambek 1988]. Секвенциальная дедуктивная система представляет собой мультиграф, состоящий из класса стрелок (называемых также "секвенциями") и класса объектов (иногда называемых "типами") и двух отображений

Начало: {стрелки} -> {объекты}*

Конец: {стрелки} —? {объекты}

где {объекты}* представляет собой свободный моноид, порожденный классом объектов, его элементами являются последовательности Г - А ... А_п объектов. Заметим, что п может быть равно нулю и в этом случае Г представляет собой пустую последовательность. Стрелка f:-B также называется элементом В.

Чтобы получить минимальное секвенциальное дедуктивное исчисление в генценовском стиле (но без структурных правил), введем специальную стрелку

и бинарную операцию на стрелках:

(сечение)

Импликативное секвенциальное дедуктивное исчисление GI мы получаем при введении специальных стрелок

и правил

Как и в случае импликативного дедуктивного исчисления, легко видеть, что наше импликативное секвенциальное дедуктивное исчисление GI соответствует системе I. Действительно, мы получаем:

а) аксиому I в виде:

б) правило модус поненс в виде:

Если мы теперь введем в нашей системе новую специальную стрелку, выглядящую следующим образом:

то мы получаем секвенциальное импликативное исчисление GIB, соответствующее системе минимальной импликативной логики IB [Карпенко 1993, с.230]. Действительно, с помощью ранее введенных правил нетрудно вывести следующее правило:

(слабая транзитивность)

Для этого достаточно положить

Аксиому В получаем теперь в виде следующей стрелки:

Действуя подобным же образом, мы можем добавить к секвенциальному импликативному исчислению GIB аксиомы, являющиеся аналогами импликативных аксиом С, W> К :

Нетрудно видеть, что это ведет к добавлению следующих правил (стрелок):

(достаточно положить/^у = е (е (у (/“)» (достаточно положить f^w-e(w(f^ec))) (где/^к = е (к (/))).