# Library Gentzen

Require Export PropL.

Inductive gen : context -> form -> Prop :=
| genV A x : Var x el A -> gen A (Var x)
| genF A u : Fal el A -> gen A u
| genIR A s t : gen (s::A) t -> gen A (Imp s t)
| genIL A s t u : Imp s t el A -> gen A s -> gen (t::A) u -> gen A u.

Lemma gen_nd A s :
gen A s -> nd A s.

Consistency

Lemma gen_con :
~ gen nil Fal.

Unprovability of DN

Lemma gen_DN' A x s :
A <<= [Var x; Not (Not (Var x))] -> gen A s -> s <> Fal /\ s <> Not (Var x).

Lemma gen_DN x :
~ gen [Not (Not (Var x))] (Var x).

Assumption rule

Lemma genA A s :
s el A -> gen A s.

Weakening rule

Lemma genW A B s :
gen A s -> A <<= B -> gen B s.

Cut rule

Lemma genC' A s B u :
gen A s -> gen B u -> gen (A ++ rem B s) u.

Lemma genC A s u :
gen A s -> gen (s::A) u -> gen A u.

Completeness for ND

Lemma nd_gen A s :
nd A s -> gen A s.

Theorem gen_iff_nd A s :
gen A s <-> nd A s.

Subformula Closure

Definition sf_closed (A : context) : Prop :=
forall u, u el A -> match u with
| Imp s t => s el A /\ t el A
| _ => True
end.

Lemma sf_closed_app A B :
sf_closed A -> sf_closed B -> sf_closed (A ++ B).

Lemma sf_closed_cons s t A :
s el A -> t el A -> sf_closed A -> sf_closed (Imp s t :: A).

Fixpoint scl' (s : form) : context :=
s :: match s with
| Imp u v => scl' u ++ scl' v
| _ => nil
end.

Lemma scl'_in s :
s el scl' s.

Lemma scl'_closed s :
sf_closed (scl' s).

Fixpoint scl (A : context) : context :=
match A with
| nil => nil
| s :: A' => scl' s ++ scl A'
end.

Lemma scl_incl' A :
A <<= scl A.

Lemma scl_incl A B :
A <<= B -> A <<= scl B.

Lemma scl_closed A :
sf_closed (scl A).

Decidability

Definition goal := prod (context) form.

Instance goal_eq_dec gamma delta :
dec (gamma = delta :> goal).

Section Decidability.
Variable A0 : context.
Variable s0 : form.
Definition U := scl (s0::A0).
Definition U_sfc : sf_closed U := @scl_closed _.
Definition Gamma := list_prod (power U) U.

Definition step (Delta : list goal) (gamma : goal) : Prop :=
let (A,u) := gamma in
match u with
| Var _ => u el A
| Imp s t => (rep (s::A) U, t) el Delta
| _ => False
end
\/
exists v, v el A /\
match v with
| Fal => True
| Imp s t => (A, s) el Delta /\ (rep (t::A) U, u) el Delta
| _ => False
end.

Instance step_dec Delta gamma :
dec (step Delta gamma).

Definition Lambda : list goal :=
FCI.C (step := step) Gamma.

Lemma lambda_closure gamma :
gamma el Gamma -> step Lambda gamma -> gamma el Lambda.

Lemma lambda_ind (p : goal -> Prop) :
(forall Delta gamma, inclp Delta p -> gamma el Gamma -> step Delta gamma -> p gamma) -> inclp Lambda p.

Lemma gen_lambda A u :
A <<= U -> u el U -> gen A u -> (rep A U,u) el Lambda.

Lemma lambda_gen A u :
(A,u) el Lambda -> gen A u.

Theorem nd_dec :
dec (nd A0 s0).

End Decidability.