VIII. Исчисления секвенций

Глава VIII. Исчисления секвенций.

Исчисление секвенций (от англ. Sequent calculus) — система формального вывода формул логики первого порядка предложенная немецким логиком Герхардом Генценом. Генценом были разработаны несколько эквивалентных вариантов исчисления секвенций.

Секвенциальные формулы представляют собой последовательность, разделенную знаком выводимости «⊦», в которой слева (в антецеденте) находится дизъюнктивная последовательность, а справа (в консеквенте, или в «сукцеденте») – конъюнктивная. В целом, секвенциальная формула выглядит следующим образом:

(a˅b˅c˅d˅…˅z) ⊦ (a˄b˄c˄d˄…˄z)

Подразумевается, что обе части уравнения эквивалентны в том смысле, что антецедент служит доказательством сукцедента, а сукцедент служит доказательством антецедента:

(a˅b˅c˅d˅…˅z) ↔ (a˄b˄c˄d˄…˄z)

Секвенция с пустым антецедентом интерпретируется как истина, а секвенция с пустым сукцедентом – как ложь. Если пустыми оказываются как антецедент, так и сукцедент — секвенция интерпретируется в качестве противоречивой:

∅ ⊦ (a˄b˄c˄d˄…˄z) – «истина»

(a˅b˅c˅d˅…˅z) ⊦ ∅ — «ложь»

∅ ⊦ ∅ — «противоречие»

Логические правила

где «t» — любая переменная (возможно «x», если «x» — свбодная переменная));

где «y» — любая новая переменная (либо уже имеющаяся перемененная «x», не связанная кванторами в Γ и ∆).

Эти две важнейшие оговорки мы объясним чуть позже на примерах.

Структурные правила:

Символы «Г», «Δ», «Σ» и «Π» означают множества формул (возможно пустые).

Читатель, вероятно, уже обратил внимание, что правила исчисления секвенций не являются чем-то принципиально новым для нас. Все эти правила (в том или ином виде) мы встречали в системе натурального вывода.

Примеры вывода.

Пусть необходимо доказать аксиому «⊦ A⊃A».

Σ_1. A ⊦ A – аксиома

Σ₂. ⊦ A⊃A – из Σ₁ по ⊃R ∎

Пусть необходимо доказать аксиому «⊦ A˅¬A».

Часто, для доказательства формулы необходимо наличие нескольких аксиом. Например, если мы доказываем формулу «A, B ⊦ A˄B», возможна следующая последовательность действий:

Σ_1. A ⊦ A – аксиома

Σ₂. B ⊦ B – аксиома

Σ₃. A, B ⊦ A˄B – из Σ₁ и Σ₂ по ˄R ∎

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

Табличная форма исчислений более распространена в практике исчисления секвенций, однако, она крайне неудобна для изложения в книжной полиграфии (по определенным техническим причинам).

Доказательство формулы «(A⊃(B˅C))⊃(((B⊃¬A)˄¬C)⊃¬A)» табличным способом:

Доказательство формулы «(A⊃(B˅C))⊃(((B⊃¬A)˄¬C)⊃¬A)» линейным способом:

Σ_1. A ⊦ A – аксиома

Σ₂. C ⊦ C — аксиома

Σ₃. B˅C ⊦ B, C – из Σ₁ и Σ₂  по ˅L

Σ_4. B˅C ⊦ C, B из Σ₃ по PR

Σ₅. B˅C, ¬C ⊦ B из Σ₄ по ¬L

Σ₆. ¬A ⊦ ¬A — аксиома

Σ₇. (B˅C), ¬C, (B⊃¬A) ⊦ ¬A — из Σ₅ и Σ₆  по ⊃L

Σ₈. (B˅C), ¬C, ((B⊃¬A)˄¬C) ⊦ ¬A – из Σ₇ по ˄L

Σ_9. (B˅C), ((B⊃¬A)˄¬C), ¬C ⊦ ¬A — из Σ₈ по PL

