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

Матеріал з Вікіпедії — вільної енциклопедії.
Перейти до: навігація, пошук

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

Термінологія[ред.ред. код]

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

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

  • \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[ред.ред. код]