One-step conditions, 4.1 - 4.3
Require Export rule_sets semantics renaming list_multiset.
Section One_step_conditions.
Variable V : Type.
Variable L : modal_operators.
Variable T : functor.
Need a decidable equality for limit_subst, which is needed in 4.3
Definition one_step_sound(nonempty_v : V)(LS : lambda_structure L T)
(rules : set (sequent_rule V L))
(osr : one_step_rule_set rules) : Prop :=
∀(X : Type)(r : sequent_rule V L)(rules_r : rules r)
(coval : X → set V),
(∀(n : nat)(n_less : n < length (assumptions r)),
prop_seq_val_valid nonempty_v coval
(nth (assumptions r) n n_less)
(one_step_rule_propositional_assumption r
(osr r rules_r) n n_less))
→
mod_seq_val_valid LS coval (conclusion r)
(one_step_rule_nonempty_conclusion r (osr r rules_r))
(one_step_rule_prop_modal_prop_conclusion r (osr r rules_r)).
Towards one-step Completeness, Def 4.1
Definition simple_mod_weaken_rule(rules : set (sequent_rule V L))
: set (sequent_rule V L) :=
fun(r_subst : sequent_rule V L) ⇒
∃(r_base : sequent_rule V L)
(sigma : lambda_subst V L)
(delta : sequent V L),
rules r_base ∧
rank_subst 1 sigma ∧
simple_modal_sequent delta ∧
assumptions r_subst = map (subst_sequent sigma) (assumptions r_base) ∧
list_reorder (conclusion r_subst)
((subst_sequent sigma (conclusion r_base)) ++ delta).
Lemma simple_mod_weaken_rule_assumptions :
∀(rules : set (sequent_rule V L))(r : sequent_rule V L),
one_step_rule_set rules →
simple_mod_weaken_rule rules r →
every_nth propositional_sequent (assumptions r).
: set (sequent_rule V L) :=
fun(r_subst : sequent_rule V L) ⇒
∃(r_base : sequent_rule V L)
(sigma : lambda_subst V L)
(delta : sequent V L),
rules r_base ∧
rank_subst 1 sigma ∧
simple_modal_sequent delta ∧
assumptions r_subst = map (subst_sequent sigma) (assumptions r_base) ∧
list_reorder (conclusion r_subst)
((subst_sequent sigma (conclusion r_base)) ++ delta).
Lemma simple_mod_weaken_rule_assumptions :
∀(rules : set (sequent_rule V L))(r : sequent_rule V L),
one_step_rule_set rules →
simple_mod_weaken_rule rules r →
every_nth propositional_sequent (assumptions r).
The set of assumptions
Definition valid_subst_n_conclusions
{X : Type}(nonempty_v : V)
(rules : set (sequent_rule V L))
(osr : one_step_rule_set rules)
(coval : X → set V) : set (sequent V L) :=
fun(s : sequent V L) ⇒
∃(r : sequent_rule V L),
swr # simple_mod_weaken_rule rules r /#\
s = conclusion r ∧
∀(i : nat)(i_less : i < length (assumptions r)),
prop_seq_val_valid nonempty_v coval
(nth (assumptions r) i i_less)
(simple_mod_weaken_rule_assumptions _ _ osr swr _ _).
Lemma multiset_valid_subst_n_conclusions :
∀(X : Type)(nonempty_v : V)(rules : set (sequent_rule V L))
(osr : one_step_rule_set rules)(coval : X → set V),
sequent_multiset
(valid_subst_n_conclusions nonempty_v rules osr coval).
Lemma rank_sequent_set_valid_subst_n_conclusions :
∀(X : Type)(nonempty_v : V)
(rules : set (sequent_rule V L))(osr : one_step_rule_set rules)
(coval : X → set V),
rank_sequent_set 2
(valid_subst_n_conclusions nonempty_v rules osr coval).
{X : Type}(nonempty_v : V)
(rules : set (sequent_rule V L))
(osr : one_step_rule_set rules)
(coval : X → set V) : set (sequent V L) :=
fun(s : sequent V L) ⇒
∃(r : sequent_rule V L),
swr # simple_mod_weaken_rule rules r /#\
s = conclusion r ∧
∀(i : nat)(i_less : i < length (assumptions r)),
prop_seq_val_valid nonempty_v coval
(nth (assumptions r) i i_less)
(simple_mod_weaken_rule_assumptions _ _ osr swr _ _).
Lemma multiset_valid_subst_n_conclusions :
∀(X : Type)(nonempty_v : V)(rules : set (sequent_rule V L))
(osr : one_step_rule_set rules)(coval : X → set V),
sequent_multiset
(valid_subst_n_conclusions nonempty_v rules osr coval).
Lemma rank_sequent_set_valid_subst_n_conclusions :
∀(X : Type)(nonempty_v : V)
(rules : set (sequent_rule V L))(osr : one_step_rule_set rules)
(coval : X → set V),
rank_sequent_set 2
(valid_subst_n_conclusions nonempty_v rules osr coval).
Generic one-step completeness
Definition one_step_generic_complete
(nonempty_v : V)(LS : lambda_structure L T)
(prop_rules : set (sequent_rule V L))
(rules : set (sequent_rule V L))
(osr : one_step_rule_set rules) : Prop :=
∀(X : Type)(coval : X → set V)
(gamma : sequent V L)(gamma_nonempty : gamma ≠ [])
(gamma_simple : simple_modal_sequent gamma),
mod_seq_val_valid LS coval gamma gamma_nonempty
(simple_modal_sequent_is_prop_modal_prop gamma gamma_simple) →
provable prop_rules
(valid_subst_n_conclusions nonempty_v rules osr coval)
gamma.
(nonempty_v : V)(LS : lambda_structure L T)
(prop_rules : set (sequent_rule V L))
(rules : set (sequent_rule V L))
(osr : one_step_rule_set rules) : Prop :=
∀(X : Type)(coval : X → set V)
(gamma : sequent V L)(gamma_nonempty : gamma ≠ [])
(gamma_simple : simple_modal_sequent gamma),
mod_seq_val_valid LS coval gamma gamma_nonempty
(simple_modal_sequent_is_prop_modal_prop gamma gamma_simple) →
provable prop_rules
(valid_subst_n_conclusions nonempty_v rules osr coval)
gamma.
Definition one_step_complete(nonempty_v : V)(LS : lambda_structure L T)
(rules : set (sequent_rule V L))
(osr : one_step_rule_set rules) : Prop :=
one_step_generic_complete nonempty_v LS (GC_n_set V L 2) rules osr.
(rules : set (sequent_rule V L))
(osr : one_step_rule_set rules) : Prop :=
one_step_generic_complete nonempty_v LS (GC_n_set V L 2) rules osr.
Definition one_step_cut_free_complete
(nonempty_v : V)
(LS : lambda_structure L T)
(rules : set (sequent_rule V L))
(osr : one_step_rule_set rules) : Prop :=
one_step_generic_complete nonempty_v LS (G_n_set V L 2) rules osr.
(nonempty_v : V)
(LS : lambda_structure L T)
(rules : set (sequent_rule V L))
(osr : one_step_rule_set rules) : Prop :=
one_step_generic_complete nonempty_v LS (G_n_set V L 2) rules osr.
Lemma propositional_renamed_one_step_assumptions :
∀(rules : set (sequent_rule V L))(r : sequent_rule V L)
(sigma : lambda_subst V L)
(i : nat)(i_less : i < length (assumptions r)),
one_step_rule_set rules →
rules r →
renaming sigma →
propositional_sequent
(subst_sequent sigma (nth (assumptions r) i i_less)).
Lemma simple_one_step_cut_free_complete :
∀(nonempty_v : V)(LS : lambda_structure L T)
(rules : set (sequent_rule V L))(osr : one_step_rule_set rules),
one_step_cut_free_complete nonempty_v LS rules osr ↔
∀(X : Type)(coval : X → set V)
(gamma : sequent V L)(gamma_nonempty : gamma ≠ [])
(gamma_simple : simple_modal_sequent gamma),
mod_seq_val_valid LS coval gamma gamma_nonempty
(simple_modal_sequent_is_prop_modal_prop gamma gamma_simple) →
∃(r : sequent_rule V L)(sigma : lambda_subst V L),
rules_r # rules r /#\
renaming_sigma # renaming sigma /#\
multi_subset (subst_sequent sigma (conclusion r)) gamma ∧
∀(i : nat)(i_less : i < length (assumptions r)),
prop_seq_val_valid nonempty_v coval
(subst_sequent sigma (nth (assumptions r) i i_less))
(propositional_renamed_one_step_assumptions rules r sigma
i i_less osr rules_r renaming_sigma).
End One_step_conditions.
Implicit Arguments one_step_sound [V L T].
Implicit Arguments valid_subst_n_conclusions [V L X].
Implicit Arguments simple_mod_weaken_rule_assumptions [V L].
Implicit Arguments one_step_complete [V L T].
Implicit Arguments one_step_cut_free_complete [V L T].
Implicit Arguments simple_one_step_cut_free_complete [V L T].
∀(nonempty_v : V)(LS : lambda_structure L T)
(rules : set (sequent_rule V L))(osr : one_step_rule_set rules),
one_step_cut_free_complete nonempty_v LS rules osr ↔
∀(X : Type)(coval : X → set V)
(gamma : sequent V L)(gamma_nonempty : gamma ≠ [])
(gamma_simple : simple_modal_sequent gamma),
mod_seq_val_valid LS coval gamma gamma_nonempty
(simple_modal_sequent_is_prop_modal_prop gamma gamma_simple) →
∃(r : sequent_rule V L)(sigma : lambda_subst V L),
rules_r # rules r /#\
renaming_sigma # renaming sigma /#\
multi_subset (subst_sequent sigma (conclusion r)) gamma ∧
∀(i : nat)(i_less : i < length (assumptions r)),
prop_seq_val_valid nonempty_v coval
(subst_sequent sigma (nth (assumptions r) i i_less))
(propositional_renamed_one_step_assumptions rules r sigma
i i_less osr rules_r renaming_sigma).
End One_step_conditions.
Implicit Arguments one_step_sound [V L T].
Implicit Arguments valid_subst_n_conclusions [V L X].
Implicit Arguments simple_mod_weaken_rule_assumptions [V L].
Implicit Arguments one_step_complete [V L T].
Implicit Arguments one_step_cut_free_complete [V L T].
Implicit Arguments simple_one_step_cut_free_complete [V L T].