Syntactic proof of contraction and cut elimination, 5.6.2-3, 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
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).
∀(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
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.
∀(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
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).
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.
∀(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.
∀(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.