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

Сформулируем понятие секвенциальной дедуктивной системы, следуя [Lambek 1988]. Секвенциальная дедуктивная система представляет собой мультиграф, состоящий из класса стрелок (называемых также «секвенциями») и класса объектов (иногда называемых «типами») и двух отображений Начало: {стрелки} -> {объекты}*.

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

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

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

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

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

и правил.

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

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

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

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

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

(слабая транзитивность) Для этого достаточно положить.

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

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

aside class="viderzhka__img" itemscope itemtype="http://schema.org/ImageObject">

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

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