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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Приклад 1

Покажемо, що

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

Маємо:

${\displaystyle {\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

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

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

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

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

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

Див. також

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

Джерела

• Правила виводу // Філософський енциклопедичний словник / В. І. Шинкарук (гол. редкол.) та ін. — Київ : Інститут філософії імені Григорія Сковороди НАН України : Абрис, 2002. — С. 507. — 742 с. — 1000 екз. — ББК (87я2). — .
• 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