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

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

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


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

Дедуктивные импликативные системы

Подразумевая под объектами дедуктивной системы формулы, под стрелками - доказательства, и под операциями на стрелках - правила вывода, мы получаем импликативное исчисление, если мы допускаем, что существует формула Т (= истина) и бинарная операция о (= “если,...,то”) для образования импликации A z> В из двух данных формул А а В. Кроме этого, мы вводим следующие два правила вывода:

Нетрудно видеть, что наше импликативное исчисление соответствует системе / [Карпенко 1993, с.225], ибо:

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

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

Подобные формулировки дают нам дедуктивные системы, которые мы будем называть гильбертовскими системами (см. [Dosen 1996]), а стрелки типа Tl - гильбертовскими стрелками.

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

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

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

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

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

Разрабатывая структуру импликативных систем, мы можем добавить к /Я-импликативному исчислению аксиомы, являющиеся дедуктивными аналогами импликативных логических аксиом С, Wy К

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

. г— —1

(достаточно положить/т= (у*Вс / )s)

(достаточно положить fw= (wAB f )s)

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

если А/В- Су то А- В z> С.

В случае чисто импликативных систем теорема дедукции приобретает несколько иную форму, поскольку в их языке отсутствует связка конъюнкции.

Пусть S будет представлять собой некоторую дедуктивную импликативную систему. Обозначим как S[x] некоторое расширение S за счет добавления к ней новой аксиомы - стрелки х: Тн А, которую мы (следуя терминологии Дж.Ламбека) назовем индетер- минантом (неопределенной стрелкой). Очевидным образом стрелка х не будет принадлежать системе S, хотя и Т и А принадлежат системе S в качестве ее объектов. Логиков обычно интересует случай, когда новая стрелка х: Тн А такова, что в S нет более стрелок подобного типа (т.е. отсутствуют допущения). Тем не менее, не следует исключать такой ситуации, когда в S уже есть такие стрелки, что может случиться тогда, когда вводится новое доказательство уже известной теоремы.

Рассмотрим полученную дедуктивную импликативную систему S[x], Ее объекты совпадают с объектами S, в то время как стрелки отличаются от стрелок S за счет наличия новой стрелки х и всех стрелок, полученных из нее с помощью операций на стрелках. Обычная теорема дедукции или теорема функциональной полноты в импликативной системе устанавливает, что

Теорема дедукции. Для каждой стрелки типа Tl- В в S[x], где х: Тн А, существует стрелка типа А Н В из S.

Иначе это можно переформулировать следующим образом:

С каждым доказательством <р(х): Тн В из допущения х:ТН А может быть ассоциирована стрелка типа Ah В, не зависящая от х.

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

Более общая (и тем самым более слабая) формулировка выглядит следующим образом:

С каждым доказательством ф(Х|,...,хя).’Т1-В из допущений xi.Tb.4i,..., хт:Т-Ат может быть ассоциирована стрелка Т(- А з(... z>(A,„z> В)...), не зависящая от Xj, ...,хт.

(см. в этой связи [Сшту 1954]).

Ее также условно можно изобразить в виде следующего дерева доказательства:

Для случая стрелки типа В- С теоремы дедукции выглядит следующим образом:

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

Слабая теорема дедукции. С каждым доказательством (p(xi,...prm): В-С из допущений Xi:TH4|,..., хт:7- Ат может быть ассоциирована стрелка ТЬ А z>(... э (8 э С))...), зависящая от В и С, но не зависящая от Xi, ...,хт.

Теорему дедукции можно доказать для IBCWK- импликативного исчисления (чего нельзя сделать, например, для /В-импликативной системы).

Теорема 1 (теорема дедукции). В IBCWK-импликативиом исчислении для каждого доказательства ф(х): В- С из допущения x:Th- А существует стрелка f: Т э(8эС), не зависящая от х.

Доказательство. Положим / = &*е/<ф(х)[1]. Каждое доказательство <р(х): В— С из допущения х: Тн А должно иметь одну из следующих форм:

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

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

Здесь и далее ? означает конец доказательства.

Для /В-импликативной системы можно доказать следующую «обобщенную» слабую теорему дедукции:

Теорема 2 (обобщенная слабая теорема дедукции). В IB- импликативном исчислении с каждым доказательством <р(х/,...,х„): В- С из допущений х‘. Ть Аь ..., х„: TI- Ат может быть ассоциирована стрелка типа f: Tl- С з (,..з (С„ з зС))...), не зависящая от Х|, ... т, где Ct есть либо одно из Аь ... , Ат, либо 1В- теорема.

