Properties of coalgebraic logics, Section 3
Weakening, 3.7 - 3.11
Require Export admissibility rule_sets.
Section Weakening.
Variable V : Type.
Variable L : modal_operators.
need a decidable equality on propositional constants
for limit_subst in stratified_one_step_rules
Towards 3.7
The characterization of ranked substitution instances of one-step rules.
Definition rank_weaken_subst_rule(rules : set (sequent_rule V L))
(n : nat)(posn : 0 < n)
: 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 (pred n) sigma ∧
rank_sequent n delta ∧
assumptions r_subst = map (subst_sequent sigma) (assumptions r_base) ∧
list_reorder (conclusion r_subst)
((subst_sequent sigma (conclusion r_base)) ++ delta).
Lemma rank_sequent_osr_subst_conclusion :
∀(r : sequent_rule V L)(sigma : lambda_subst V L)
(delta s : sequent V L)(n : nat),
one_step_rule r →
rank_subst (S n) sigma →
rank_sequent (2 + n) delta →
list_reorder s (subst_sequent sigma (conclusion r) ++ delta) →
rank_sequent (2 + n) s.
(n : nat)(posn : 0 < n)
: 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 (pred n) sigma ∧
rank_sequent n delta ∧
assumptions r_subst = map (subst_sequent sigma) (assumptions r_base) ∧
list_reorder (conclusion r_subst)
((subst_sequent sigma (conclusion r_base)) ++ delta).
Lemma rank_sequent_osr_subst_conclusion :
∀(r : sequent_rule V L)(sigma : lambda_subst V L)
(delta s : sequent V L)(n : nat),
one_step_rule r →
rank_subst (S n) sigma →
rank_sequent (2 + n) delta →
list_reorder s (subst_sequent sigma (conclusion r) ++ delta) →
rank_sequent (2 + n) s.
Lemma 3.7, page 13
Stratified weakend one-step substitution rules.
Lemma stratified_one_step_rules :
∀(nonempty_v : V)(rules : set (sequent_rule V L))
(n : nat)(npos : 0 < n),
one_step_rule_set rules →
set_equal (rank_rules n (weaken_subst_rule rules))
(rank_weaken_subst_rule rules n npos).
∀(nonempty_v : V)(rules : set (sequent_rule V L))
(n : nat)(npos : 0 < n),
one_step_rule_set rules →
set_equal (rank_rules n (weaken_subst_rule rules))
(rank_weaken_subst_rule rules n npos).
Towards 3.10, the equivalence of GR_n and GR
Lemma decrease_rank_R :
∀(n : nat)(r : sequent_rule V L)(rules : set (sequent_rule V L)),
one_step_rule_set rules →
weaken_subst_rule rules r →
rank_sequent n (conclusion r) →
every_nth (rank_sequent (pred n)) (assumptions r).
Lemma const_rank_R :
∀(n : nat)(r : sequent_rule V L)(rules : set (sequent_rule V L)),
one_step_rule_set rules →
weaken_subst_rule rules r →
rank_sequent n (conclusion r) →
every_nth (rank_sequent n) (assumptions r).
∀(n : nat)(r : sequent_rule V L)(rules : set (sequent_rule V L)),
one_step_rule_set rules →
weaken_subst_rule rules r →
rank_sequent n (conclusion r) →
every_nth (rank_sequent (pred n)) (assumptions r).
Lemma const_rank_R :
∀(n : nat)(r : sequent_rule V L)(rules : set (sequent_rule V L)),
one_step_rule_set rules →
weaken_subst_rule rules r →
rank_sequent n (conclusion r) →
every_nth (rank_sequent n) (assumptions r).
Backward application of rules in GR does not increase the rank.
Implicit property in 3.10.
Lemma const_rank_GR :
∀(n : nat)(r : sequent_rule V L)(rules : set (sequent_rule V L)),
one_step_rule_set rules →
GR_set rules r →
rank_sequent n (conclusion r) →
every_nth (rank_sequent n) (assumptions r).
∀(n : nat)(r : sequent_rule V L)(rules : set (sequent_rule V L)),
one_step_rule_set rules →
GR_set rules r →
rank_sequent n (conclusion r) →
every_nth (rank_sequent n) (assumptions r).
Lemma rank_proof_GR_fixed_rank :
∀(rules : set (sequent_rule V L))(n : nat)(s : sequent V L),
one_step_rule_set rules →
rank_sequent n s →
(provable (GR_set rules) (empty_sequent_set V L) s
↔
provable (GR_n_set rules n) (empty_sequent_set V L) s).
∀(rules : set (sequent_rule V L))(n : nat)(s : sequent V L),
one_step_rule_set rules →
rank_sequent n s →
(provable (GR_set rules) (empty_sequent_set V L) s
↔
provable (GR_n_set rules n) (empty_sequent_set V L) s).
Towards Lemma 3.9, page 14
Definition provable_subst_n_conclusions
(rules : set (sequent_rule V L))(n : nat)(npos : 0 < n)
: set (sequent V L) :=
fun(s : sequent V L) ⇒
∃(r : sequent_rule V L),
rank_weaken_subst_rule rules n npos r ∧
s = conclusion r ∧
every_nth
(provable (GR_n_set rules (pred n)) (empty_sequent_set V L))
(assumptions r).
(rules : set (sequent_rule V L))(n : nat)(npos : 0 < n)
: set (sequent V L) :=
fun(s : sequent V L) ⇒
∃(r : sequent_rule V L),
rank_weaken_subst_rule rules n npos r ∧
s = conclusion r ∧
every_nth
(provable (GR_n_set rules (pred n)) (empty_sequent_set V L))
(assumptions r).
Lemma rank_sequent_set_provable_subst_n_conclusions :
∀(rules : set (sequent_rule V L))(n : nat)(npos : 0 < n),
1 < n →
one_step_rule_set rules →
rank_sequent_set n (provable_subst_n_conclusions rules n npos).
Lemma multiset_provable_subst_n_conclusions :
∀(rules : set (sequent_rule V L))(n : nat)(npos : 0 < n),
sequent_multiset (provable_subst_n_conclusions rules n npos).
Lemma bounded_weakening_provable_subst_n_conclusions :
∀(rules : set (sequent_rule V L))(n : nat)(npos : 0 < n),
bounded_weakening_closed n (provable_subst_n_conclusions rules n npos).
Lemma 3.9, provability of GR_n from S(R) n assumptions
Lemma GR_n_provable_with_premises :
∀(nonempty_V : V)(rules : set (sequent_rule V L))
(n : nat)(npos : 0 < n)(gamma : sequent V L),
one_step_rule_set rules →
(provable (GR_n_set rules n) (empty_sequent_set V L) gamma ↔
provable (G_n_set V L n)
(provable_subst_n_conclusions rules n npos)
gamma).
∀(nonempty_V : V)(rules : set (sequent_rule V L))
(n : nat)(npos : 0 < n)(gamma : sequent V L),
one_step_rule_set rules →
(provable (GR_n_set rules n) (empty_sequent_set V L) gamma ↔
provable (G_n_set V L n)
(provable_subst_n_conclusions rules n npos)
gamma).
Lemma bounded_head_weakening_admissible_ax :
∀(rules : set (sequent_rule V L))(hyp : set (sequent V L))(n : nat)
(r : sequent_rule V L)(f : lambda_formula V L),
rule_multiset rules →
subset (rank_rules n is_ax_rule) rules →
is_ax_rule r →
rank_formula n f →
every_nth (rank_sequent n) (assumptions r) →
rank_sequent n (conclusion r) →
every_nth (fun s : sequent V L ⇒ provable rules hyp (f :: s))
(assumptions r) →
provable rules hyp (f :: conclusion r).
Lemma bounded_head_weakening_admissible_and :
∀(rules : set (sequent_rule V L))(hyp : set (sequent V L))(n : nat)
(r : sequent_rule V L)(f : lambda_formula V L),
rule_multiset rules →
subset (rank_rules n is_and_rule) rules →
is_and_rule r →
rank_formula n f →
every_nth (rank_sequent n) (assumptions r) →
rank_sequent n (conclusion r) →
every_nth (fun s : sequent V L ⇒ provable rules hyp (f :: s))
(assumptions r) →
provable rules hyp (f :: conclusion r).
Lemma bounded_head_weakening_admissible_neg_and :
∀(rules : set (sequent_rule V L))(hyp : set (sequent V L))(n : nat)
(r : sequent_rule V L)(f : lambda_formula V L),
rule_multiset rules →
subset (rank_rules n is_neg_and_rule) rules →
is_neg_and_rule r →
rank_formula n f →
every_nth (rank_sequent n) (assumptions r) →
rank_sequent n (conclusion r) →
every_nth (fun s : sequent V L ⇒ provable rules hyp (f :: s))
(assumptions r) →
provable rules hyp (f :: conclusion r).
Lemma bounded_head_weakening_admissible_neg_neg :
∀(rules : set (sequent_rule V L))(hyp : set (sequent V L))(n : nat)
(r : sequent_rule V L)(f : lambda_formula V L),
rule_multiset rules →
subset (rank_rules n is_neg_neg_rule) rules →
is_neg_neg_rule r →
rank_formula n f →
every_nth (rank_sequent n) (assumptions r) →
rank_sequent n (conclusion r) →
every_nth (fun s : sequent V L ⇒ provable rules hyp (f :: s))
(assumptions r) →
provable rules hyp (f :: conclusion r).
Lemma bounded_head_weakening_admissible_G_n_step :
∀(rules : set (sequent_rule V L))(hyp : set (sequent V L))(n : nat)
(r : sequent_rule V L)(f : lambda_formula V L),
rule_multiset rules →
subset (G_n_set V L n) rules →
G_n_set V L n r →
rank_formula n f →
every_nth (rank_sequent n) (assumptions r) →
rank_sequent n (conclusion r) →
every_nth (fun s : sequent V L ⇒ provable rules hyp (f :: s))
(assumptions r) →
provable rules hyp (f :: conclusion r).
Lemma bounded_head_weakening_admissible_G_n_ind :
∀(hyp : set (sequent V L))(s : sequent V L)(f : lambda_formula V L)
(n : nat),
bounded_weakening_closed n hyp →
sequent_multiset hyp →
rank_formula n f →
rank_sequent n s →
provable (G_n_set V L n) hyp s →
provable (G_n_set V L n) hyp (f :: s).
Bounded weakening is admissible in G_n + H,
provided H is closed under bounded weakening used in 3.11
Lemma weakening_admissible_Gn :
∀(n : nat)(hyp : set (sequent V L)),
bounded_weakening_closed n hyp →
sequent_multiset hyp →
admissible_rule_set
(G_n_set V L n) hyp
(bounded_weakening_rules V L n).
∀(n : nat)(hyp : set (sequent V L)),
bounded_weakening_closed n hyp →
sequent_multiset hyp →
admissible_rule_set
(G_n_set V L n) hyp
(bounded_weakening_rules V L n).
Lemma weakening_admissible_GR_n :
∀(nonempty_V : V)(rules : set (sequent_rule V L))(n : nat),
0 < n →
one_step_rule_set rules →
admissible_rule_set
(GR_n_set rules n) (empty_sequent_set V L)
(bounded_weakening_rules V L n).
∀(nonempty_V : V)(rules : set (sequent_rule V L))(n : nat),
0 < n →
one_step_rule_set rules →
admissible_rule_set
(GR_n_set rules n) (empty_sequent_set V L)
(bounded_weakening_rules V L n).
Theorem weakening_admissible_GR :
∀(nonempty_V : V)(rules : set (sequent_rule V L)),
one_step_rule_set rules →
admissible_rule_set
(GR_set rules) (empty_sequent_set V L)
(full_weakening_rules V L).
∀(nonempty_V : V)(rules : set (sequent_rule V L)),
one_step_rule_set rules →
admissible_rule_set
(GR_set rules) (empty_sequent_set V L)
(full_weakening_rules V L).
Towards weakening in GRC_n
Lemma bounded_head_weakening_admissible_R :
∀(rules osr : set (sequent_rule V L))(n : nat)
(r : sequent_rule V L)(f : lambda_formula V L),
rule_multiset rules →
one_step_rule_set osr →
subset (rank_rules n (weaken_subst_rule osr)) rules →
weaken_subst_rule osr r →
rank_formula n f →
every_nth (rank_sequent n) (assumptions r) →
rank_sequent n (conclusion r) →
every_nth (fun s : sequent V L ⇒
provable rules (empty_sequent_set V L) (s) ∧
provable rules (empty_sequent_set V L) (f :: s))
(assumptions r) →
provable rules (empty_sequent_set V L) (f :: conclusion r).
∀(rules osr : set (sequent_rule V L))(n : nat)
(r : sequent_rule V L)(f : lambda_formula V L),
rule_multiset rules →
one_step_rule_set osr →
subset (rank_rules n (weaken_subst_rule osr)) rules →
weaken_subst_rule osr r →
rank_formula n f →
every_nth (rank_sequent n) (assumptions r) →
rank_sequent n (conclusion r) →
every_nth (fun s : sequent V L ⇒
provable rules (empty_sequent_set V L) (s) ∧
provable rules (empty_sequent_set V L) (f :: s))
(assumptions r) →
provable rules (empty_sequent_set V L) (f :: conclusion r).
Induction step for cut
Lemma bounded_head_weakening_admissible_cut :
∀(rules : set (sequent_rule V L))(n : nat)
(r : sequent_rule V L)(f : lambda_formula V L),
rule_multiset rules →
subset (rank_rules n is_cut_rule) rules →
is_cut_rule r →
rank_formula n f →
every_nth (rank_sequent n) (assumptions r) →
rank_sequent n (conclusion r) →
every_nth (fun s : sequent V L ⇒
provable rules (empty_sequent_set V L) (s) ∧
provable rules (empty_sequent_set V L) (f :: s))
(assumptions r) →
provable rules (empty_sequent_set V L) (f :: conclusion r).
∀(rules : set (sequent_rule V L))(n : nat)
(r : sequent_rule V L)(f : lambda_formula V L),
rule_multiset rules →
subset (rank_rules n is_cut_rule) rules →
is_cut_rule r →
rank_formula n f →
every_nth (rank_sequent n) (assumptions r) →
rank_sequent n (conclusion r) →
every_nth (fun s : sequent V L ⇒
provable rules (empty_sequent_set V L) (s) ∧
provable rules (empty_sequent_set V L) (f :: s))
(assumptions r) →
provable rules (empty_sequent_set V L) (f :: conclusion r).
Do the induction
Lemma bounded_head_weakening_admissible_GRC_n :
∀(rules : set (sequent_rule V L))(n : nat)
(s : sequent V L)(f : lambda_formula V L),
one_step_rule_set rules →
rank_formula n f →
proof (GRC_n_set rules n) (empty_sequent_set V L) s →
provable (GRC_n_set rules n) (empty_sequent_set V L) (s) ∧
provable (GRC_n_set rules n) (empty_sequent_set V L) (f :: s).
∀(rules : set (sequent_rule V L))(n : nat)
(s : sequent V L)(f : lambda_formula V L),
one_step_rule_set rules →
rank_formula n f →
proof (GRC_n_set rules n) (empty_sequent_set V L) s →
provable (GRC_n_set rules n) (empty_sequent_set V L) (s) ∧
provable (GRC_n_set rules n) (empty_sequent_set V L) (f :: s).
Lemma weakening_admissible_GRC_n :
∀(rules : set (sequent_rule V L))(n : nat),
one_step_rule_set rules →
admissible_rule_set
(GRC_n_set rules n) (empty_sequent_set V L)
(bounded_weakening_rules V L n).
∀(rules : set (sequent_rule V L))(n : nat),
one_step_rule_set rules →
admissible_rule_set
(GRC_n_set rules n) (empty_sequent_set V L)
(bounded_weakening_rules V L n).
List weakening
Lift weakening of a single formula to weakening with a sequent.
Lemma evar_bug_list_weakening_admissible_GRC_n :
∀(rules : set (sequent_rule V L))(n : nat)
(s1 s2 : sequent V L),
one_step_rule_set rules →
rank_sequent n s1 →
rank_sequent n s2 →
provable (GRC_n_set rules n) (empty_sequent_set V L) s1 →
provable (GRC_n_set rules n) (empty_sequent_set V L) (s1 ++ s2).
Lemma generic_bounded_list_weakening :
∀(rules : set (sequent_rule V L))(hyp : set (sequent V L))(n : nat)
(s1 s2 : sequent V L),
rule_multiset rules →
admissible_rule_set rules hyp
(bounded_weakening_rules V L n) →
sequent_multiset hyp →
rank_sequent n s1 →
rank_sequent n s2 →
provable rules hyp s1 →
provable rules hyp (s1 ++ s2).
Lemma list_weakening_admissible_G_n_hyp :
∀(hyp : set (sequent V L))(n : nat)(s1 s2 : sequent V L),
sequent_multiset hyp →
bounded_weakening_closed n hyp →
rank_sequent n s1 →
rank_sequent n s2 →
provable (G_n_set V L n) hyp s1 →
provable (G_n_set V L n) hyp (s1 ++ s2).
Lemma list_weakening_admissible_GR_n :
∀(nonempty_v : V)(rules : set (sequent_rule V L))(n : nat)
(s1 s2 : sequent V L),
0 < n →
one_step_rule_set rules →
rank_sequent n s2 →
provable (GR_n_set rules n) (empty_sequent_set V L) s1 →
provable (GR_n_set rules n) (empty_sequent_set V L) (s1 ++ s2).
Lemma list_weakening_admissible_GRC_n :
∀(rules : set (sequent_rule V L))(n : nat)
(s1 s2 : sequent V L),
one_step_rule_set rules →
rank_sequent n s1 →
rank_sequent n s2 →
provable (GRC_n_set rules n) (empty_sequent_set V L) s1 →
provable (GRC_n_set rules n) (empty_sequent_set V L) (s1 ++ s2).
End Weakening.
Implicit Arguments provable_subst_n_conclusions [V L].
∀(rules : set (sequent_rule V L))(n : nat)
(s1 s2 : sequent V L),
one_step_rule_set rules →
rank_sequent n s1 →
rank_sequent n s2 →
provable (GRC_n_set rules n) (empty_sequent_set V L) s1 →
provable (GRC_n_set rules n) (empty_sequent_set V L) (s1 ++ s2).
Lemma generic_bounded_list_weakening :
∀(rules : set (sequent_rule V L))(hyp : set (sequent V L))(n : nat)
(s1 s2 : sequent V L),
rule_multiset rules →
admissible_rule_set rules hyp
(bounded_weakening_rules V L n) →
sequent_multiset hyp →
rank_sequent n s1 →
rank_sequent n s2 →
provable rules hyp s1 →
provable rules hyp (s1 ++ s2).
Lemma list_weakening_admissible_G_n_hyp :
∀(hyp : set (sequent V L))(n : nat)(s1 s2 : sequent V L),
sequent_multiset hyp →
bounded_weakening_closed n hyp →
rank_sequent n s1 →
rank_sequent n s2 →
provable (G_n_set V L n) hyp s1 →
provable (G_n_set V L n) hyp (s1 ++ s2).
Lemma list_weakening_admissible_GR_n :
∀(nonempty_v : V)(rules : set (sequent_rule V L))(n : nat)
(s1 s2 : sequent V L),
0 < n →
one_step_rule_set rules →
rank_sequent n s2 →
provable (GR_n_set rules n) (empty_sequent_set V L) s1 →
provable (GR_n_set rules n) (empty_sequent_set V L) (s1 ++ s2).
Lemma list_weakening_admissible_GRC_n :
∀(rules : set (sequent_rule V L))(n : nat)
(s1 s2 : sequent V L),
one_step_rule_set rules →
rank_sequent n s1 →
rank_sequent n s2 →
provable (GRC_n_set rules n) (empty_sequent_set V L) s1 →
provable (GRC_n_set rules n) (empty_sequent_set V L) (s1 ++ s2).
End Weakening.
Implicit Arguments provable_subst_n_conclusions [V L].