Полная версия

Главная arrow Логика arrow КАТЕГОРНАЯ ЛОГИКА

  • Увеличить шрифт
  • Уменьшить шрифт


<<   СОДЕРЖАНИЕ ПОСМОТРЕТЬ ОРИГИНАЛ   >>

ПРОПОЗИЦИОНАЛЬНАЯ КАТЕГОРНАЯ ЛОГИКА

первая. Импликативные дедуктивные системы и дедуктивные экспоненциальные категории

Ламбековские дедуктивные системы и дедуктивные категории

Описывая возникновение понятия дедуктивной системы К.Дошен [Dosen 1996] замечает (как и многие другие авторы), что в целом процедура построения гильбертовских формулировок систем обычно сводится к выбору из всех формул данного языка теорем системы. Генценовские формулировки логических систем, чьей разновидностью являются системы натурального вывода, основываются на формулировании отношении следования между формулами. В простейшей секвенциальной системе секвенции имеют вид А- В, где посылка А и заключение В являются формулами. О подобных секвенциях говорится, что они являются единичными по обеим сторонам.

В более общем случае допускается множественность формул, по крайней мере, в посылках, по левую сторону от знака К, что соответствует тому факту, что дедуктивный вывод может исходить более чем из одной посылки. Посылки обычно образуют множество, или секвенции, или мультимножества, либо что-нибудь другое. Тем не менее, допущение лишь единичных формул по обеим сторонам секвенции не должно быть существенным 01раничением, если у нас имеются связки, позволяющие заменить совокупность посылок на синонимичную единичную посылку.

Секвенция Ah- В может пониматься как утверждение о том, что существует естественно-дедуктивное доказательство В, исходящее из гипотез, собранных в совокупность А, в то время как в гильбер- товской формулировке системы мы доказываем секвенции вида 1- Ву где пропозициональная константа / замещает пустую совокупность посылок. (Конечно, обычно нет необходимости в снабжении каждой теоремы приставкой Ih, если подразумевается, что каждая теорема имеет такую приставку, но некоторые авторы обычно уделяют внимание снабжению теорем в гильбертовской формулировке системы хотя бы символом Ь).

Заметим, что символ I- не является символом языка, к которому принадлежат А и В в А-В. Однако, если мы рассмотрим расширения языка, в котором Ah В будет формулой, то секвенциальные формулировки будут подобны гильбертовским формулировкам в таком расширенном языке. В случае- единичным по обеим сторонам секвенций мы можем даже заменить символ h на знак импликации и тогда наша система будет выглядеть как система в обычной гильбертовской формулировке. Тем не менее, система в подобной гильбертовской формулировке будет представлять собой систему более высокого порядка.

На практике, в случае секвенциальных формулировок логических систем, мы заинтересованы лишь в существовании доказательств секвенции, и мы не вводим специальной нотации для различения различных доказательств одной и той же секвенции. Это выглядит так, как будто все доказательства одной и той же секвенции эквивалентны. Тем не менее, если исходить из процедуры нормализации или устранения сечения, то хотелось бы иметь возможность приравнять одни доказательства и различить другие. В этом случае было бы удобно записывать рядом с секвенцией некоторый код, указывающий на историю получения ее доказательства. Подобное кодирование стало общепринятым в натуральной дедукции, где типовые лямбда термы выполняют роль кодов (а кодирование называется "изоморфизмом Карри-Ховарда" или "интерпретацией формул типами"). Если правила секвенциальной системы ссылаются на правила натуральной дедукции, то мы могли бы работать с типовым лямбда кодированием, но ниже мы увидим, что существуют иные (даже для натуральной дедукции) виды кодирования, исходящие из теории категорий.

Коды будут термами, такими, что аксиоматические секвенции кодируются атомными термами, а правила вывода секвенциальной системы отвечают операциям на термах. Это незначительно отличается от общепринятой практики, где правила вывода являются отношениями, не обязательно функционального типа. Например, правило перестановки

