,
кафедра философии естественных факультетов,
ассистент
О дедуктивной эквивалентности систем натурального вывода с зависимостями и натурального субординатного вывода (для классической логики высказываний[1]).
Натуральные системы с зависимостями были построены и представляют собой оригинальный вариант так называемых «естественных» исчислений. Данные системы очень удобны, прежде всего, для решения проблем дедукции в релевантных и модальных логиках, где присутствует большое число ограничений на структуру вывода, а также для работы в классическом исчислении предикатов, где они позволяют избежать весьма трудоемких понятий абсолютно и относительно ограниченной переменной.
Натуральные субординатные исчисления высказываний и предикатов представляют вывод в виде частично упорядоченной древесной структуры – главного и вспомогательного подвыводов. Указанные исчисления также имеют свои преимущества, особенно при работе в классической логике высказываний, в силлогистических натуральных исчислениях: например, простое понятие вывода, отсутствие непрямого правила удаления дизъюнкции и т. п. Т. е. данные исчисления удобны там, где на формулы вывода не требуется налагать слишком большое число ограничений, как это происходит, например, при дедукции в релевантных системах; в противном случае за соблюдением всех этих ограничений довольно сложно следить.
Таким образом, каждая из систем имеет свои методологические и дедуктивные преимущества.
Целью данной работы является доказательство дедуктивной эквивалентности указанных систем, а также формулировка алгоритмов перестройки натурального субординатного вывода для классической логики высказываний в натуральный вывод с зависимостями и обратно через доказательство факта о погружаемости натурального субординатного вывода в систему натурального вывода с зависимостями и наоборот.
Для начала приведем формулировки субординатного натурального исчисления и натурального исчисления с зависимостями для КЛВ.
Субординатный натуральный вывод для КЛВ.
Непрямые правила вывода:
(1) 
, где С – последнее допущение в выводе; все формулы, начиная с C и заканчивая предшественником С⊃B, должны быть исключены из дальнейшего построения вывода; обозначать исключение формул будем с помощью пунктирных линий.
(2) 
, где С – последнее допущение в выводе; все формулы, начиная с C и заканчивая предшественником ØС, должны быть исключены из дальнейшего построения вывода.
Прямые правила вывода:
(3) 
(4) 
(5) 
(6) 
(7) 
(8)
(9) 
(10) 
Натуральный вывод с зависимостями для КЛВ.
(1) 
, где А – любое имеющееся в выводе допущение.
(2) 
, где А – любое имеющееся в выводе допущение.
(3) 
(4) 
(5) 
(6) 
(7) 
(8) 
(9) 
(10) 
Перед тем, как сформулировать теоремы о погружении, докажем вспомогательную теорему о дедуктивной эквивалентности прямого и непрямого правил удаления дизъюнкции.
Теорема 1. Правила исключения дизъюнкции (8) и (8’) дедуктивно эквиваленты, как в субординатном натуральном исчислении, так и в натуральном исчислении с зависимостями для КЛВ.
Данная теорема вытекает из следующих двух Лемм.
Лемма 1. Все, что можно доказать с помощью правила (8) в натуральном исчислении с зависимостями, можно доказать при помощи правила (8’), и обратно.
Так как мы начинаем работу в исчислении с зависимостями, переформулируем правило (8’) как:
Докажем сначала первое утверждение Леммы 1. Обозначим его как (a).
Доказательство проведем методом возвратной математической индукции по длине вывода.
Индуктивное допущение. Пусть наше утверждение справедливо для всех формул с номером, строго меньшим, чем n. Покажем, что оно справедливо и для формулы с номером n.
По условию Леммы 1 (а), на шаге n некоторая формула С была получена по правилу (8), т. е. наш вывод имеет вид (обозначим данный вывод как В1):
j. A∨B [Γ]
m. C[A, Γ1]
l. C[B, Γ2]
n. C[Γ,Γ1,Γ2], где j, m,l < n. -∨e: j, m, l
Перестроим теперь вывод следующим образом (и обозначим полученный вывод как В2):
j. A∨B [Γ]
m. C[A, Γ1]
l. C[B, Γ2]
l+1. A⊃C [A, Γ1\A] = [Γ1] - ⊃i: m.
l+2. B⊃C [A, Γ2\A] = [Γ2] - ⊃i: l.
l+3. С [l+3] –доп.
l+4. A [l+4] –доп.
l+5. B [Γ, l+4]-∨e (8’): j, l+4
l+6. C [Γ, l+4, Γ2]- ⊃i: l+2, l+5
l+7. A [Γ, l+4, Γ2, l+3\l+4] =[Γ, Γ2, l+3]-i: l+3,l+6
l+8. A-[Γ, Γ2, l+3]-e: l+7
l+9. C [Γ, Γ2, l+3, Γ1] -⊃e: l+1, l+8
l+10.C [Γ, Γ2, l+3, Γ1\l+3] = [Γ, Γ2, Γ1]- i:l+9, l+3
l+11. C [Γ, Γ2, Γ1] - e: l+10
В результате мы получили формулу C с теми же характеристиками зависимости, как и при применении правила (8) (см. вывод В1). Лемма 1 (a) справедлива и для шага n.
Индуктивный переход обоснован.
Леммы 1 (а) справедлива для всякого n.
Таким образом, мы можем перестроить вывод, заменяя все применения правила (8) на вывод В2, т. е. заменяя все выводы вида В1 на выводы вида В2.
В результате данных замен вывод сохранит все свои метатеоретические свойства.
Докажем обратное утверждение Леммы 1. Обозначим его как (b).
Доказательство проведем методом возвратной математической индукции по длине вывода.
Индуктивное допущение. Пусть наше утверждение справедливо для всех формул с номером, строго меньшим, чем n. Покажем, что оно справедливо и для формулы с номером n.
По условию Леммы 1 (b), на шаге n некоторая формула С была получена по правилу (8’), т. е. наш вывод имеет вид (обозначим данный вывод как В1’):
j. A∨B [Γ]
m. A [Γ1]
n. B [Γ, Γ1], где j, m, < n. -∨e: j, m
Перестроим теперь вывод следующим образом (и обозначим полученный вывод как В2’):
j. A∨B [Γ]
m. A [Γ1]
m+1. A[m+1] –доп.
m+2. B [m+2] – доп.
m+3. B [Γ1, m+1\m+2] = [Γ1, m+1] - i: m, m+1
m+4. B[Γ1, m+1] - e: m+3
m+5. B[m+5] – доп.
m+6. B[Γ, Γ1] - ∨e (8): j, m+4, m+5
В результате мы получили формулу B с теми же характеристиками зависимости, как и при применении правила (8’) (см. вывод В1’). Лемма 1 (b) справедлива и для шага n.
Индуктивный переход обоснован.
Лемма 1 (b) справедлива для всякого n.
Таким образом, мы можем перестроить вывод, заменяя все применения правила (8’) на вывод В2’, т. е. заменяя все выводы вида В1’ на выводы вида В2’.
В результате данных замен вывод сохранит все свои метатеоретические свойства.
Лемма 1 доказана.
Отсюда делаем вывод, что правила (8) и (8’) дедуктивно эквиваленты в натуральном исчислении с зависимостями для КЛВ.
Аналогично проводим рассуждение и для натурального субординатного исчисления, доказывая Лемму 2.
Лемма 2. Все, что можно доказать с помощью правила (8’) в натуральном субординатном исчислении, можно доказать при помощи правила (8), и обратно.
Так как мы начинаем работу в субординатном натуральном исчислении, то переформулируем правило ∨e (8’) следующим образом[2]:
A∨B; Γ,A ⊢ C; Γ1, B ⊢ C |
Γ, Γ1 ⊢ C |
где Γ, Γ1 – множества неисключенных на момент применения правила (8’) допущений.
Теперь дополнительно переформулируем данное правило вывода с использованием Теоремы дедукции для КЛВ:
A∨B; Γ ⊢ A⊃C; Γ1 ⊢ B⊃C |
Γ, Γ1 ⊢ C |
В дальнейшем будем использовать правило (8’) именно в последней формулировке.
Докажем сначала первое утверждение Леммы 2. Обозначим его как (a).
Доказательство проведем методом возвратной математической индукции по длине вывода.
Индуктивное допущение. Пусть наше утверждение справедливо для всех формул с номером, строго меньшим, чем n. Покажем, что оно справедливо и для формулы с номером n.
По условию Леммы 2 (а), на шаге n некоторая формула С была получена по правилу (8’), т. е. наш вывод имеет вид (обозначим данный вывод как D1):
j. A∨B
|+m. A
|.
|.
|.
|mi. C
mi+1. A⊃C - i⊃:mi
|+mi+2. B
|.
|.
|.
|m+2+j. C
m+j+3. B⊃C - i⊃: m+2+j
m+j+4 = n. C - ∨e: j, mi+1, m+j+3
Перестроим теперь вывод следующим образом c использованием правила (8) (и обозначим полученный вывод как D2):
j. A∨B
|+m. A
|.
|.
|.
|mi. C
mi+1. A⊃C - i⊃:mi
|+mi+2. B
|.
|.
|.
|m+2+j. C
m+j+3. B⊃C - i⊃: m+2+j
|+m+j+4.C – доп.
||+m+j+5.A – доп.
||m+j+6. B - ∨e:j, m+j+5
||m+j+7.C - ⊃e: m+j+3, m+j+6
|m+j+8.A - Øi: m+j+4, m+j+7
|m+j+9. A - Øe: m+j+8
|m+j+10. C - ⊃e: mi+1, m+j+9
m+j+11. ØØC – Øi: m+j+4, m+j+10
m+j+12. C - Øe: m+j+11
Формула С лежит в том же подвыводе, что и формулы A∨B, A⊃C, A⊃B, как и при применении правила (8’) (см. вывод D1). Лемма 2 (a) справедлива и для шага n.
Индуктивный переход обоснован.
Лемма 2 (a) справедлива для всякого n.
Таким образом, мы можем перестроить вывод, заменяя все применения правила (8’) на вывод D2, т. е. заменяя все выводы вида D1 на выводы вида D2.
В результате данных замен вывод сохранит все свои метатеоретические свойства.
Докажем обратное утверждение Леммы 2. Обозначим его как (b).
Доказательство проведем методом возвратной математической индукции по длине вывода.
Индуктивное допущение. Пусть наше утверждение справедливо для всех формул с номером, строго меньшим, чем n. Покажем, что оно справедливо и для формулы с номером n.
По условию Леммы 2 (b), на шаге n некоторая формула С была получена по правилу (8), т. е. наш вывод имеет вид (обозначим данный вывод как D1’):
j. A∨B
m.ØA
n. B - ∨e: j, m; j, m < n
Перестроим теперь вывод следующим образом c использованием правила (8’) (и обозначим полученный вывод как D2’):
j. A∨B
m.ØA
|+m+1.A – доп.
||+m+2.ØB– доп.
|m+3. ØØB– Øi: m, m+1
|m+4. B– Øe: m+3
m+5. A⊃B - ⊃i: m+4
|m+6. B– доп.
m+7. B⊃B - ⊃i: m+6
m+8. B - ∨e: j, m+5, m+7
Формула В лежит в том же подвыводе, что и формулы A∨B, ØA, как и при применении правила (8) (см. вывод D1’). Лемма 2 (b) справедлива и для шага n.
Индуктивный переход обоснован.
Лемма 2 (b) справедлива для всякого n.
Таким образом, мы можем перестроить вывод, заменяя все применения правила (8) на вывод D2’, т. е. заменяя все выводы вида D1’ на выводы вида D2’.
В результате данных замен вывод сохранит все свои метатеоретические свойства.
Лемма 2 доказана.
Отсюда делаем вывод, что правила (8) и (8’) дедуктивно эквиваленты в натуральном субординатном исчислении для КЛВ.
Поэтому автоматически будет справедлива Теорема 1.
В силу Теоремы 1 переформулируем исчисление с зависимостями, заменив правило (8) на правило (8’). Таким образом, при классической интерпретации дизъюнкции данные правила взаимозаменимы.
Теперь сформулируем алгоритм перестройки произвольного натурального вывода в соответствующий ему натуральный вывод с зависимостями. Перестройка осуществится таким образом, что изменения не будут вноситься в саму последовательность формул (она сохранит инвариантность).
Для придания нашему результату строгости докажем Теорему 2.
Теорема 2. Всякий завершенный[3] натуральный субординатный вывод погружается в систему натурального вывода с зависимостями.
Докажем данный факт методом возвратной математической индукции по длине вывода.
Индуктивное допущение. Пусть наша Теорема справедлива для всех формул с номером, строго меньшим, чем n. Покажем, что она справедлива и для формулы с номером n.
Доказательство будет конструктивно и, по сути, будет являться алгоритмом перестройки произвольного натурального субординатного вывода в натуральный вывод с зависимостями.
Доказательство базируется на демонстрации того факта, что указанная перестройка полностью сохраняет определение натурального вывода с зависимостями и натурального субординатного выводов, т. е. на каждом шаге данной перестройки у нас будет получаться в точности натуральный вывод с зависимостями (т. е. мы последовательно показываем, что каждый шаг полученного вывода соответствует определению вывода в системе натурального субординатного вывода с зависимостями), и обратно.
Так как в Теореме 2 речь идет о погружении, то нам надо доказать и обратное утверждение: полученный натуральный вывод с зависимостями перестраивается обратно в натуральный субординатный вывод, совпадающий с исходным. Доказательство этого утверждения проведем чуть позже (оно будет почти автоматическим).
Теперь обоснуем индуктивный переход для первой части Теоремы 2.
Проведем данное обоснование разбором случаев.
Случай 1. Пусть на шаге n у нас имеется посылка (мы имеем дело не с теоремой, а выводимостью).
n. A – пос. (Перестраиваем вывод) n. A[∅]– пос.
Таким образом, на шаге n мы получили в точности натуральный вывод с зависимостями – его определение полностью сохранено, данный шаг подпадает под определение вывода в указанной системе, он полностью в рамках разрешенных в ней действий (понимание натурального вывода как совокупности разрешенных действий принадлежит – см. [5]; мы ведем себя в точности так, как в данной системе дозволено).
Случай 2. Пусть на шаге n у нас имеется допущение. (Так как мы последовательно анализируем завершенный натуральный субординатный вывод, то все допущения у нас уже исключены, и рядом с каждым допущением у нас имеется набор черточек[4], число которых показывает степень вложенности подвывода, открываемого данным допущением, в главный подвывод. При перестройке в НВЗ (натуральный вывод с зависимостями) мы стираем эти черточки, но запоминаем их число для каждой исключенной формулы и записываем его в некоторое невидимое «поле» для перестроенной формулы: данная метахарактеристика понадобится нам при обратной перестройке вывода для доказательства второй части теоремы)
|… {k раз, 1 ≤ k ≤ l, где l – общее число допущений в выводе } n. A – доп. (Перестраиваем вывод) \k\ – невидимо n. A[n] – доп.
На шаге n мы опять получили именно то, что дозволено в системе натурального вывода с зависимостями, вновь получив вывод в точности в данном исчислении.
Случай 3. На шаге n мы получили некоторую формулу А по одному из прямых правил вывода. Здесь нам надо рассмотреть несколько подслучаев по числу прямых п. в., однако в целях экономии места мы ограничимся анализом применения правила &i. Другие подслучаи рассматриваются совершенно аналогично.
|…{k раз, 0 ≤ k ≤ l, где l – общее число допущений в выводе} n. A – &i:j, m (Перестраиваем вывод) \k\ – невидимо n. A[Γ, Γ1] – &i:j, m, где Γ, Γ1 – характеристики зависимости для формул с номерами j, m, соответственно. Мы получили их по ИД, так как j, m < n, и для формул-посылок перестройка уже успешно проведена, так что мы можем смело воспользоваться их характеристиками зависимости, в полном соответствии с определением правила &i для данной системы.
Таким образом, на шаге n у нас опять полностью сохраняется как определение вывода для натуральной системы с зависимостями, так и применение прямых правил в ней.
Случай 4. На шаге n мы получили некоторую формулу А по одному из непрямых правил вывода. Здесь нам надо рассмотреть несколько подслучаев по числу непрямых п. в., однако в целях экономии места мы ограничимся анализом применения правила ⊃i. Подслучай для Øi рассматривается совершенно аналогично.
|…{k раз, 0 ≤ k ≤ l-1, где l – общее число допущений в выводе} n. A ≗ С⊃B –⊃i: j (Перестраиваем вывод) \k\ – невидимо n. A≗ С⊃B [Γ\С] – ⊃i: j, где Γ– характеристика зависимости для В, а С – характеристика зависимости для С, соответственно. Мы получили их по ИД, так как j, №(С) < n. В силу ИД, мы можем смело воспользоваться данными характеристиками в точном соответствии с определением правила ⊃i для НВЗ.
Таким образом, на шаге n у нас опять полностью сохраняется как определение вывода для натуральной системы с зависимостями, так и применение непрямых правил в ней.
Индуктивный переход обоснован.
Утверждение справедливо для всякого n.
Первая часть Теоремы 2 доказана.
Доказательство второй части Теоремы 2 также проведем возвратной математической индукцией по длине вывода (номеру формулы) в системе натурального вывода с зависимостями, поменяв местами левую и правую части в рассуждении по случаям (мы убираем характеристики зависимости для посылок, допущений и соответствующих правил вывода и каждой формуле приписываем соответствующее число черточек k). Определение натурального субординатного вывода у нас также будет сохраняться на каждом шаге.
(При анализе применения непрямых правил вывода соответствующей формуле будет приписываться на одну черточку меньше, что полностью соответствует определению вывода в субординатных системах. Таким образом, исключение допущений в субординатных системах и теоретико-множественное вычитание характеристики зависимости допущения являются своеобразными синтаксическими «синонимами».)
Заметим, что в субординатный вывод мы перестраиваем не произвольный натуральный вывод с зависимостями некоторой формулы А, а вывод, полученный посредством перестройки соответствующего субординатного вывода. Таким образом, во второй части Теоремы 2 исследуется обратная перестройка из результирующего вывода в исходный.
Теорема 2 доказана.
Таким образом, имеет место погружаемость субординатного натурального вывода для КЛВ в систему натурального вывода с зависимостями.
Аналогичным образом мы могли бы проработать и системы с непрямым правилом удаления дизъюнкции. Основываясь на результате Теоремы 1, мы бы установили необходимое соответствие и провели соответствующие замены для правила ∨e. Подробный анализ данного факта мы предоставляем читателю.
К тому же, мы предъявили алгоритм перестройки субординатного натурального вывода в натуральный вывод с зависимостями, который может быть реализован за полиномиальное время детерминированной машиной Тьюринга[5].
Продемонстрируем на примере, как он работает.
Пример 1.
|1.(P⊃Q) ⊃P – доп. /1/ 1.(P⊃Q) ⊃P [1]– доп.
||2.P – доп. /2/ 2.P [2] – доп.
|||3.P– доп. /3/ 3.P [3] – доп.
||||4.Q– доп. /4/ 4.Q [4]– доп.
|||5.Q –i: 2,3 /3/ 5.Q [2,3\4] = [2,3] –i: 2,3
|||6.Q –e: 5 /3/ 6.Q[2,3] –e: 5
||7.P⊃Q –⊃i: 6 /2/ 7.P⊃Q [2,3\3] = [2] –⊃i: 6
||8.P –⊃e:1,7 /2/ 8.P [2,1]–⊃e:1,7
|9.P– i: 2,8 /1/ 9.P [2,1\2] = [1] – i: 2,8
|10.P– e: 9 /1/ 10.P [1]– e: 9
11.((P⊃Q) ⊃P) ⊃P– ⊃i: 10 /0/ 11.((P⊃Q) ⊃P) ⊃P [∅] – ⊃i: 10
Как мы видим, определение натурального вывода с зависимостями у нас полностью сохранено на каждом шаге перестроенного вывода. Поэтому на последнем шаге у нас, согласно Теореме 2, получилась в точности та же формула-теорема, что и на последнем шаге исходного вывода. Обратная перестройка также верна.
Что касается Теоремы 3 о погружении произвольного натурального вывода с зависимостями в субординатный натуральный вывод, то ее доказательство не столь просто хотя бы в силу того факта, что далеко не каждый натуральный вывод с зависимостями может быть перестроен в субординатный натуральный вывод без изменения последовательности формул вывода, одной лишь манипуляцией с характеристиками зависимостями и черточками – степенями субординатных подвыводов. Например,
Пример 2.
1. P [1] – доп.
2. Q[2] – доп.
3. R[3] – доп.
4. R⊃R [∅]–⊃i: 3
5.P⊃( R⊃R) [∅]–⊃i:4
не может быть непосредственно перестроен в СНВ (субординатный натуральный вывод), так как получение формулы P⊃( R⊃R) происходит с «перескакиванием» через допущение №2 и нарушает определение вывода в субординатной системе, не соответствует разрешенным в ней действиям. (Здесь для перестройки в СНВ необходимо, к тому же, удалить второе допущение, и правомерность данных действий также надо обосновывать).
Можно привести и более сложный пример.
Пример 3.
1.P&P [1] – доп.
2. P [1] - &e: 1
3.P [1] - &e: 1
4. Q [4] – доп.
5. Q [1] – i: 2,3
6. (P&P)⊃ Q [∅]–⊃i: 5
7. Q⊃((P&P)⊃ Q) [∅]–⊃i: 6
В данном примере допущение №4 используется дважды (второй раз – при введении импликации), хотя оно уже было отработано при применении правила i. В СНВ такие действия запрещены. Для перевода данного примера в СНВ необходимо ввести допущение Q в вывод еще раз, скажем, с помощью встраивания дополнительного шага № 7 (после 6-ого; 7-ой шаг автоматически становится 8-ым).
Теперь перейдем к доказательству Теоремы 3.
Теорема 3. Любой вывод в натуральном исчислении с зависимостями для КЛВ, в котором последняя формула имеет пустую характеристику зависимости, погружается в систему натурального субординатного вывода (для КЛВ).
Доказательство проведем методом возвратной математической индукции по числу случаев, когда невозможна непосредственная, без изменения самой последовательности формул перестройка вывода с зависимостями в натуральный субординатный вывод.
Проанализируем последовательно все эти случаи. Доказательство того, что в каждом из них последовательность формул вывода успешно перестраивается в СНВ, будет доказательством базиса указанной индукции (Теорему 3 лучше доказывать с использованием базиса).
Существует всего 4 базовых случая, при которых невозможна непосредственная перестройка в СНВ, так как, в противном случае, она нарушила бы определение натурального субординатного вывода. Все другие случаи представляют собой лишь комбинацию произвольного, но конечного, по определению вывода, числа базовых.
Итак, Случай 1.
Случай 1. В выводе использовано т. н. лишнее допущение, которое не задействуется при применении непрямых правил вывода (см. Пример 2, допущение №2). (Заметим, что в общем случае избыточные допущения могут быть на любом шаге вывода и в любом количестве). Непосредственная перестройка такого вывода в СНВ невозможна, так как это противоречит определению СНВ, согласно которому все введенные в вывод допущения должны быть исключены.
Перестроим данный базовый вывод в промежуточный вывод с зависимостями, который будет дедуктивно эквивалентен исходному выводу с зависимостями, но, в то же время, будет подпадать под условие Теоремы 2 и конструктивно перестраиваться в дедуктивно эквивалентный ему субординатный вывод. По транзитивности отношения дедуктивной эквивалентности, исходный вывод с зависимостями будет дедуктивно эквивалентен полученному субординатному выводу, а значит, будет погружаться в него.
Для доказательства Случая 1 нам необходимо вспомнить, что запись A[Γ] есть не что иное, как Γ ⊢ А (по определению). Итак, по условию Случая 1, Γ, Γ1 ⊢ А, где Γ1 как раз и есть то самое избыточное допущение. Но раз оно избыточное, то мы имеем полное право утверждать, что Γ ⊢ А. Обратное утверждение от Γ ⊢ А к Γ, Γ1 ⊢ А справедливо в силу свойств классической выводимости. Следовательно, в Случае 1 Γ, Γ1 ⊢ А ⇔ Γ ⊢ А и натуральный вывод с зависимостями перестраивается в дедуктивно эквивалентный ему вывод с зависимостями без избыточного допущения. Перестроенный таким образом вывод уже полностью подпадает под условие Теоремы 2.
Случай 2. При применении непрямых правил вывода допущения использовались в порядке, не допустимом для систем СНВ. Приведем пример.
Пример 4.
1. P [1] – доп.
2. Q[2] – доп.
3. R[3] – доп.
4. R⊃R [∅]–⊃i: 3
5. P⊃( R⊃R) [∅]–⊃i:4
6. Q⊃( P⊃( R⊃R)) [∅]–⊃i:4
Здесь в качестве антецедента импликации было взято сначала допущение №1, потом допущение №2. В системах субординатного вывода непрямые правила должны применяться строго к последнему допущению в выводе, произвольный порядок недопустим. Заметим, что в Случае 2 порядок может быть нарушен только для двух допущений, так как для произвольного их числа (всегда конечного, по определению вывода) справедливость дедуктивно-эквивалентной перестройки доказывается с использованием индуктивного допущения.
Пусть по условию Случая 2, Г, Г1, Г2⊢ A, где допущения Г1, Г2 записаны в том порядке, в каком их ввели в исходный натуральный вывод с зависимостями. По условию, данный порядок не соответствует допустимому для СНВ. Тогда требуемый порядок можно создать путем перестановки допущений: Г, Г1, Г2 ⊢ A ⇔ Г, Г2, Г1 ⊢ A. Полученный промежуточный вывод будет дедуктивно эквивалентен исходному в силу свойств классической выводимости, и таким образом полученный вывод будет подпадать под условие Теоремы 2 и благополучно перестраиваться в СНВ.
Случай 3. Непрямые правила вывода применялись к допущению, к которому уже было применено то или иное непрямое п. в. (см. Пример 3) и которое поэтому не может использоваться при работе в СНВ, так как должно быть исключено из процесса дедукции.
Как же перестроить вывод такого рода в соответствующий промежуточный подвывод? Нужно ввести еще раз указанное допущение. Вставка должна производиться перед шагом, где начинает использоваться указанное допущение. Затем применение непрямого правила вывода идет с ориентировкой на добавленное допущение – т. е. относительно других шагов мы должны изменить только их номера (и числовые значения характеристик зависимости для соответствующих формул).
Для Примера 3: 7. Q[7] – доп. 8. Q⊃((P&P)⊃ Q) [∅]–⊃i: 7.
Строгое доказательство правомерности такой перестройки таково.
По условию, Г, Г1 ⊢ A, где Г1 – то самое повторно использованное допущение. Тогда по свойствам классической выводимости Г, Г1 ⊢ A ⇔ Г, Г1, Г1 ⊢ A (продублировали допущение; обратный переход – устранили введенное допущение: в системах с зависимостями мы можем это сделать). Полученный промежуточный вывод будет дедуктивно эквивалентен исходному, а также будет подпадать под условие Теоремы 2.
Случай 4. В процессе дедукции в системах с зависимостями могло повторно использоваться не только само допущение, но и полученные с его помощью формулы (формулы из исключенного подвывода, по терминологии СНВ). Правда, в этом случае, «породившее» их допущение (т. е. то допущение, в чьем подвыводе они лежат) также обязательно должно использоваться повторно, иначе, по определению вывода в системах с зависимостями, мы не получим в итоге формулу с пустой характеристикой зависимости. (А погружение таких подвыводов в СНВ не имеет для нас смысла.)
Заметим, что сначала используются формулы, полученные с помощью указанного допущения, а потом само допущение, иначе автоматически будет иметь место Случай 3 (т. е. у нас уже имеет место комбинация случаев, где Случай 3 – основной).
Пример 5.
1.P&P [1] – доп.
2. P [1] - &e: 1
3.P [1] - &e: 1
4. Q [4] – доп.
5. Q∨Q [4] – ∨i: 4
6. Q [1] – i: 2,3
7. (P&P)⊃ Q [∅]–⊃i: 6
8. ((P&P)⊃ Q)&(Q∨Q) [4] – &i: 5, 7
9. Q⊃ (((P&P)⊃Q)&(Q∨Q)) [∅]–⊃i: 8
Здесь в дальнейшем построении вывода участвовала формула Q∨Q, которая в системе СНВ уже должна быть исключена из процесса дедукции, а потом и допущение, от которого она зависела.
Для перестройки в промежуточный подвывод нужно ввести еще раз требуемое допущение, а также формулы, которые были получены с его помощью и которые использовались в дальнейшей дедукции. Вставка данного фрагмента вывода должна производиться перед шагом, где начинают использоваться формулы, полученные с помощью данного допущения. Затем применение правил вывода идет уже к новым, добавленным формулам, а не к старым, исключенным – т. е. относительно других шагов мы должны изменить только их номера и номера формул в анализе (и числовые значения характеристик зависимости для соответствующих формул). Т. е. для Примера 5 мы должны после шага 7 вставить дополнительно шаги: 8. Q [7] – доп. 9. Q∨Q [7] - ∨i: 8. Тогда: 10. ((P&P)⊃Q)&(Q∨Q) [7]– &i: 7, 9 11. Q⊃ (((P&P)⊃Q)&(Q∨Q)) [∅]–⊃i: 10.
Для Случая 4 строго рассуждаем следующим образом. По условию: Г, Г1 ⊢ A; Г, Г1 ⊢ Г2,.. Гn; следовательно, Г, Г1, Г2,.. Гn ⊢ A (по условию и свойствам классической выводимости). Тогда по свойствам классической выводимости Г, Г1, Г2,.. Гn ⊢ A ⇔ Г, Г1, Г2,.. Гn, Г1, Г2,.. Гn ⊢ A (продублировали не только допущение, то и необходимый фрагмент вывода; обратный переход – устранили продублированные формулы: в системах с зависимостями мы можем это сделать).
Базис доказан.
Индуктивное допущение. Теорема 3 справедлива для числа случаев, с порядковым номером меньшим, чем n.
Покажем, что она справедлива и для n-ного случая.
В случае n может иметь место одна из уже рассмотренных нами четырех возможностей. Таким образом, с учетом индуктивного допущения, индуктивный переход доказывается совершенно алогично базису.
Теорема 3 справедлива для любого числа таких случаев и поэтому – для любого вывода.
Действительно, для любого числа «нестыковок» можно, последовательно применяя «Случаи сведения» 1 – 4, привести за конечное число шагов (в силу конечности любого вывода и, как следствие, числа «нестыковок») исходный вывод с зависимостями к дедуктивно эквивалентному ему промежуточному выводу с зависимостями, в котором уже не будет ни одной «нестыковки».
Т. о., мы перестраиваем произвольный натуральный вывод с зависимостями в промежуточный натуральный вывод с зависимостями, который, уже по Теореме 2, перестраивается в СНВ.
Затем, по свойствам отношения дедуктивной эквивалентности, мы можем утверждать, что произвольный натуральный вывод с зависимостями дедуктивно эквивалентен соответствующему ему натуральному субординатному выводу.
Важное замечание. Невидимый параметр k, определяющий степень вложенности произвольного подвывода в главный (в СНВ), определяется следующим образом для каждой формулы.
В готовом промежуточном выводе полагаем параметр k для каждой формулы равным нулю. Затем последовательно пробегаем по всему выводу и от каждого допущения вплоть до формулы-предшественника результата применения непрямого п. в., опирающегося на данное допущение, увеличиваем k ровно на 1. В конце нашего «пробега» значения k для каждой формулы будут равны степени вложенности соответствующих им подвывовов в главный (в субординатном натуральном исчислении). Доказательство данного факта мы предоставим читателю.
Т. о., мы можем с полным правом применить Теорему 2 и погрузить произвольный вывод с зависимостями в систему натурального субординатного вывода.
Теорема 3 доказана.
В силу конструктивности доказательства, Теорема 3 также представляет собой алгоритм перестройки произвольного вывода с зависимостями в СНВ.
По Теоремам 2 и 3 и транзитивности отношения дедуктивной эквивалентности, система натурального вывода с зависимостями и субординатный натуральный вывод дедуктивно эквиваленты для КЛВ.
На основе данного исследования можно построить натуральные исчисления с зависимостями и для всех систем негативной силлогистики, рассмотренных в [6].
Литература:
1. , Маркин логики// Учебник. Москва, ИНФРА-М, 2002.
2. Ивлев . Учебник// Москва, «Проспект», 2009.
3. Войшвилло -методологические аспекты релевантной логики. Москва, Издательство Московского Университета, 1988.
4. Войшвилло логика: классическая и релевантная. Москва, "Высшая школа", 1989.
5. Катречко вариант систем натурального вывода. http://www. *****/library/katr/logic/logic_natural_katr. doc
6. Красненкова поиска вывода для систем негативной силлогистики. Диссертация на соискание ученой степени кандидата философских наук. Специальность 09.00.07 – Логика. Москва, 2009.
[1] Далее – КЛВ.
[2] Данная формулировка для непрямого правила удаления дизъюнкции приведена в [2, стр.70].
[3]Под завершенным выводом будем понимать вывод, в котором исключены все введенные в него допущения.
[4] Если заменить пунктирные линии более традиционными для натурального субординатного вывода прямыми линиями (либо квадратными скобками), очерчивающими подвыводе как некоторые совокупности формул, то ни определение вывода, ни мощность k от этого не изменятся.
[5] Данное утверждение временно оставим без доказательства, так как оно выходит за рамки обозначенной темы.
