Library gentzen


Gentzen Systems as Decision Procedures


Notation "[F s ; sc ; b ]" := ( (b,[ss s ; sc]) ) (at level 0).

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.

Demos

  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.

Sequent System for K^+


Propositional Retracts


  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.

Jumps and Loops


  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].

Derivability


  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.

The Demo of underivable Clauses


  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.

Model Existence


  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.

Translation Theorem


  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.

Main Results


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.