Σ₁₀. (B˅C), ((B⊃¬A)˄¬C), ((B⊃¬A)˄¬C) ⊦ ¬A- из Σ₉ по ˄L

Σ₁₁. (B˅C), ((B⊃¬A)˄¬C) ⊦ ¬A — из Σ₁₀ по CL

Σ₁₂. ((B⊃¬A)˄¬C), (B˅C) ⊦ ¬A — из Σ₁₁ по PL

Σ₁₃. ⊦ ¬A, A — из Σ₁ по ¬R

Σ_14. ⊦ A, ¬A — из Σ₁₃ по PR

Σ₁₅. ((B⊃¬A)˄¬C), (A⊃(B˅C)) ⊦ ¬A, ¬A — из Σ₁₄ и Σ₁₂  по ⊃L

Σ₁₆. ((B⊃¬A)˄¬C), (A⊃(B˅C)) ⊦ ¬A — из Σ₁₅ по CR

Σ₁₇. (A⊃(B˅C)), ((B⊃¬A)˄¬C) ⊦ ¬A — из Σ₁₆ по PL

Σ₁₈. (A⊃(B˅C)) ⊦ (((B⊃¬A)˄¬C)⊃¬A) — из Σ₁₇ по ⊃R

Σ_19. ⊦ (A⊃(B˅C))⊃(((B⊃¬A)˄¬C)⊃¬A) — из Σ₁₈ по ⊃R ∎

Мы специально привели достаточно сложный и длинный пример исчисления секвенций, чтобы использовать максимально большое количество правил. Разобрав каждый вывод, для студента в дальнейшем не будет сложностей с исчислением секвенций.

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

Пусть необходимо доказать формулу

«Ǝy(∀x(p(x, y))) ⊦ ∀x(Ǝy(p, (x, y)))»

Напомним, что для правил кванторов есть определенные ограничения (как и во всех остальных системах исчислений). Если для правил ∀L и ∃R ограничения несущественны, то для правил ∀R и ∃L следует помнить: получаемая переменная не должна быть связана в предыдущих выводах кванторами.

Предположим, мы хотим построить доказательство формулы вида «∃xP(x) ⊦ ∃xP(x)». Интуитивно мы понимаем, что какие бы кванторы не находились в антецеденте и сукцеденте формулы, ошибочным может быть только один вариант — «∃xP(x) ⊦ ∀xP(x)».

Начинаем, как обычно, с аксиомы:

Σ_1. P(x) ⊦ P(x) – аксиома

Σ₂. P(x) ⊦ ∃xP(x) – из Σ₁  по ∃R

Σ₃. ∃xP(x) ⊦ ∃xP(x) – из Σ₂  по ∃L

Вывод построен неверно, поскольку правило ∃L в третьем действии нарушено: мы использовали переменную «x», которая уже была связана квантором общности во втором действии. Третье действие мы могли бы завершить только так:

Σ_1. P(x) ⊦ P(x) – аксиома

Σ₂. P(x) ⊦ ∃xP(x) – из Σ₁  по ∃R

Σ₃. ∀xP(x) ⊦ ∃xP(x) – из Σ₂  по ∀L

В целом, у нас получилась правильная формула, однако мы так и не доказали искомую — «∃xP(x) ⊦ ∃xP(x)». Может быть наша ошибка заключалась в том, что мы начали не с той стороны? Попробуем еще раз:

Σ_1. P(x) ⊦ P(x) – аксиома

Σ₂. ∃xP(x) ⊦ P(x) – из Σ₁  по ∃L

Σ₃. ∃xP(x) ⊦ ∃xP(x) – из Σ₂  по ∃R

Теперь правила выполнены.

                                     Совет

Вероятнее всего, последовательность действий будет важна и для решения формулы «∃xP(x) ⊦ ∃xP(x)»:

Σ_1. P(x) ⊦ P(x) – аксиома

Σ₂. ∀xP(x) ⊦ P(x) – из Σ₁  по ∀L

