Formula : A := X ( t 1 , … , t n ) ∣ ¬ A ∣ A ∨ B ∣ A ∧ B ∣ ∀ x A ∣ ∃ x A {\displaystyle 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) : Γ := 1 ∣ A . Γ {\displaystyle \Gamma :=1\mid A.\Gamma } (le point est une conjonction)
Séquent : Δ := 0 ∣ Γ , Δ {\displaystyle \Delta :=0\mid \Gamma ,\Delta } (la virgule est une dicjoncyion)
A . B . Γ , Δ A ∧ B . Γ , Δ ∧ i {\displaystyle {\frac {A.B.\Gamma ,\Delta }{A\wedge B.\Gamma ,\Delta }}\wedge _{i}}
A . Γ , B . Γ , Δ A ∨ B . Γ , Δ ∨ i {\displaystyle {\frac {A.\Gamma ,B.\Gamma ,\Delta }{A\vee B.\Gamma ,\Delta }}\vee _{i}}
A . Γ , Δ ∀ x A . Γ , Δ ∀ i ( x non libre dans la conclusion ) {\displaystyle {\frac {A.\Gamma ,\Delta }{\forall xA.\Gamma ,\Delta }}\forall _{i}(x{\hbox{non libre dans la conclusion}})}
A [ x := t ] . Γ , Δ ∃ x A . Γ , Δ ∃ i {\displaystyle {\frac {A[x:=t].\Gamma ,\Delta }{\exists xA.\Gamma ,\Delta }}\exists _{i}}
(le point est une conjonction)
(la virgule est une dicjoncyion)
![{\displaystyle {\frac {A[x:=t].\Gamma ,\Delta }{\exists xA.\Gamma ,\Delta }}\exists _{i}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/51fe7b9c33dbaaae175f1bb5f291db6153dcb351)