в обычной секвенциальной системе, с произвольными конечными Г и А, возможно пустыми, последовательностями формул, не соответствуют функции, которая, будучи приложена к верхней секвенции, порождает единичную нижнюю секвенцию: мы можем переставить первую и вторую формулу в секвенции по левую сторону от символа н, или вторую и третью и т. д. Однако, мы можем заменить подобные нефункциональные правила на совокупность функциональных правил, осуществляющих по отдельности многие задания, приписываемые первоначальному правилу. (Перестановка может быть заменена на бесконечно много функциональных правил, переставляющих первую и вторую формулы, вторую и третью формулы и т.д., либо двумя функциональными правилами: первое из них переставляет первую и вторую формулу, а другое ставит первую формулу в конец секвенции по левой стороне.) Как бы там ни было, большинство правил, с которыми мы имеем дело на практике, являются функциональными. В общем случае, операции на термах, отвечающие правилам вывода, являются частичными операциями, поскольку правила могут быть применены к секвенциям одного типа, но не другого.

Когда доказательство секвенции может быть преобразовано в другое доказательство той же самой секвенции посредством процедуры, подобно тому, как мы действуем в случае нормализации натуральной дедукции или устранения сечения, мы приравниваем коды двух доказательств. Чтобы избежать тривиальности, не обязательно требовать, чтобы коды, отвечающие той же самой секвенции, были всегда одинаковы.

Введем понятие системы секвенций с кодами, называемых дедуктивными системами (и термин и понятие принадлежат Дж. Ламбеку).

Пусть у нас имеется множество вещей, которые мы назовем, нейтрально, объектами, но из которых мы намереваемся построить язык - если мы будем иметь в виду теоретико-доказательные вопросы логики, то под этими объектами лучше всего, конечно, понимать формулы. Будем использовать буквы А, В, ... (в случае необходимости - с индексами) как схемы букв для объектов. При этом у нас нет необходимости уточнять, что представляют собой объекты. В то же время, если наш язык имеет связки, то они лучше всего отвечают понятию операций на объектах. Предполагается, что эти операции носят тотальный характер. Под "операцией" мы будем понимать, как обычно это делается, любую функцию с областью

определения D' и областью значения D, при этом необязательно одно-однозначную. Таким образом "операция на объектах" есть более общее понятие, чем "связка", которая включает в себя, как правило, лишь биективные функции. Алгебра формул полностью свободна, но при этом не исключается, что анализируемые объекты могут оказаться различным образом взаимно эквивалентны. Могут иметься также специальные объекты, которые представляют собой нульместные операции на объектах.

В качестве следующего шага мы устанавливаем, что у нас имеется множество предметов, отвечающих секвенциям с кодами, сингулярными по обеим сторонам, которые мы будем называть стрелками. Помимо этого имеются две функции, сопоставляющие каждой стрелке объект, являющийся ее началом, т.е. ее посылкой, и объект, являющийся концом, т.е. заключением. Может существовать более чем одна стрелка для одного и того же начала и конца. Выражение / Ah- В означает, что/есть стрелка с началом А и концом В будем говорить, что Ah- В является типом f Для именования стрелок будем использовать просто f g, ... без указания типа, если у нас нет в этом необходимости. Эти термы-стрелки отвечают кодам, о которых речь шла выше.

Множество объектов и множество стрелок совместно с функцией начала и конца стрелок образует граф (в теории графов, обычно, подобные вещи называются несколько сложнее - мультиграфами с циклами). В принципе мы можем допустить существование таких совокупностей объектов и стрелок, которые являются собственными классами, но вопросы мощности этих совокупностей для нас здесь не играют никакой роли. Использование множеств, а позднее малых категорий, делает наше изложение более определенным и ясным.

Итак, граф состоит из класса стрелок (в теории графов называемых "ориентированными ребрами") и класса объектов (обычно называемых "вершинами", но в различных разделах математики может использоваться и иная терминология) и двух отображений: Начало: {стрелки} —> {объекты}

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