Σ₃. ∀xP(x) ⊦ ∀xP(x) – из Σ₂  по ∀R

Вывод Σ₃ сделан с нарушением правила ∀R. Пробуем в другой последовательности:

Σ_1. P(x) ⊦ P(x) – аксиома

Σ₂. P(x) ⊦ ∀xP(x) – из Σ₁  по ∀R

Σ₃. ∀xP(x) ⊦ ∀xP(x) – из Σ₂  по ∀L

Теперь всё верно.

Попробуем усложнить задачу и доказать закон отрицания общеутвердительного суждения «¬∀xP(x) ⊦ ∃x¬P(x)»:

Σ_1. ¬P(x) ⊦ ¬P(x) – аксиома

Σ_2. ⊦ P(x), ¬P(x)– из Σ₁ по ¬R

Σ₃. ⊦ ∀xP(x), ¬P(x)– из Σ₂ по ∀R

Σ₄. ¬∀xP(x) ⊦ ¬P(x)– из Σ₃ по ¬L

Σ₅. ¬∀xP(x) ⊦ ∃x¬P(x)– из Σ₄ по ∃R ∎

Теперь попробуем доказать формулу, записанную в расширенном виде «⊦ ∃x(S(x)˄¬P(x))⊃¬∀x(S(x)⊃P(x))».

Поскольку у нас два предиката, начнём построение секвенций с двух аксиом:

Σ_1. S(x) ⊦ S(x) – аксиома

Σ_2. P(x) ⊦ P(x) – аксиома

Мы должны получить импликацию, следовательно, преминяем закон ⊃L:

Σ₃. S(x), S(x)⊃P(x) ⊦ P(x) – из Σ₁ и Σ₂ по ⊃L

Теперь надо получит конъюнкцию. Проще всего это сделать, прибавив произвольный термин в антецеденте формулы:

Σ₄. S(x)˄¬P(x), S(x)⊃P(x) ⊦ P(x) – из Σ₃ по ˄L

Перенеся из сукцедента в антецедент формулу «P(x)», получим повторение формулы «¬P(x)». Повторение убираем по правилу CL:

Σ₅. S(x)˄¬P(x), ¬P(x), S(x)⊃P(x) ⊦ – из Σ₄ по ¬L

Σ₆. S(x)˄¬P(x), S(x)⊃P(x) ⊦ – из Σ₅ по CL

Далее, вводим кванторы:

Σ₇. ∃x(S(x)˄¬P(x)), S(x)⊃P(x) ⊦ – из Σ₆ по ∃L

Σ₈. ∃x(S(x)˄¬P(x)), ∀x(S(x)⊃P(x)) ⊦ – из Σ₇ по ∀L

И, наконец, переносим формулу «∀x(S(x)⊃P(x))» из антецедента в сукцедент с отрицанием по правилу ¬R:

Σ₉. ∃x(S(x)˄¬P(x)) ⊦ ¬∀x(S(x)⊃P(x))– из Σ₈ по ¬R

Σ₁₀. ⊦ ∃x(S(x)˄¬P(x))⊃¬∀x(S(x)⊃P(x))– из Σ₉ по ⊃R ∎

Последнее действие совершено по правилу «⊃R», напоминающему правило дедукции.

Последнее исчисление представим в табличной форме:

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

Например, правило Modus Ponens (иногда именуемое как «правило исключения импликации»)

К этому правилу можно добавить

и так далее.

Используя дополнительные правила (например правило сведения к абсурду), некоторые задачи можно решить короче. Например, выводимость «⊦∀x(S(x)⊃P(x))⊃∀x(¬S(x)˅P(x))»:

Σ_1. S(x)⊃P(x) ⊦ S(x)⊃P(x) – аксиома

Σ_2. S(x)⊃P(x), S(x) ⊦ P(x) из Σ₁ по правилу удаления импликации

