Чи́слення секве́нцій — система формального виведення формул логіки першого порядку (і як часткового випадку логіки висловлень ) запропонована німецьким логіком Ґергардом Ґенценом . Після праці Ґенцена розроблено кілька варіантів числення секвенцій, що є еквівалентними між собою і альтернативою аксіоматичному підходу.
Числення секвенцій є альтернативною системою формального виводу до аксіоматичних систем описаних у статтях Числення висловлень і Логіка першого порядку . Формули логіки першого порядку для поданої нижче формальної системи мають лише дві логічні зв'яязки
(
¬
,
∨
)
{\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 ))}
Подібно визначається і квантор загальності :
∀
x
φ
:⇔
¬
∃
x
¬
φ
{\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 }
(
A
n
t
)
Γ
⊢
φ
Γ
′
⊢
φ
{\displaystyle \quad \left(Ant\right)\qquad {\frac {\Gamma \vdash \varphi }{\Gamma '\vdash \varphi }}}
Γ
⊆
Γ
′
{\displaystyle \Gamma \subseteq \Gamma '}
(
A
n
n
)
Γ
⊢
φ
{\displaystyle \quad \left(Ann\right)\qquad {\frac {}{\Gamma \vdash \varphi }}}
φ
∈
Γ
{\displaystyle \varphi \in \Gamma }
(
F
U
)
Γ
ψ
⊢
φ
Γ
¬
ψ
⊢
φ
Γ
⊢
φ
{\displaystyle \quad \left(FU\right)\qquad {\frac {\begin{aligned}{\Gamma \psi \vdash \varphi }\\{\Gamma \neg \psi \vdash \varphi }\end{aligned}}{\Gamma \vdash \varphi }}}
ред.
(
K
D
)
Γ
¬
ψ
⊢
ρ
Γ
¬
ψ
⊢
¬
ρ
Γ
⊢
ψ
{\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 }}}
ред.
(
∨
−
A
n
t
)
Γ
φ
⊢
ρ
Γ
ψ
⊢
ρ
Γ
(
φ
∨
ψ
)
⊢
ρ
{\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 }}}
ред.
(
∨
−
K
o
n
1
)
Γ
⊢
φ
Γ
⊢
(
φ
∨
ψ
)
{\displaystyle \quad \left(\vee -Kon1\right)\qquad {\frac {\begin{aligned}{\Gamma \vdash \varphi }\end{aligned}}{\Gamma \vdash (\varphi \vee \psi )}}}
(
∨
−
K
o
n
2
)
Γ
⊢
ψ
Γ
⊢
(
φ
∨
ψ
)
{\displaystyle \quad \left(\vee -Kon2\right)\qquad {\frac {\begin{aligned}{\Gamma \vdash \psi }\end{aligned}}{\Gamma \vdash (\varphi \vee \psi )}}}
ред.
(
∃
−
K
o
n
)
Γ
⊢
φ
t
x
Γ
⊢
∃
x
φ
{\displaystyle \quad \left(\exists -Kon\right)\qquad {\frac {\Gamma \vdash \varphi {\frac {t}{x}}}{\Gamma \vdash \exists x\varphi }}}
ред.
(
∃
−
A
n
t
)
Γ
φ
y
x
⊢
ψ
Γ
∃
x
φ
⊢
ψ
{\displaystyle \quad \left(\exists -Ant\right)\qquad {\frac {\Gamma \varphi {\frac {y}{x}}\vdash \psi }{\Gamma \exists x\varphi \vdash \psi }}}
∃
x
φ
ψ
{\displaystyle \exists x\varphi \psi }
ред.
(
R
e
f
)
⊢
t
≡
t
{\displaystyle \quad \left(Ref\right)\qquad {\frac {}{\vdash t\equiv t}}}
ред.
(
∃
−
S
u
b
)
Γ
⊢
φ
t
x
Γ
t
≡
t
′
⊢
φ
t
′
x
{\displaystyle \quad \left(\exists -Sub\right)\qquad {\frac {\Gamma \vdash \varphi {\frac {t}{x}}}{\Gamma t\equiv t'\vdash \varphi {\frac {t'}{x}}}}}
Покажемо, що
(
A
D
)
φ
∨
¬
φ
{\displaystyle \quad \left(AD\right)\qquad {\frac {}{\varphi \vee \neg \varphi }}}
Маємо:
1.
φ
⊢
φ
(
A
n
n
)
2.
φ
⊢
(
φ
∨
¬
φ
)
(
∨
−
K
o
n
1
)
:
1.
3.
¬
φ
⊢
¬
φ
(
A
n
n
)
4.
¬
φ
⊢
(
φ
∨
¬
φ
)
(
∨
−
K
o
n
2
)
:
3.
5.
⊢
(
φ
∨
¬
φ
)
(
F
U
)
:
2.
,
4.
{\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}}}
(
T
r
i
v
)
Γ
φ
Γ
¬
φ
Γ
ψ
{\displaystyle \quad \left(Triv\right)\qquad {\frac {\begin{aligned}\Gamma \varphi \\\Gamma \neg \varphi \end{aligned}}{\Gamma \psi }}}
Як і в першому прикладі:
1.
Γ
φ
(
P
r
a
¨
m
i
s
s
e
)
2.
Γ
¬
φ
(
P
r
a
¨
m
i
s
s
e
)
3.
Γ
¬
ψ
φ
(
A
n
t
)
:
1.
4.
Γ
¬
ψ
¬
φ
(
A
n
t
)
:
2.
5.
Γ
ψ
(
K
D
)
:
3.
,
4.
{\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}}}
ред.
