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

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

Покажемо, що

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

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