Доказательство. Будем писать / = кХх€ЛуХ2еАг...,Хт€Атср(лги ... уХт)у где индекс хеА указывает, что х имеет тип А. Заметим, что каждое доказательство jcm): В- С из допущений х: Tl- A[f ..., хт: Ть- Ат должно иметь одну из следующих форм:

Во всех случаях х(хи ••• r*m) и |/(xi,... уХт) являются более краткими доказательствами, чем ф(хь ... jcm), и мы определяем индуктивно:

Нетрудно заметить, что случаи (iv) и (v) отличаются только выбором С„. Далее, поскольку речь идет об индукции по длине доказательства ф(*ь ••• уХт)> то формально можно было бы определить эту длину как 0 в случаях (i) и (й), как сумму длин %(хь ... и |/(xi, ... уСт) плюс один в случае (iii) и как длину j/(xi, ... уКт) плюс один в случаях (iv) - (vi). ?

Рассмотрим теперь следующий список гильбертовских стрелок, отвечающих известным аксиомам импликативных логических исчислений:

(см. [Salto Mendez 1999]). Стрелки a9 и alO описывают логические аксиомы, известные под именем «классический закон Пирса» и «85-закон Пирса».

С помощью стрелок из этого списка мы можем сформировать дедуктивные системы, отвечающие различным импликативным фрагментам известных логик.

Если добавить к дедуктивной импликативной /5-системе стрелку

отвечающую гильбертовской стрелке al, то полученная дедуктивная импликативная /55 -система будет соответствовать импликативной минимальной логике. Добавление стрелки [У приводит также к добавлению нового правила

(достаточно положить/Ы с = (Р' / ) *).

Если добавить к дедуктивной импликативной /55-системе стрелку

отвечающую стрелке а2, то полученная система MLc^ соответствует системе расширенной минимальной логики. При этом добавляется правило

(достаточно положить/“ = (а / ) *)•

Добавление к дедуктивной системе /55'стрелки wAB превращает ее в дедуктивную релевантную импликативную систему, соответствующую импликативному фрагменту логической системы следования Т->.

Добавляя же к /55'стрелку

отвечающей гильбертовской стрелке аЗ, получаем дедуктивную импликативную систему следования без сокращения E-W~ которая соответствует импликативному фрагменту логики следования Е без сокращения. В полученной системе имеет место правило

(достаточно положить/б = (8/) *).

Добавление к IBB 'вместо стрелки 5 стрелки

соответствующей гильбертовской стрелке а4, приводит к дедуктивной системе R-W” отвечающей импликативному фрагменту релевантной логики R без сокращения. В R-W”* справедливо правило

(достаточно положить/' = (т/)г).

Дедуктивную систему Е-*, отвечающую импликативному фрагменту логики следования Е, получаем добавлением к Т”* стрелки 5, а дедуктивную систему R”*, отвечающую импликативному фрагменту релевантной логики R, получаем добавлением к Т-* стрелки т (получая и соответствующие дополнительные правила вывода).

Систему ЕМОЛ отвечающую логике следования «смешения» ЕМ, получаем теперь добавлением к Е“* стрелки

отвечающей гильбертовской стрелке а5. Это влечет за собой принятие следующего правила вывода

(достаточно положить/" = (л / ) ’)•

Дедуктивная система RM0”* (дедуктивный аналог релевантной логики R) получается при добавлении к R стрелки

отвечающей гильбертовской стрелке аб и приводящей к добавлению следующего правила вывода

(достаточно положить/® = (0 / У).

Дедуктивную модальную систему S3”* (дедуктивный эквивалент импликативного фрагмента модальной логики S3) получаем добавлением к Е“* стрелки

отвечающей гильбертовской стрелке а7 и дающей правило вывода

(достаточно положить/*?= {С, / )').

Дедуктивную модальную систему S4~* (дедуктивный эквивалент импликативного фрагмента модальной логики S4) получаем добавлением к стрелки

отвечающей гильбертовской стрелке а8 и дающей правило вывода

(достаточно положить/х= (Я. / )

Систему J-* (дедуктивный эквивалент импликативного фрагмента интуиционистской логики) мы получаем добавлением к R * стрелки к а дедуктивная модальная система S5~* получается при добавлении к Е-* стрелки

отвечающей гильбертовской стрелке а10 (Бб-закон Пирса) и порождающей правило вывода

(достаточно положить/и= (р / )*).

Наконец, дедуктивная классическая импликативная система С-* получается путем добавления к J-* стрелки Пирса

отвечающей гильбертовской стрелке а9, и правила вывода

(достаточно положить/®! = @J).

  • [1] по меткому замечания К.Дошена [Dosen 1996, р.271 ] кхйЛ представляет собойаватару ХхеА (если сравнивать кххЛ (р(х) и ХхеА.(р{х)).
 
<<   СОДЕРЖАНИЕ ПОСМОТРЕТЬ ОРИГИНАЛ   >>