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

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

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

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

• • $(\phi \wedge \psi ):\iff \mathrm{\neg }(\mathrm{\neg }\phi \vee \mathrm{\neg }\psi )$
  • $(\phi \to \psi ):\iff (\mathrm{\neg }\phi \vee \psi )$
  • $(\phi \leftrightarrow \psi ):\iff \mathrm{\neg }(\mathrm{\neg }(\mathrm{\neg }\phi \vee \psi )\vee \mathrm{\neg }(\mathrm{\neg }\psi \vee \phi ))$
• Подібно визначається і квантор загальності:
  • $\mathrm{\forall }x\phi :\iff \mathrm{\neg }\mathrm{\exists }x\mathrm{\neg }\phi$

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

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

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

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

$\left(Ant\right)\frac{\mathrm{\Gamma }⊢\phi }{{\mathrm{\Gamma }}^{\prime }⊢\phi }$ якщо: $\mathrm{\Gamma }\subseteq {\mathrm{\Gamma }}^{\prime }$.

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

$\left(Ann\right)\frac{}{\mathrm{\Gamma }⊢\phi }$ якщо: $\phi \in \mathrm{\Gamma }$

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

$\left(FU\right)\frac{\begin{array}{c}\mathrm{\Gamma }\psi ⊢\phi \\ \mathrm{\Gamma }\mathrm{\neg }\psi ⊢\phi \end{array}}{\mathrm{\Gamma }⊢\phi }$

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

$\left(KD\right)\frac{\begin{array}{c}\mathrm{\Gamma }\mathrm{\neg }\psi ⊢\rho \\ \mathrm{\Gamma }\mathrm{\neg }\psi ⊢\mathrm{\neg }\rho \end{array}}{\mathrm{\Gamma }⊢\psi }$

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

$(\vee -Ant)\frac{\begin{array}{c}\mathrm{\Gamma }\phi ⊢\rho \\ \mathrm{\Gamma }\psi ⊢\rho \end{array}}{\mathrm{\Gamma }(\phi \vee \psi )⊢\rho }$

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

$(\vee -Kon1)\frac{\begin{array}{c}\mathrm{\Gamma }⊢\phi \end{array}}{\mathrm{\Gamma }⊢(\phi \vee \psi )}$

$(\vee -Kon2)\frac{\begin{array}{c}\mathrm{\Gamma }⊢\psi \end{array}}{\mathrm{\Gamma }⊢(\phi \vee \psi )}$

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

$(\mathrm{\exists }-Kon)\frac{\mathrm{\Gamma }⊢\phi \frac{t}{x}}{\mathrm{\Gamma }⊢\mathrm{\exists }x\phi }$

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

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

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

$\left(Ref\right)\frac{}{⊢t\equiv t}$

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

$(\mathrm{\exists }-Sub)\frac{\mathrm{\Gamma }⊢\phi \frac{t}{x}}{\mathrm{\Gamma }t\equiv t^{\prime }⊢\phi \frac{t^{\prime }}{x}}$

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

Приклад 1

Покажемо, що

$\left(AD\right)\frac{}{\phi \vee \mathrm{\neg }\phi }$

Маємо:

$\begin{array}{cccc}1.& \phi ⊢\phi & & (Ann)\\ 2.& \phi ⊢(\phi \vee \mathrm{\neg }\phi )& & (\vee -Kon1):1.\\ 3.& \mathrm{\neg }\phi ⊢\mathrm{\neg }\phi & & (Ann)\\ 4.& \mathrm{\neg }\phi ⊢(\phi \vee \mathrm{\neg }\phi )& & (\vee -Kon2):3.\\ 5.& ⊢(\phi \vee \mathrm{\neg }\phi )& & (FU):2.,4.\end{array}$

Приклад 2

$\left(Triv\right)\frac{\begin{array}{c}\mathrm{\Gamma }\phi \\ \mathrm{\Gamma }\mathrm{\neg }\phi \end{array}}{\mathrm{\Gamma }\psi }$

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

$\begin{array}{cccc}1.& \mathrm{\Gamma }\phi & & (Pr\ddot{a}misse)\\ 2.& \mathrm{\Gamma }\mathrm{\neg }\phi & & (Pr\ddot{a}misse)\\ 3.& \mathrm{\Gamma }\mathrm{\neg }\psi \phi & & (Ant):1.\\ 4.& \mathrm{\Gamma }\mathrm{\neg }\psi \mathrm{\neg }\phi & & (Ant):2.\\ 5.& \mathrm{\Gamma }\psi & & (KD):3.,4.\end{array}$

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

Числення секвенцій є коректним і повним. Тобто всі формули, що можна вивести за його допомогою є логічно значимі і всі логічно значимі формули можна вивести за допомогою числення секвенцій. Це еквівалентно твердженню, що $\mathrm{\Phi }\models \phi$ тоді і тільки тоді коли $\mathrm{\Phi }⊢\phi$ для довільних множини формул $\mathrm{\Phi }$ і формули $\phi$.

Див. також

• Числення конструкцій

Джерела

• Правила виводу // Шаблон:ФЕС
• 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