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

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

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

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

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

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

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

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

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

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

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

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

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

. г— —1.

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

(достаточно положить f^w= (w_AB 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,…pr_m): В-С из допущений 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еАг}…,_Хт€Атср (лг_и … уХ_т)_у где индекс хеА указывает, что х имеет тип А. Заметим, что каждое доказательство.

jc_m): ВС из допущений х: Tl- A_[f …, х_т: Ть- А_т должно иметь одну из следующих форм:

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

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

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

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

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

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

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

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

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

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

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

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

Добавляя же к /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 ] кхйЛ представляет собойаватару ХхеА (если сравнивать кххЛ (р (х) и ХхеА.(р{х)).