Числення секвенцій: відмінності між версіями

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

 

 

<math>\quad\left(Ant\right)\qquad\frac{\Gamma \vdash \varphi}{\Gamma '\vdash \varphi}</math>

якщо: <math>\Gamma\subseteq\Gamma '</math>.

 

 

<math>\quad\left(Ann\right)\qquad\frac{}{\Gamma \vdash \varphi}</math> якщо: <math>\varphi\in\Gamma</math>

 

 

<math>\quad\left(FU\right)\qquad\frac{

{\Gamma \vdash \varphi}</math>

 

 

<math>\quad\left(KD\right)\qquad\frac{

{\Gamma \vdash \psi}</math>

 

 

<math>\quad\left(\vee -Ant\right)\qquad\frac{

{\Gamma (\varphi\vee\psi ) \vdash \rho}</math>

 

 

<math>\quad\left(\vee -Kon1\right)\qquad\frac{

{\Gamma \vdash (\varphi\vee\psi )}</math>

 

 

<math>\quad\left(\exists -Kon\right)\qquad\frac{\Gamma \vdash \varphi\frac{t}{x}}{\Gamma \vdash \exists x\varphi}</math>

 

 

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

 

 

<math>\quad\left(Ref\right)\qquad\frac{}{\vdash t\equiv t}</math>

 

 

 

<math>\quad\left(\exists -Sub\right)\qquad\frac{\Gamma \vdash \varphi\frac{t}{x}}{\Gamma t\equiv t' \vdash \varphi\frac{t'}{x}}</math>