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).
Proof. case:s sc => /= s sc sc'. by rewrite (bool_irrelevance sc sc'). Qed.
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.
Proof. apply: sub_trans => //=. by rewrite !inE mem_cat sub_refl. Qed.
Lemma pIr s t (sc : s ---> t \in sub s0) : t \in sub s0.
Proof. apply: sub_trans => //=. by rewrite !inE mem_cat sub_refl. Qed.
Lemma pB s (sc : Box s \in sub s0) : s \in sub s0.
Proof. apply: sub_trans => //=. by rewrite !inE sub_refl. Qed.
Lemma pP s (sc : PBox s \in sub s0) : s \in sub s0.
Proof. apply: sub_trans => //=. by rewrite !inE sub_refl. Qed.
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.
Proof.
rewrite /initial /initial_bot. move: (Logic.eq_refl _).
rewrite {2 3}sc => e H. by rewrite (bool_irrelevance e sc) H.
Qed.
Lemma initialIcontra C s sc : [F s ; sc ; true] \in C -> [F s ; sc ; false] \in C -> initial C.
rewrite /initial /initial_contra => H1 H2. rightb; bexists [ss s;sc].
by rewrite subUset !sub1set H1 H2.
Qed.
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}.
Proof.
move: C. apply: slack_ind => /= C IH.
case e: (hintikka C).
- exists [set C]. (split; first by constructor) => H /set1P -> //.
- move/existsP : e => E. move: (xchoose E) (xchooseP E) => {E} s.
rewrite negb_imply.
case: s. case => [|] [] [p||u v|u|u] sc //= ; try by rewrite andbF.
+ rewrite andbT => X. exists set0.
split; by [constructor; exact: initialIbot | move => ?; rewrite inE].
+ rewrite negb_orb. case/and3P => H1 H2 H3. rewrite (set1mem H1) in IH H2 H3.
case (IH _ (properU1 H2)) => D1 [D11 D12 D13].
case (IH _ (properU1 H3)) => D2 [D21 D22 D23].
exists (D1 :|: D2). rewrite (set1mem H1).
split; first by constructor; rewrite (set1mem H1).
move => H /setUP []. exact: D12. exact: D22.
move => H /setUP [inD|inD].
apply: subset_trans _ (D13 _ inD). exact:subsetUr.
apply: subset_trans _ (D23 _ inD). exact:subsetUr.
+ rewrite negbK => /andP [H1 H2].
exists set0. constructor; try by move => ?; rewrite inE.
constructor. exact : initialIcontra H2 H1.
+ case/andP => H1 H2.
have: C \proper [set [F u; pIl sc; true]; [F v; pIr sc; false]] :|: C.
apply: properUr. by rewrite subUset !sub1set.
case/IH => D [D1 D2 D3].
exists D; split => //. rewrite (set1mem H1). by constructor.
move => H inD. apply: subset_trans _ (D3 _ inD). exact: subsetUr.
Qed.
Definition hret C := sval (saturationS C).
Lemma hretP C : hretract (hret C) C.
Proof. exact: svalP (saturationS C). Qed.
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.
Proof.
move => /= S S' sub. apply: setUSS => //. apply/subsetP => C.
rewrite !inE. case/existsP => D HD. bexists D.
case/andP : HD => H ->. by rewrite (subset_trans H sub).
Qed.
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.
Proof.
move => rul der. rewrite /derivable (muE mono_derivableF) {1}/derivableF.
apply/setUP;right. rewrite inE. bexists D. rewrite rul andbT.
apply/subsetP => C'. exact: der.
Qed.
Lemma consistent_asm D C : rule D C -> consistent C -> exists2 C', (C' \in D) & consistent C'.
Proof.
move => rul /negP con. apply/exists_inP.
rewrite -[existsb _, _]negbK negb_exists. apply/negP => /forallP /= H.
apply: con. apply: derivable_asm rul _ => C' inD. move: (H C').
by rewrite negb_andb inD /= negbK.
Qed.
Lemma extension C : consistent C -> exists H: {set F}, [/\ C \subset H , hintikka H & consistent H].
Proof.
move => cons.
have hrul: rule (hret C) C by rewrite /rule /hretractb eqxx.
case : (consistent_asm hrul cons) => /= H inD consH.
exists H. case (hretP C) => _; split; auto.
Qed.
Lemma consistent_jump C s sc :
consistent C -> [F Box s ; sc ; false] \in C -> consistent ([F s; pB sc; false] |: request C).
Proof.
move => con inC.
have hr: rule [set [F s; pB sc; false] |: request C ] C.
rightb; leftb. rewrite /jump . bexists [F Box s; sc; false].
by rewrite /= inC eqxx.
case: (consistent_asm hr con) => x.
by rewrite inE => /eqP ->.
Qed.
Definition DEMO := [set C | consistent C && hintikka C ].
Lemma demoDia_aux : demoDia DEMO.
Proof.
apply/forall_inP => C inD. move : (inD). rewrite inE => /andP [con _].
apply/forall_inP. do 4 case => //=. move => s sc inC.
have/extension: consistent ([F s; pB sc; false] |: request C) by exact: consistent_jump.
case => H [H1 H2 H3]. bexists H. rewrite (subsetP H1) ?inE ?eqxx // andbT.
rewrite /dstep inD !inE H2 H3 /=. apply: subset_trans _ H1. exact: subsetUr.
Qed.
Lemma demoPDia_aux : demoPDia DEMO.
Proof.
apply/forall_inP => C inD. move : (inD). rewrite inE => /andP [con hint].
apply/forall_inP. (do 4 case) => //= s sc inC.
set t := [F □+ s; sc; false] in inC.
set L := [set C' \in DEMO | (t \in C') && connect (dstep DEMO) C C'].
set D := [set C | derivable C].
simpl in *.
have CinL : C \in L by rewrite /L !inE con hint inC connect0.
have nhcmp: ~~ compound t L D. apply/negP => cmp.
have hrul: rule D C. rewrite /rule /loop. do 2 rightb.
bexists t => /=. bexists L. by rewrite cmp.
suff: derivable C. rewrite /consistent in con. by rewrite (negbTE con).
apply: derivable_asm hrul _ => C'. by rewrite !inE.
move : nhcmp. rewrite /compound /= negb_forall => /existsP /= [C'].
rewrite negb_imply !inE => /andP [] /and3P [/andP [con' hint'] t' conn'].
rewrite t' /=.
have -> : hret (t |: request C') \subset L :|: D.
case: (hretP (t |: request C')) => H1 H2 H3. apply/subsetP => H inHH.
case e: (derivable H); first by rewrite inE /D inE e.
rewrite inE /L /DEMO !inE /consistent e H2 // orbF /= (subsetP (H3 _ inHH)) ?inE ?eqxx //=.
apply: connect_trans conn' _. rewrite connect1 // /dstep !inE {2}/consistent e //=.
by rewrite con' hint' H2 //= (subset_trans _ (H3 _ inHH)) // subsetUr.
rewrite andbT -/(consistent ([F s; pP sc; false] |: request C')).
case/extension => H [H1 H2 H3]. bexists H. rewrite (subsetP H1) ?inE ?eqxx // andbT.
bexists C'. rewrite conn' /=.
rewrite /dstep // !inE H2 H3 /= con' hint' /=. apply: subset_trans _ H1. exact: subsetUr.
Qed.
Lemma demo_lemma : demo DEMO.
Proof. by rewrite /demo demoDia_aux demoPDia_aux. Qed.
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).
Proof. case: X => /= H. rewrite mem_enum inE. case/andP => _ /forall_inP. by apply. Qed.
Lemma request_box s sc C : [F Box s; sc; true] \in C -> [F s; pB sc; true] \in request C.
Proof.
move => H. apply/setUP; right. apply/imsetP; exists [F □ s; sc; true] => //.
by rewrite !inE H.
Qed.
Lemma request_pbox1 s sc C : [F PBox s; sc; true] \in C -> [F s; pP sc; true] \in request C.
Proof.
move => H. apply/setUP; right. apply/imsetP. exists [F □+ s; sc; true] => //.
by rewrite !inE H.
Qed.
Lemma request_pbox2 s sc C : [F PBox s; sc; true] \in C -> [F PBox s; sc; true] \in request C.
Proof. move => H. apply/setUP; left. by rewrite inE H. Qed.
Lemma in_DEMO X : (val X) \in DEMO.
Proof. rewrite -mem_enum. exact: ssvalP. Qed.
Lemma plus_dstep_Dt (H H' : Ds) : plus (dstep DEMO) (ssval H) (ssval H') -> plus Dt H H'.
Proof.
case: H' => /= H' inD P. elim: P inD => {H'} H'.
- case/and3P => H1 H2 H3 inD. exact: plus1.
- move => H'' step IH0 IH inD.
have inD' : H' \in enum DEMO. rewrite mem_enum. case: IH0 => [? | ? ?]; by case/and3P.
apply: plus_n1 _ (IH inD'). by case/and3P : step.
Qed.
Lemma model_MD (t : F) (H : Ds) : t \in val H -> @satisfies demo_ts H (interp t).
Proof.
case: t H. move => a b. move: b a. case. elim => [p | | u IHu v IHv | u IHu | u IHu ] sc [|] H //=.
- rewrite /Dl. move: (Logic.eq_refl _). rewrite {2 3}sc => sc'.
by rewrite (bool_irrelevance sc sc').
- rewrite /Dl. move: (Logic.eq_refl _). rewrite {2 3}sc => sc'.
move/D_hintikka => /=. rewrite (bool_irrelevance sc sc'). by move/negP.
- move/D_hintikka => //.
- move/D_hintikka => /=; case/orP => [/IHu | /IHv] /=; tauto.
- move/D_hintikka => /=; case/andP => /IHu /= Hu /IHv /=; tauto.
- move => inH H' /subsetP sub. apply: (IHu (pB sc) true). apply: sub. exact: request_box.
- move => inH.
case/andP : (demo_lemma) => /forall_inP /(_ _ (in_DEMO H)).
move => /forall_inP /(_ [F □ u; sc; false]) /= /(_ inH).
case/exists_inP => H' [H1 H2] _.
have inD : H' \in (enum (mem DEMO)). rewrite mem_enum. by case/and3P : H1.
have HDt : Dt H [ss H'; inD]. by destruct H; case/and3P : H1.
move => /(_ _ HDt). exact: (IHu _ _ [ss H'; inD] H2).
- move => inH H' P. apply: (IHu (pP sc) true).
suff: [F PBox u; sc; true] \in val H' /\ [F u; pP sc; true] \in val H' by tauto.
elim: P inH => {H'} H'.
+ move/subsetP => sub inH. rewrite !sub //.
exact: request_pbox1. exact: request_pbox2.
+ move => H'' /subsetP sub _ IH /IH [X _]. split; rewrite sub //.
exact: request_pbox2. exact: request_pbox1.
- move => inH.
case/andP : (demo_lemma) => _ /forall_inP /(_ _ (in_DEMO H)).
move => /forall_inP /(_ [F □+ u; sc; false]) /= /(_ inH).
case/exists_inP => H' [/plusP /= H1 H2].
have inD : H' \in (enum (mem DEMO)).
rewrite mem_enum. case/plusP : H1 => /exists_inP [H'' _]. by case/and3P.
move => X. apply: (IHu _ _ [ss H'; inD] H2). apply: X. exact: plus_dstep_Dt.
Qed.
End ModelExistence.
Notation "[af C ]" := (\and_(s \in C) interp s).
Lemma memC C s : s \in C -> prv ( [af C] ---> interp s).
Proof. move => inC. apply: big_andE. by rewrite mem_enum. Qed.
Lemma and1n s sc : prv (Neg s ---> [af [set [F s ; sc ; false]]]).
Proof. rewrite enum1s /= big_cons big_nil. rewrite <- (ax_andT _). I. Qed.
Lemma and1 s sc : prv (s ---> [af [set [F s ; sc ; true]]]).
Proof. rewrite enum1s /= big_cons big_nil. rewrite <- (ax_andT _). I. Qed.
Lemma af_1nF s C :
prv ([af (false,s) |: C ] ---> Bot) <-> prv ([af C] ---> val s).
Proof.
split.
- rewrite <- (and_aU _ _ _), <- (ax_dn (val s)) => H.
HYP. do 2 Intro. Apply H. Apply ax_aI. Det. mp;[K|]. apply: and1n. exact: valP.
- move => H. rewrite -> (and_Ua _ _ _), -> H. rule ax_aEl. apply: memC (set11 _).
Qed.
Lemma initial_prv C : initial C -> prv ([af C ] ---> Bot).
Proof.
case/orP.
- case e : (Bot \in sub s0); rewrite /initial_bot; move : (Logic.eq_refl _);
rewrite {2 3}e => e' //= /memC H //.
- case/existsP => s /subsetP S.
have P1 : prv ([af C] ---> val s).
have/memC : (true,s) \in C by rewrite S // !inE. apply.
have P2 : prv ([af C] ---> Neg (val s)).
have/memC : (false,s) \in C by rewrite S // !inE. apply.
HYP. Intro. Apply P2. Apply P1.
Qed.
Lemma hilbert_retract D C :
retract D C -> prv ([af C] ---> \or_(C' \in D) [af C']).
Proof.
elim => {D C}.
- move => C /initial_prv H. rewrite -> H. exact: ax_ex.
- move => C. rewrite enum1s big_cons big_nil. rewrite <- (ax_orI1 _ _). I.
- move => D1 D2 s t C sc _ IH1 _ IH2.
rewrite -> (and_Ua _ _ _), <- (big_orU _ _ _), <- IH1, <- IH2.
rewrite enum1s /= big_cons big_nil /=.
rewrite -> (ax_aE1 _ Top), -> (ax_imp_or s t), -> (ax_aDl _ _ _).
rewrite -> (and1n (pIl sc)).
rewrite -> (and1 (pIr sc)) at 2. do 2 rewrite -> (and_aU _ _ _). by I.
- move => D s t C sc _ IH.
rewrite -> (and_Ua _ _ _), <- IH.
rewrite enum1s /= big_cons big_nil.
rewrite -> (ax_aE1 _ Top), -> (ax_nimp_a s t), -> (ax_aA1 _ _ _).
rewrite -> (and1n (pIr sc)). rewrite -> (and1 (pIl sc)) at 1.
do 2 rewrite -> (and_aU _ _ _). rewrite setUA. by I.
Qed.
Lemma box_request C : prv ([af C] ---> Box [af request C]).
Proof.
rewrite <- (big_and_box _ interp). apply: big_andI=> s.
rewrite mem_enum !inE andbC. case/orP.
- move: s;(do 4 case) => //= t sc inC.
rewrite <- (ax_bpE1 _). exact: memC inC.
- case/imsetP => u H -> {s}. move: H. rewrite !inE ![(u \in C) && _]andbC.
case/orP; move: u; (do 4 case) => //= s sc inC; first rewrite <- (ax_bpE2 _);
exact: memC inC.
Qed.
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).
Proof. move => H. apply big_orE => i in_r. rewrite -> (H _). exact: big_orI. Qed.
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).
Proof.
case/andP. move: s. (do 4 case) => //= s sc _ /forall_inP /= cmp ref inE.
case/and3P : (cmp _ inE) => C1 _ _.
suff {C1} : prv ([af C] ---> PBox s).
have: prv ([af C] ---> Neg (PBox s)) by exact: memC C1.
move => P1 P2. HYP. Intro. Apply P1. by Apply P2.
have req: forall C', C' \in L -> prv ([af request C'] ---> s).
move => C' /cmp /and3P [C1 C2 C3]. rewrite [s]/(interp [F s; pP sc; true]).
apply/af_1nF. exact: ref.
set I:= SBox s :\/: \or_(C \in L) [af request C].
have I1 : prv ([af C] ---> Box I).
rewrite /I. rewrite <- (ax_bo _ _), <- (ax_orI2 _ _), <- (big_bo _ _).
have/big_orI H : C \in enum L by rewrite mem_enum.
rewrite <- (H _). exact: box_request.
have I2 : prv (I ---> Box I).
move => {C inE I1}.
rewrite /I. rule ax_orE.
- rewrite <- (ax_bo _ _), <- (ax_orI1 _ _). exact: ax_sbE1.
- apply: big_orE => /= C. rewrite mem_enum => inL.
case/and3P: (cmp _ inL) => _ _ E1.
case (hretP ([F □+ s; sc; false] |: request C)) => E2 _ _. set D := hret _ in E1 E2.
move: (hilbert_retract E2) => H.
rewrite <- (ax_bo _ _), <- (ax_pbsb _). rewrite {1}/Or. rule ax_aIL.
rewrite -> (and1n sc), -> (and_aU _ _ _). rewrite setUC.
rewrite -> H. rewrite <- (big_bo _ _).
rewrite <- (big_orW _ (box_request)).
apply: big_orE => j. rewrite mem_enum => /(subsetP E1). case/setUP.
+ rewrite -mem_enum => X. by cutB;[apply big_orI with (j := j) | I].
+ move/ref => X. rewrite -> X. exact: ax_ex.
have I3 : prv (I ---> s).
rewrite /I. rule ax_orE; first exact: ax_aE1. apply: big_orE => /= C'.
rewrite mem_enum. exact: req.
HYP. Intro. Apply (r_preg I3). Apply ax_seg. Apply I1.
mp;[K|]. exact: r_pnec.
Qed.
Lemma hilbert_jump C D :
(forall C, C \in D -> prv ([af C] ---> Bot)) -> jump D C -> prv ([af C] ---> Bot).
Proof.
move => H.
case/existsP => s. move: s; (do 4 case) => //= s sc /andP [J1 /eqP J2]. subst D.
move : (H _ (set11 _)). move/af_1nF => /= /r_reg => H'. rewrite (set1mem J1).
apply/af_1nF => /=. cutB; first apply H'.
exact: box_request.
Qed.
Lemma translation C : derivable C -> prv ([af C] ---> Bot).
Proof.
rewrite /derivable. move: C. apply mu_ind; first by move => ?;rewrite inE.
move => /= S IH C. case/setUP; first exact: IH. rewrite inE.
case/exists_inP => /= D subS. case/or3P.
- rewrite /hretractb => /eqP e; subst. case: (hretP C) => /hilbert_retract H _ _.
rewrite -> H => {H}.
apply: big_orE => C'. rewrite mem_enum => /(subsetP subS). exact: IH.
- apply: hilbert_jump => C'. move/(subsetP subS). exact: IH.
- case/exists_inP. (do 4 case) => //= s sc _ /exists_inP [L L1 L2].
apply: hilbert_compound L1 _ L2 => C' /(subsetP subS). exact: IH.
Qed.
End Signed.
Theorem decidability s :
{ (exists C : Ds s, @satisfies (demo_ts s) C (Neg s)) } + { prv s }.
Proof.
case der: (derivable [set [F s; sub_refl s; false]]); [right|left].
- move/translation : der.
rewrite enum1s /= big_cons big_nil. rewrite <- (ax_andT _).
move => P. by rule ax_dn.
- case/negbT : der => /extension [H [H1 H2 H3]].
have Dt: H \in enum (DEMO s) by rewrite mem_enum inE H2 H3.
exists ([ss H; Dt]). change (Neg s) with (interp [F s; sub_refl s; false]).
apply: model_MD. by rewrite /= (subsetP H1) // inE.
Qed.
Theorem completeness s : valid s -> prv s.
Proof.
move => V. case (decidability s) => // [[C]] /=.
move: (V (demo_ts s) C); tauto.
Qed.
Print Assumptions completeness.