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

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

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


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

вторая. Дедуктивные системы и дедуктивные категории

Конъюнктивные и дизъюнктивные дедуктивные системы

Путем добавления к языку новых связок и констант могут быть получены дедуктивные системы иного типа, чем чисто имплика- тивные дедуктивные системы. Приведем примеры подобных систем, соответствующих существующим логическим системам.

Рассмотрим, например, (ко)импликативные дедуктивные системы, в языке которых наряду с импликацией и коимпликацией присутствует произведение - бинарная связка •. Система NL, являющаяся вариантом неассоциативного синтаксического исчисления Ламбека [Lambek 1961], имеет следующие примитивные стрелки, т.е. аксиомы, для каждого А и В:

а также следующие правила вывода:

Можно рассмотреть также расширения NL, получающиеся путем добавления следующих примитивных стрелок:

Опуская нижние индексы, мы получаем следующий список систем, допустимых для всех А, В, С:

Система AL является вариантом ассоциативного синтаксического исчисления Ламбека [Lambek 1958]. Что касается NL, то существенное отличие ее от оригинальной системы Ламбека заключается в том, что добавлены стрелки, использующие Т. Система ML отвечает релевантной логике без сокращения [Meyer McRobbie 1982], или линейной логике Жирара [Girard 1987]. (М означает здесь "мультимножество"). В М и ее расширениях связки импликации и коим- пликации становятся синонимичными, т.е. они могут быть без особых затруднений заменены на одну связку с сохранением доказуемости. Система R соответствует релевантной логике И. Е. Орлова [Орлов 1928], Чёрча и Андерсона-Белнапа, a RM соответствует "mingle''-расширению R (см. [Anderson Belnap 1975], [Dunn 1986]). Система ВСК. соответствует интуиционистской логике без сокращений [Ono Komori 1985] и J соответствует интуиционистской логике.

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

Вот как выглядит, например, простое доказательство так называемого коммутативного закона для конъюнкции:

Другим примером является доказательство ассоциативного закона аА.в.с* (А л В) л С -> А л (В л Q. Оно выглядит следующим образом:

или просто как

Позитивное интуиционистское дедуктивное исчисление представляет собой конъюнктивное импликативное дедуктивное исчисление, т.е. конъюнктивное дедуктивное исчисление (а) к языку которого добавлена бинарная операция импликации z> и (б) следующая новая стрелка и правило вывода:

Заметим, что отсюда легко можно получить следующую стрелку и правило вывода :

Чтобы получить это, достаточно положить

Нетрудно также получить известные нам уже правила вывода

однако доказательство будет уже иным:

Интуиционистское дедуктивное исчисление требует помимо конъюнкции и импликации еще и наличие дизъюнкции и константы "ложь", т.е. формулы _1_ и операции v (= или) на формулах, а также следующих дополнительных стрелок:

Последнее правило может быть получено по правилу поскольку мы можем положить

Мы получаем полное классическое дедуктивное исчисление, если добавим к полному интуиционистскому дедуктивному исчислению следующую стрелку:

или равносильную ей стрелку

Напомним, что обычная теорема дедукции для логических исчислений утверждает:

В полных дедуктивных системах этот результат описывается с помощью следующего правила:

Горизонтальная черта функционирует здесь как символ дедукции, и мы получаем как бы новую форму теоремы дедукции. Она имеет дело с доказательствами из допущения х:Т-А. Иными словами, мы формируем новую дедуктивную систему с присоединенной стрелкой х; TV А и ведем речь о доказательствах ф(дг): Bh С в этой новой системе. Точнее говоря, если мы исходим из дедуктивной системы L, то новая система L(x) имеет те же самые формулы (= объекты), что и L, и ее доказательства (= стрелки) ср(х) свободно порождены доказательствами L и новой стрелкой х по соответствующим правилам вывода (= операциям). Ясно, что если L является конъюнктивно-дизъюнктивным дедуктивным исчислением (позитивным исчислением, интуиционистским исчислением, классическим исчислением), то и L(x) будет конъюнктивно-дизъюнктивным дедуктивным исчислением. Теорема дедукции в этом случае принимает следующий вид:

Теорема 1 (теорема дедукции). В позитивным, интуиционистском или классическом дедуктивном исчислении с каждым доказательством <р(х): В- С из допущения х: Tf- А может быть ассоциирована стрелкаf: А л ВУ- С в L, не зависящая от х.

Доказательство. Приводим доказательство для позитивного исчисления. Это же доказательство имеет место и для конъюнктивного исчисления, если игнорировать *. Это доказательство пригодно и для дедуктивного интуиционистского или классического исчисления, когда дополнительная структура представлена преимущественно в виде стрелок, а не в виде правил вывода.

Будем писать /= кх€А <р(х), где нижний индекс хеА указывает, что х имеет тип А. Заметим, что для каждого доказательства ф(лг): В- С допущение*: TV А должно иметь одну из следующих форм:

Во всех случаях i(x) и х(*) являются более краткими доказательствами, чем ф(*), и мы определяем индуктивно:

где ola.b.c' (АаВ) лС'ь Аа(В лС") есть доказательство ассоциативности.

Поскольку речь идет об индукции по длине доказательства <р(*), то формально можно было бы определить эту длину как 0 в случаях (i) и (ii), как сумму длин %(*) и у(*) плюс один в случаях (iii) и (iv), и как длину /(*) плюс один в случае (v). ?

Теорему дедукции можно сформулировать для позитивного интуиционистского дедуктивного исчисления в более общем виде следующим образом:

Теорема 2 (теорема дедукции). В позитивным интуиционистском дедуктивном исчислении с каждым доказательством (f{x): В- Сиз допущения х: Th А может быть ассоциирована стрелкаf (Dz> А) л ВС, не зависящая от х.

Доказательство. Записывая/= р* <р(х), положим: где vp(jc): В'лВ"- С. я

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