Properties of coalgebraic logics, Section 3

Weakening, 3.7 - 3.11

This module formalizes the characterization of GR_n provability 3.7 and 3.9, Lemma 3.10 and the weakening Lemma 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
  Variable v_eq : eq_type V.

Towards 3.7

The characterization of ranked substitution instances of one-step rules.
Stratified weakend substitution rules, right hand side in Lem 3.7, page 13. See also simple_mod_weaken_rule in module one_step_conditions.
  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.


Lemma 3.7, page 13

Stratified weakend one-step substitution rules.
This result needs the nonempty V to rule out a border case for rank 0 (n = 1) in the inclusion from right to left
  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).

Towards 3.10, the equivalence of GR_n and GR

Backward application of rules in S(R) decreases the rank by one. Needed for 3.10, where the rank must not increase.
  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).

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

Lemma 3.10, equivalence of GR_n and GR

Page 14. See also rank_proof_GR in module cut_properties.
  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).

Towards Lemma 3.9, page 14

GR_n provability coincides with G_n provability with S(R) n conclusions as axioms
Define first the set of S(R) n conclusions
  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).

Some properties that are needed later


  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

The nonempty V assumption is only needed for the implication from right to left. The assumption about the rank of Gamma is not needed.
  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).

Towards the weakening lemma 3.11


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

Weakening Lemma 3.11, page 14

bounded weakening is admissible in GR_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).

Another weakening lemma

Weakening is admissible in GR, comment on page 15
  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).

Towards weakening in GRC_n

This is a missing lemma in the paper. It is needed in the proof of 4.13 to split the propositional part. In contrast to the previous weakening lemma, the GRC_n result cannot be proven via lemma 3.9. Here we have to do a full induction over the proof tree.
Induction step for one-step rules.
  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).

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

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

Weakening lemma for GRC_n

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

List weakening

Lift weakening of a single formula to weakening with a sequent.
XXX Keep the following lemma for reproducing the print evar bug only.
  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].