Вместо того, чтобы писать начало(/) = А, конец{/) = В, часто пишут /: А-> В или f. Ah- В. Для логики интерес представляют графы с дополнительной структурой.

Дедуктивная система представляет собой граф, который может иметь следующие операции на стрелках: для каждого объекта А

нульместную операцию (т.е. специальную стрелку), стрелку тождества

и бинарную частичную операцию на стрелках (композицию), которая, будучи применена к стрелкам f. А К В и g: В С, порождает стрелку gf: At- С. Наряду с этими операциями могут иметься и другие. Специальные стрелки соответствуют аксиоматическим секвенциям и «-местным операциям на стрелках с п > 1, отвечающим правилам вывода. Композиция представляет собой единичную форму правила сечения:

Вместо того, чтобы говорить, как это обычно принято в‘логике, что стрелка есть теорема дедуктивной системы или доказуема в ней, будем просто говорить, что стрелка есть стрелка дедуктивной системы, как это порой также делается в логике. Когда речь идет о стрелках дедуктивной системы, то имеются в виду стрелки дедуктивной системы, что не следует смешивать с логическим способом высказывания о формулах системы, истинных формулах языка логической системы, когда не подразумевается их доказуемость.

Отношение следования является обобщением отношения пред- порядка на совокупности объектов и объект (или на две совокупности объектов, когда отношение следования множественно по обеим сторонам, как в случае генценовских систем классической логики. В случае дедуктивных систем мы имеем дело с иным обобщением отношения предпорядка. Отношение предпорядка представляет собой специальный вид дедуктивной системы, когда для каждой пары объектов (А,В) имеется, по крайней мере, одна стрелка с началом А и концом В. Предупорядоченные графы выполняют следующую эквивалентность, которая имеет место для каждой дедуктивной системы:

Справа налево это эквивалентно рефлексивности: а слева направо это дает нам транзитивность:

Отсюда по рефлексивности и транзитивности мы получаем стрелку тождества и композицию стрелок.

Дедуктивная категория есть дедуктивная система, в которой следующие уравнения между доказательствами имеют место:

Нетрудно видеть, что эти тождества имеют совершенно ясный смысл в теории доказательств. Первое из них утверждает, что композиции, т.е. сечения, с единичными стрелками являются устранимыми, в то время как второе говорит о том, что композиции могут меняться местами друг с другом. В свободной дедуктивной категории, порожденной произвольным графом без стрелок, т.е. множеством объектов, композиция устранима: в этой категории имеются только лишь стрелки тождества.

Существование подобных свободных дедуктивной категорий гарантируется эквациональной формой категорных аксиом. Свободные категории некоторого вида подобны чистым логическим системам: они выполняют лишь то, что допустимо для подобного вида категорий и ничего сверх этого.

Заметим, что с более абстрактной точки зрения можно рассматривать категорию (что обычно и делается в математике) просто как некую структуру, когда она представляет собой совокупность двух разновидностей сущностей: объектов (а не формул) и стрелок или морфизмов (а не выводов). Сами объекты тоже могут обладать структурой, а морфизмы представляют собой отображения, сохраняющие эту структуру.

Самый популярный пример подобной категории категория множеств Set. В этой категории объекты представляют собой произвольные множества, а морфизмы являются произвольными отображениями.

Другой популярный пример - категория предупорядоченных множеств. Ее объекты представляют собой предупорядоченные множества, т.е. множества с заданными на них транзитивным и рефлексивным отношением, в то время как морфизмы суть монотонные отображения, сохраняющие эти отношения.'

Связь между множествами и дедуктивными категориями можно описать следующим образом: свободная абстрактная категория, порожденная произвольным графом без стрелок (так называемая дискретная категория или дискрет), может рассматриваться как

1 Многочисленные примеры категорий можно найти в [Гольдблатт 1983].

категорное понятие множества. В подобной категории имеются только стрелки тождества.

 
<<   СОДЕРЖАНИЕ ПОСМОТРЕТЬ ОРИГИНАЛ   >>