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

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

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

Числення секвенцій є альтернативною системою формального виводу до аксіоматичних систем описаних у статтях Числення висловлень і Логіка першого порядку. Формули логіки першого порядку для поданої нижче формальної системи мають лише дві логічні зв'яязки $(\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{align} {\Gamma\psi \vdash \varphi} \\ {\Gamma\neg\psi \vdash \varphi} \end{align} } {\Gamma \vdash \varphi}$

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

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

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

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

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

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

$\quad\left(\vee -Kon2\right)\qquad\frac{ \begin{align} {\Gamma \vdash \psi} \end{align} } {\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{alignat}{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{alignat}$

Приклад 2

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

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

$\begin{alignat}{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{alignat}$

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

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

Джерела

• 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