Σ₃. S(x)⊃P(x), S(x) ⊦ ¬S(x)˅P(x) из Σ₂ по ˅R

Σ₄. S(x)⊃P(x) ⊦ ¬S(x)˅P(x), ¬S(x) из Σ₃ по ¬R

Σ₅. S(x)⊃P(x), ¬(¬S(x)˅P(x)), ⊦¬S(x) из Σ₄ по ¬R

Σ₆. S(x)⊃P(x), ¬(¬S(x)˅P(x)), ⊦¬S(x)˅P(x) из Σ₅ по ˅R

Σ₇. ¬(¬S(x)˅P(x)) ⊦ ¬(¬S(x)˅P(x)) — аксиома

Σ₈. S(x)⊃P(x), ¬(¬S(x)˅P(x)) ⊦ — из Σ₆ и Σ₇ по правилу сведения к абсурду

Σ₉. S(x)⊃P(x) ⊦ ¬S(x)˅P(x) — из Σ₈  по ¬R

Σ₁₀. S(x)⊃P(x) ⊦ ∀x(¬S(x)˅P(x)) — из Σ₉  по ∀R

Σ₁₁. ∀x(S(x)⊃P(x)) ⊦ ∀x(¬S(x)˅P(x)) — из Σ₁₀  по ∀L

Σ₁₂. ⊦∀x(S(x)⊃P(x))⊃∀x(¬S(x)˅P(x)) — из Σ₁₁  по правилу дедукции∎

Обращаем внимание на то, что в решении данной формулу мы применили два новых правила: правило удаления импликации (в действии 2) и правило сведения к абсурду (действие 8).

Понятно, что любая секвенция может иметь несколько решений. Например, формулу «⊦∀x(S(x)⊃P(x))⊃∀x(¬S(x)˅P(x))» можно решить по-другому:

Σ_1. S(x)⊃P(x) ⊦ S(x)⊃P(x) – аксиома

Σ_2. S(x)⊃P(x), S(x) ⊦ P(x) из Σ₁ по правилу удаления импликации

Σ₃. S(x)⊃P(x) ⊦ P(x), ¬S(x) из Σ₂ по ¬R

Σ₄. S(x)⊃P(x) ⊦ P(x), ¬S(x)˅P(x) из Σ₃ по ˅R

Σ₅. S(x)⊃P(x) ⊦ ¬S(x)˅P(x), ¬S(x)˅P(x) из Σ₄ по ˅R

Σ₆. S(x)⊃P(x) ⊦ ¬S(x)˅P(x) из Σ₅ по CR

Σ₇. S(x)⊃P(x) ⊦ ∀x(¬S(x)˅P(x)) — из Σ₆  по ∀R

Σ₈. ∀x(S(x)⊃P(x)) ⊦ ∀x(¬S(x)˅P(x)) — из Σ₇  по ∀L

Σ₉. ⊦∀x(S(x)⊃P(x))⊃∀x(¬S(x)˅P(x)) — из Σ₈  по правилу дедукции∎

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

Решаем последнюю формулу, опустив кванторы. Пусть дано «⊦ S(x)⊃P(x)⊃¬S(x)˅P(x)».

Найдя в формуле знак основной импликации, мы перестраиваем формулу в «S(x)⊃P(x) ⊦ ¬S(x)˅P(x)».

Поскольку в формуле есть дизъюнкция, значит, у нас появляется альтернатива: либо «S(x)⊃P(x) ⊦ ¬S(x)», либо «S(x)⊃P(x) ⊦ P(x)».

Теперь необходимо каким-то образом «разбить» импликацию. Преобразуем «S(x)⊃P(x)» в «¬S(x)˅P(x)». Таким образом, получаем еще две альтернативы: «¬S(x) ⊦ ¬S(x)», «P(x) ⊦ ¬S(x)» и «¬S(x) ⊦ P(x)», «P(x) ⊦ P(x)». Поскольку в последних альтернативах мы наблюдаем аксиомы, следовательно, искомая формула верная.