Числення секвенцій

Чи́слення секве́нцій — система формального виведення формул логіки першого порядку (і як часткового випадку логіки висловлень) запропонована німецьким логіком Генріхом Генценом. Після праці Генцена розроблено кілька варіантів числення секвенцій, що є еквівалентними між собою і альтернативою аксіоматичному підходу.

Термінологія

Числення секвенцій є альтернативною системою формального виводу до аксіоматичних систем описаних у статтях Числення висловлень і Логіка першого порядку. Формули логіки першого порядку для поданої нижче формальної системи мають лише дві логічні зв'яязки $(\neg ,\vee )$ і квантор існування. Інші символи логічних зв'язок можна визначити формулами:

• • $(\varphi \wedge \psi ):\Leftrightarrow \neg (\neg \varphi \vee \neg \psi )$
  • $(\varphi \rightarrow \psi ):\Leftrightarrow (\neg \varphi \vee \psi )$
  • $(\varphi \leftrightarrow \psi ):\Leftrightarrow \neg (\neg (\neg \varphi \vee \psi )\vee \neg (\neg \psi \vee \varphi ))$
• Подібно визначається і квантор загальності:
  • $\forall x\varphi :\Leftrightarrow \neg \exists x\neg \varphi$

Загалом при визначенні правил використовуються такі позначення:

• $\Gamma ,\Phi$ ... (скінченні множини формул)
• $\varphi ,\psi ,\rho$ ... (формули логіки першого порядку)
• $\vdash$ ... (Символ, що показує, що з формул з лівої сторони (антецеденту) виводяться формули з правої сторони (консеквент))
• $\neg$ ... (символ логічного заперечення)
• $\vee$ ... (символ диз'юнкції)
• $\exists$ ... (квантор існування)

Правила виводу

Правило антецедента

$\quad \left(Ant\right)\qquad {\frac {\Gamma \vdash \varphi }{\Gamma '\vdash \varphi }}$ якщо: $\Gamma \subseteq \Gamma '$.

Правило припущення

$\quad \left(Ann\right)\qquad {\frac {}{\Gamma \vdash \varphi }}$ якщо: $\varphi \in \Gamma$

Перебір варіантів

$\quad \left(FU\right)\qquad {\frac {\begin{aligned}{\Gamma \psi \vdash \varphi }\\{\Gamma \neg \psi \vdash \varphi }\end{aligned}}{\Gamma \vdash \varphi }}$

Доведення від супротивного

$\quad \left(KD\right)\qquad {\frac {\begin{aligned}{\Gamma \neg \psi \vdash \rho }\\{\Gamma \neg \psi \vdash \neg \rho }\end{aligned}}{\Gamma \vdash \psi }}$

Диз'юнкція а антецеденті

$\quad \left(\vee -Ant\right)\qquad {\frac {\begin{aligned}{\Gamma \varphi \vdash \rho }\\{\Gamma \psi \vdash \rho }\end{aligned}}{\Gamma (\varphi \vee \psi )\vdash \rho }}$

Диз'юнкція в консеквенті

$\quad \left(\vee -Kon1\right)\qquad {\frac {\begin{aligned}{\Gamma \vdash \varphi }\end{aligned}}{\Gamma \vdash (\varphi \vee \psi )}}$

$\quad \left(\vee -Kon2\right)\qquad {\frac {\begin{aligned}{\Gamma \vdash \psi }\end{aligned}}{\Gamma \vdash (\varphi \vee \psi )}}$

Введення квантора істинності в консеквенті

$\quad \left(\exists -Kon\right)\qquad {\frac {\Gamma \vdash \varphi {\frac {t}{x}}}{\Gamma \vdash \exists x\varphi }}$

Введення квантора істинності в антецеденті

$\quad \left(\exists -Ant\right)\qquad {\frac {\Gamma \varphi {\frac {y}{x}}\vdash \psi }{\Gamma \exists x\varphi \vdash \psi }}$, де y не зустрічається у вільному вигляді у формулі $\exists x\varphi \psi$ .

Рефлексивність рівності

$\quad \left(Ref\right)\qquad {\frac {}{\vdash t\equiv t}}$

Правило заміни в рівності

$\quad \left(\exists -Sub\right)\qquad {\frac {\Gamma \vdash \varphi {\frac {t}{x}}}{\Gamma t\equiv t'\vdash \varphi {\frac {t'}{x}}}}$

Приклади виведення

Приклад 1

Покажемо, що

$\quad \left(AD\right)\qquad {\frac {}{\varphi \vee \neg \varphi }}$

Маємо:

${\begin{alignedat}{3}1.\quad &\varphi \vdash \varphi &\quad &(Ann)\\2.\quad &\varphi \vdash (\varphi \vee \neg \varphi )&\quad &(\vee -Kon1):1.\\3.\quad &\neg \varphi \vdash \neg \varphi &\quad &(Ann)\\4.\quad &\neg \varphi \vdash (\varphi \vee \neg \varphi )&\quad &(\vee -Kon2):3.\\5.\quad &\vdash (\varphi \vee \neg \varphi )&\quad &(FU):2.,4.\end{alignedat}}$

Приклад 2

$\quad \left(Triv\right)\qquad {\frac {\begin{aligned}\Gamma \varphi \\\Gamma \neg \varphi \end{aligned}}{\Gamma \psi }}$

Як і в першому прикладі:

${\begin{alignedat}{3}1.\quad &\Gamma \varphi &\quad &(Pr{\ddot {a}}misse)\\2.\quad &\Gamma \neg \varphi &\quad &(Pr{\ddot {a}}misse)\\3.\quad &\Gamma \neg \psi \varphi &\quad &(Ant):1.\\4.\quad &\Gamma \neg \psi \neg \varphi &\quad &(Ant):2.\\5.\quad &\Gamma \psi &\quad &(KD):3.,4.\end{alignedat}}$

Коректність і повнота

Числення секвенцій є коректним і повним. Тобто всі формули, що можна вивести за його допомогою є логічно значимі і всі логічно значимі формули можна вивести за допомогою числення секвенцій. Це еквівалентно твердженню, що $\Phi \vDash \varphi$ тоді і тільки тоді коли $\Phi \vdash \varphi$ для довільних множини формул $\Phi \;$ і формули $\varphi$.

Джерела

• Правила виводу // Філософський енциклопедичний словник / В. І. Шинкарук (гол. редкол.) та ін. — Київ : Інститут філософії імені Григорія Сковороди НАН України : Абрис, 2002. — С. 507. — 742 с. — 1000 екз. — ББК 87я2. — ISBN 966-531-128-X.
• Ebbinghaus H.-D., Flum J., Thomas W.: Mathematical logic. New York: Springer-Verlag, 1984.
• Richter, M. M.: Logikkalküle. Stuttgart: Teubner Verlag, 1978.

Weblinks

• Sequent Calculus by Alex Sakharov MathWorld