syntactic

Syntactic proof of contraction and cut elimination, 5.6.2-3, 5.7

This module puts the proof for contraction in GR_n (5.6.2) and cut elimination in GR_n (5.6.3) together. The different cases of this proof are spread over several files. This module contains the double induction for cut elimination, the final Lemma 5.6 and Theorem 5.7.

Require Export osr_cut mixed_cut prop_cut.

Section Syntactic_cut.

  Variable V : Type.
  Variable L : modal_operators.

  Variable op_eq : eq_type (operator L).
  Variable v_eq : eq_type V.

Towards proposition 5.6 (2-3), page 28

Nested induction for cut elimination

This lemma does the nested induction in G_n + H and distinguishes the major cases.

  Lemma syntactic_GR_n_cut_head_elimination_ind :
   ∀(rules : set (sequent_rule V L))(n : nat)(ssn_pos : 0 < 2 + n),
      countably_infinite V →
      one_step_rule_set rules →
      absorbs_congruence rules →
      absorbs_contraction op_eq v_eq rules →
      absorbs_cut op_eq v_eq rules →
      (∀(s : sequent V L)(f : lambda_formula V L),
         provable (GR_n_set rules (2 + n)) (empty_sequent_set V L)
                  (f :: f :: s) →
           provable (GR_n_set rules (2 + n)) (empty_sequent_set V L) (f :: s))
      →
      (∀(s : sequent V L),
           provable (GRC_n_set rules (S n)) (empty_sequent_set V L) s →
             provable (GR_n_set rules (S n)) (empty_sequent_set V L) s)
      →
         ∀(m sd : nat)
               (f : lambda_formula V L)(r q : sequent V L)
               (p_fq : proof (G_n_set V L (2 + n))
                          (provable_subst_n_conclusions rules (2 + n) ssn_pos)
                          (f :: q))
               (p_nfr : proof (G_n_set V L (2 + n))
                          (provable_subst_n_conclusions rules (2 + n) ssn_pos)
                          ((lf_neg f ) :: r)),
           proof_depth p_fq + proof_depth p_nfr ≤ sd →
           formula_measure f < m →
             provable (G_n_set V L (2 + n))
                      (provable_subst_n_conclusions rules (2 + n) ssn_pos)
               (q ++ r).

Modal rank induction step for cut elimination

This lemma reduces general cut-elimination to cut-elimination at head position in the calculus G_n + H The lemma also adds rank assumptions to the induction hypothesis.

  Lemma syntactic_GR_n_cut_elimination :
    ∀(rules : set (sequent_rule V L))(n : nat),
      countably_infinite V →
      one_step_rule_set rules →
      absorbs_congruence rules →
      absorbs_contraction op_eq v_eq rules →
      absorbs_cut op_eq v_eq rules →
      (∀(s : sequent V L)(f : lambda_formula V L),
         provable (GR_n_set rules (2 + n)) (empty_sequent_set V L)
                  (f :: f :: s) →
           provable (GR_n_set rules (2 + n)) (empty_sequent_set V L) (f :: s))
      →
      (∀(s : sequent V L),
         provable (GRC_n_set rules (S n)) (empty_sequent_set V L) s →
           provable (GR_n_set rules (S n)) (empty_sequent_set V L) s)
      →
        ∀(s : sequent V L),
           provable (GRC_n_set rules (2 + n)) (empty_sequent_set V L) s →
             provable (GR_n_set rules (2 + n)) (empty_sequent_set V L) s.

Proposition 5.6 (2-3) mutual induction lemma

Finally, this Lemma formalizes case 2 and 3 of Proposition 5.6. It proves contraction and cut elimination by mutual induction over the modal rank.

  Lemma syntactic_GR_n_cc :
    ∀(rules : set (sequent_rule V L))(n : nat),
      countably_infinite V →
      one_step_rule_set rules →
      absorbs_congruence rules →
      absorbs_contraction op_eq v_eq rules →
      absorbs_cut op_eq v_eq rules →
        (∀(s : sequent V L)(f : lambda_formula V L),
           provable (GR_n_set rules n) (empty_sequent_set V L)
                    (f :: f :: s) →
             provable (GR_n_set rules n) (empty_sequent_set V L)
                      (f :: s))
        ∧
        (∀(s : sequent V L),
           provable (GRC_n_set rules n) (empty_sequent_set V L) s →
             provable (GR_n_set rules n) (empty_sequent_set V L) s ).

Proposition 5.7, page 32

5.7, cut part

  Theorem syntactic_admissible_cut :
    ∀(rules : set (sequent_rule V L)),
      countably_infinite V →
      one_step_rule_set rules →
      absorbs_congruence rules →
      absorbs_contraction op_eq v_eq rules →
      absorbs_cut op_eq v_eq rules →
        admissible_rule_set (GR_set rules) (empty_sequent_set V L) is_cut_rule.

5.7, contraction part

  Theorem syntactic_admissible_contraction :
    ∀(osr : set (sequent_rule V L)),
      countably_infinite V →
      one_step_rule_set osr →
      absorbs_congruence osr →
      absorbs_contraction op_eq v_eq osr →
      absorbs_cut op_eq v_eq osr →
        admissible_rule_set (GR_set osr) (empty_sequent_set V L)
          is_contraction_rule.

End Syntactic_cut.