# 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).

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.

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

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.

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

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

## 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).

Definition DEMO := [set C | consistent C && hintikka C ].

Lemma demoDia_aux : demoDia DEMO.

Lemma demoPDia_aux : demoPDia DEMO.

Lemma demo_lemma : demo DEMO.

## 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).

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.

## Translation Theorem

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.

# Main Results

Theorem decidability s :
{ (exists C : Ds s, @satisfies (demo_ts s) C (Neg s)) } + { prv s }.

Theorem completeness s : valid s -> prv s.

Print Assumptions completeness.