GRC Properties 3.14 - 3.15

The name of this module could be better. It is not about properties of cut about the two lemmas 3.14 and 3.15 on GRC_n.
The substitution lemma in the paper is wrong, see my paper "Formalizing Cut Elimination of Coalgebraic Logics in Coq" for a counter example.
Apart from fixing the substitution lemma, I generalize it to arbitrary substitution closed rule sets. From this generalized version I can simply derive two substitution lemmas for GRC_n and GR_n. The latter permits to prove admissibility of non-atomic axioms in GR_n (5.6.1) independently from cut elimination in GR_n.

Require Export admissibility rule_sets.

Section Cut_properties.

  Variable V : Type.
  Variable L : modal_operators.

Towards the substitution Lemma 3.14

The substitution in the paper is restricted to GRC_n. Moreover, it uses all propositional axioms, where actually only substitution instances of p, not p are needed. I prove first a generic version, that lets me derive substitution lemmas for GRC_n and GR_n later. The restriction to substitution instances of axioms will simplify the proof of 5.6.1 (non-atomic axioms in GR_n).
(Moreover, the version in the paper is wrong, one really needs non-atomic axioms of rank n + k!)

  Lemma generic_substitution_lemma :
    ∀(rules : set (sequent_rule V L))(hypothesis : set (sequent V L))
          (sigma : lambda_subst V L)(n k : nat)(gamma : sequent V L),
      subst_closed_rule_set rules →
      rank_sequent_set n hypothesis →
      rank_subst (S k) sigma →
      provable (rank_rules n (union is_ax_rule rules)) hypothesis gamma →
        provable (rank_rules (n + k) (union is_ax_rule rules))
                 (union (subst_Ax_n_set sigma (n + k))
                        (subst_sequent_set sigma hypothesis))
          (subst_sequent sigma gamma).

Substitution lemma 3.14 for GRC_n

  Lemma GRC_n_substitution_lemma :
    ∀(rules : set (sequent_rule V L))(hypothesis : set (sequent V L))
          (sigma : lambda_subst V L)(n k : nat)(gamma : sequent V L),
      one_step_rule_set rules →
      rank_sequent_set n hypothesis →
      rank_subst (S k) sigma →
      provable (GRC_n_set rules n) hypothesis gamma →
        provable (GRC_n_set rules (n + k))
                 (union (subst_Ax_n_set sigma (n + k))
                        (subst_sequent_set sigma hypothesis))
          (subst_sequent sigma gamma).

Substitution lemma for GR_n

  Lemma GR_n_substitution_lemma :
    ∀(rules : set (sequent_rule V L))(hypothesis : set (sequent V L))
          (sigma : lambda_subst V L)(n k : nat)(gamma : sequent V L),
      one_step_rule_set rules →
      rank_sequent_set n hypothesis →
      rank_subst (S k) sigma →
      provable (GR_n_set rules n) hypothesis gamma →
        provable (GR_n_set rules (n + k))
                 (union (subst_Ax_n_set sigma (n + k))
                        (subst_sequent_set sigma hypothesis))
          (subst_sequent sigma gamma).

And the variant for empty hypothesis
  Lemma GR_n_substitution_lemma_empty_hyp :
    ∀(rules : set (sequent_rule V L))
          (sigma : lambda_subst V L)(n k : nat)(gamma : sequent V L),
      one_step_rule_set rules →
      rank_subst (S k) sigma →
      provable (GR_n_set rules n) (empty_sequent_set V L) gamma →
        provable (GR_n_set rules (n + k))
                 (subst_Ax_n_set sigma (n + k))
          (subst_sequent sigma gamma).

Towards stratified GRC provability, 3.15


  Lemma proof_minimal_proof_rank :
    ∀(rules : set (sequent_rule V L))(s : sequent V L)(n : nat),
      ∀(p : proof rules (empty_sequent_set V L) s),
        minimal_proof_rank p ≤ n →
          provable (rank_rules n rules) (empty_sequent_set V L) s.

Proposition 3.15, stratified GRC provability

  Lemma rank_proof_GRC :
    ∀(rules : set (sequent_rule V L))(s : sequent V L),
      provable (GRC_set rules) (empty_sequent_set V L) s
         ↔
      ∃(n : nat),
        provable (GRC_n_set rules n) (empty_sequent_set V L) s.

Stratified GR provability

See also rank_proof_GR_fixed_rank in module weakening. This lemma does not depend on the set of one-step rules. On the other hand, the rank n can be greater than that of s.
  Lemma rank_proof_GR :
    ∀(rules : set (sequent_rule V L))(s : sequent V L),
      provable (GR_set rules) (empty_sequent_set V L) s
         ↔
      ∃(n : nat),
        provable (GR_n_set rules n) (empty_sequent_set V L) s.

End Cut_properties.