« Reseau inverse » : différence entre les versions

Version du 20 octobre 2008 à 15:07

Formula : $A:=X(t_{1},\dots ,t_{n})\mid \neg A\mid A\vee B\mid A\wedge B\mid \forall xA\mid \exists xA$

On quotiente les formules pas les lois de De Morgan.

Clause (à démontrer) : $\Gamma :=1\mid A.\Gamma$ (le point est une conjonction)

Séquent : $\Delta :=0\mid \Gamma ,\Delta$ (la virgule est une dicjoncyion)

${\frac {\vdash A.B.\Gamma ,\Delta }{\vdash A\wedge B.\Gamma ,\Delta }}\wedge _{i}$

${\frac {\vdash A.\Gamma ,B.\Gamma ,\Delta }{\vdash A\vee B.\Gamma ,\Delta }}\vee _{i}$

${\frac {\vdash A.\Gamma ,\Delta }{\vdash \forall xA.\Gamma ,\Delta }}\forall _{i}(x{\hbox{ non libre dans la conclusion}})$

${\frac {\vdash A[x:=t].\Gamma ,\Delta }{\vdash \exists xA.\Gamma ,\Delta }}\exists _{i}$

@@ Ligne 12 : / Ligne 12 : @@
 <math>
-\frac{A . B . \Gamma , \Delta}{A \wedge B . \Gamma , \Delta}\wedge_i
+\frac{\vdash A . B . \Gamma , \Delta}{\vdash A \wedge B . \Gamma , \Delta}\wedge_i
 </math>
 <math>
-\frac{A . \Gamma, B . \Gamma, \Delta}{A \vee B. \Gamma , \Delta}\vee_i
+\frac{\vdash A . \Gamma, B . \Gamma, \Delta}{\vdash A \vee B. \Gamma , \Delta}\vee_i
 </math>
 <math>
-\frac{A . \Gamma, \Delta}{\forall x A . \Gamma, \Delta}\forall_i (x \hbox{ non libre dans la conclusion})
+\frac{\vdash A . \Gamma, \Delta}{\vdash \forall x A . \Gamma, \Delta}\forall_i (x \hbox{ non libre dans la conclusion})
 </math>
 <math>
-\frac{A[x:=t] . \Gamma, \Delta}{\exists x A . \Gamma, \Delta}\exists_i
+\frac{\vdash A[x:=t] . \Gamma, \Delta}{\vdash \exists x A . \Gamma, \Delta}\exists_i
 </math>