Library gentzen
Signed formulas and clauses
We think of the Gentzen system as a decision procedure so we fix an input formula s0. This is realized as a Section variable. To obtain our main results, we generalize all statements over s0 by closing the section.
Section Signed.
Variable s0 : form.
Definition Cs0 := seq_sub (sub s0).
Definition F := (bool * Cs0) %type.
Fixpoint interp (s : F) := match s with (true , t) => val t | (false, t) => Neg (val t) end.
Lemma FvalE (s :Cs0) sc (b : bool) : [F val s; sc; b] = (b,s).
Implicit Types (A B H : {set F}).
Implicit Types (C : {set F}) (D : {set {set F}}).
Lemma pIl s t (sc : s ---> t \in sub s0) : s \in sub s0.
Lemma pIr s t (sc : s ---> t \in sub s0) : t \in sub s0.
Lemma pB s (sc : Box s \in sub s0) : s \in sub s0.
Lemma pP s (sc : PBox s \in sub s0) : s \in sub s0.
Definition Hcond (t : F) (H : {set F}) :=
match t with
| [F Var p ; sc; false] => [F Var p ; sc; true] \notin H
| [F s ---> t ; sc; true] => ([F s ; pIl sc; false] \in H) || ([F t ; pIr sc; true] \in H)
| [F s ---> t ; sc; false] => ([F s ; pIl sc; true] \in H) && ([F t ; pIr sc; false] \in H)
| [F Bot ; _ ; true] => false
| _ => true
end.
Definition hintikka (H : {set F}) : bool := forallb t , (t \in H) ==> Hcond t H.
Definition is_Box (s : F) := if s is [F Box t; sc; true] then true else false.
Definition boxes C := [set s \in C | is_Box s].
Definition is_PBox (s : F) := if s is [F PBox t; sc; true] then true else false.
Definition pboxes C := [set s \in C | is_PBox s].
Definition project (x :F) := match x with
| [F Box t ; sc ; b] => [F t;pB sc; b]
| [F PBox t ; sc ; b] => [F t;pP sc; b]
| _ => x
end.
Definition request C : {set F} := pboxes C :|: [set project s | s <- pboxes C :|: boxes C].
Definition is_Dia (s : F) := if s is [F Box t; sc; false] then true else false.
Definition is_PDia (s : F) := if s is [F PBox t; sc; false] then true else false.
Definition dstep D C C' := [&& C \in D, C' \in D & request C \subset C'].
Definition demoDia D :=
forallb C, (C \in D) ==>
forallb s,is_Dia s && (s \in C) ==> existsb C', dstep D C C' && (project s \in C').
Definition demoPDia D :=
forallb C, (C \in D) ==>
forallb s, is_PDia s && (s \in C) ==>
existsb C', plusb (dstep D) C C' && (project s \in C').
Definition demo D := demoDia D && demoPDia D.
match t with
| [F Var p ; sc; false] => [F Var p ; sc; true] \notin H
| [F s ---> t ; sc; true] => ([F s ; pIl sc; false] \in H) || ([F t ; pIr sc; true] \in H)
| [F s ---> t ; sc; false] => ([F s ; pIl sc; true] \in H) && ([F t ; pIr sc; false] \in H)
| [F Bot ; _ ; true] => false
| _ => true
end.
Definition hintikka (H : {set F}) : bool := forallb t , (t \in H) ==> Hcond t H.
Definition is_Box (s : F) := if s is [F Box t; sc; true] then true else false.
Definition boxes C := [set s \in C | is_Box s].
Definition is_PBox (s : F) := if s is [F PBox t; sc; true] then true else false.
Definition pboxes C := [set s \in C | is_PBox s].
Definition project (x :F) := match x with
| [F Box t ; sc ; b] => [F t;pB sc; b]
| [F PBox t ; sc ; b] => [F t;pP sc; b]
| _ => x
end.
Definition request C : {set F} := pboxes C :|: [set project s | s <- pboxes C :|: boxes C].
Definition is_Dia (s : F) := if s is [F Box t; sc; false] then true else false.
Definition is_PDia (s : F) := if s is [F PBox t; sc; false] then true else false.
Definition dstep D C C' := [&& C \in D, C' \in D & request C \subset C'].
Definition demoDia D :=
forallb C, (C \in D) ==>
forallb s,is_Dia s && (s \in C) ==> existsb C', dstep D C C' && (project s \in C').
Definition demoPDia D :=
forallb C, (C \in D) ==>
forallb s, is_PDia s && (s \in C) ==>
existsb C', plusb (dstep D) C C' && (project s \in C').
Definition demo D := demoDia D && demoPDia D.
Definition initial_bot C := (if Bot \in sub s0 is true as b return Bot \in sub s0 = b -> bool
then fun sc => [F Bot; sc; true] \in C else xpred0) (Logic.eq_refl _).
Definition initial_contra C := existsb s, [set (true,s); (false,s)] \subset C.
Definition initial (C : {set F}) := initial_bot C || initial_contra C.
Lemma initialIbot C sc : [F Bot ; sc ; true] \in C -> initial C.
Lemma initialIcontra C s sc : [F s ; sc ; true] \in C -> [F s ; sc ; false] \in C -> initial C.
Inductive retract : {set {set F}} -> {set F} -> Prop :=
| retract_initial C : initial C -> retract set0 C
| retract_self C : retract [set C] C
| retract_or D1 D2 s t C sc :
retract D1 ([F s ; pIl sc ; false] |: C) -> retract D2 ([F t ; pIr sc ; true] |: C) ->
retract (D1 :|: D2) ([F s ---> t ; sc ; true] |: C)
| retract_and D s t C sc :
retract D ([set [F s; pIl sc; true] ; [F t; pIr sc; false]] :|: C) ->
retract D ([F s ---> t ; sc ; false] |: C).
Definition hretract D C :=
[/\ retract D C, (forall H, H \in D -> hintikka H) & (forall H, H \in D -> C \subset H)].
Lemma saturationS C : {H | hretract H C}.
Definition hret C := sval (saturationS C).
Lemma hretP C : hretract (hret C) C.
Definition hretractb D C := D == hret C.
Definition jump D C := existsb s, [&& is_Dia s , s \in C & D == [set project s |: request C ]].
Definition compound s (L : {set {set F}}) (U : {set {set F}}) :=
is_PDia s && forallb C, (C \in L) ==>
[&& s \in C, project s |: request C \in U & hret (s |: request C) \subset L :|: U].
Definition loop D C := existsb s, is_PDia s && existsb L, compound s L D && (C \in L).
Definition rule D C := [|| hretractb D C, jump D C | loop D C].
Definition derivableF (S : {set {set F}}) :=
S :|: [set C | existsb D : {set {set F}}, (D \subset S) && rule D C].
Lemma mono_derivableF : mono derivableF.
Definition derivable C := C \in mu derivableF.
Definition consistent C := ~~ derivable C.
Lemma derivable_asm D C : rule D C -> (forall C', C' \in D -> derivable C') -> derivable C.
Lemma consistent_asm D C : rule D C -> consistent C -> exists2 C', (C' \in D) & consistent C'.
Lemma extension C : consistent C -> exists H: {set F}, [/\ C \subset H , hintikka H & consistent H].
Lemma consistent_jump C s sc :
consistent C -> [F Box s ; sc ; false] \in C -> consistent ([F s; pB sc; false] |: request C).
Definition DEMO := [set C | consistent C && hintikka C ].
Lemma demoDia_aux : demoDia DEMO.
Lemma demoPDia_aux : demoPDia DEMO.
Lemma demo_lemma : demo DEMO.
Section ModelExistence.
Definition Ds := seq_sub (enum (mem DEMO)).
Implicit Types (X Y : Ds).
Definition Dt X Y := request (val X) \subset (val Y).
Definition Dl n X :=
(if Var n \in sub s0 is true as b return Var n \in sub s0 = b -> bool
then fun sc => [F Var n; sc; true] \in val X else xpred0) (Logic.eq_refl _).
Definition demo_ts := Eval hnf in fin_model Dt Dl.
Lemma D_hintikka t X : t \in val X -> Hcond t (val X).
Lemma request_box s sc C : [F Box s; sc; true] \in C -> [F s; pB sc; true] \in request C.
Lemma request_pbox1 s sc C : [F PBox s; sc; true] \in C -> [F s; pP sc; true] \in request C.
Lemma request_pbox2 s sc C : [F PBox s; sc; true] \in C -> [F PBox s; sc; true] \in request C.
Lemma in_DEMO X : (val X) \in DEMO.
Lemma plus_dstep_Dt (H H' : Ds) : plus (dstep DEMO) (ssval H) (ssval H') -> plus Dt H H'.
Lemma model_MD (t : F) (H : Ds) : t \in val H -> @satisfies demo_ts H (interp t).
End ModelExistence.
Notation "[af C ]" := (\and_(s \in C) interp s).
Lemma memC C s : s \in C -> prv ( [af C] ---> interp s).
Lemma and1n s sc : prv (Neg s ---> [af [set [F s ; sc ; false]]]).
Lemma and1 s sc : prv (s ---> [af [set [F s ; sc ; true]]]).
Lemma af_1nF s C :
prv ([af (false,s) |: C ] ---> Bot) <-> prv ([af C] ---> val s).
Lemma initial_prv C : initial C -> prv ([af C ] ---> Bot).
Lemma hilbert_retract D C :
retract D C -> prv ([af C] ---> \or_(C' \in D) [af C']).
Lemma box_request C : prv ([af C] ---> Box [af request C]).
Lemma big_orW (T : eqType) (r : seq T) F G :
(forall i, prv (F i ---> G i)) -> prv ((\or_(i <- r) F i) ---> \or_(j <- r) G j).
Lemma hilbert_compound s L E C:
compound s L E -> (forall C, C \in E -> prv ([af C] ---> Bot)) ->
C \in L -> prv ([af C] ---> Bot).
Lemma hilbert_jump C D :
(forall C, C \in D -> prv ([af C] ---> Bot)) -> jump D C -> prv ([af C] ---> Bot).
Lemma translation C : derivable C -> prv ([af C] ---> Bot).
End Signed.