Admissibility of contraction, 5.6.2
Require Export absorb.
Section Contraction_ind.
Variable V : Type.
Variable L : modal_operators.
Variable op_eq : eq_type (operator L).
Variable v_eq : eq_type V.
Lemma provable_assumptions_contraction_rule :
∀(rules : set (sequent_rule V L))(n : nat)
(r cr : sequent_rule V L)
(sigma inj_sigma rsigma rho : lambda_subst V L),
countably_infinite V →
one_step_rule_set rules →
absorbs_congruence rules →
rules r →
rules cr →
rank_subst (S n) inj_sigma →
renaming rsigma →
renaming rho →
subst_eq_on_vars sigma (subst_compose inj_sigma rsigma)
(prop_var_sequent (conclusion r)) →
(∀(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) →
every_nth
(provable (GR_n_set rules (S n)) (empty_sequent_set V L))
(map (subst_sequent sigma) (assumptions r)) →
every_nth
(fun ca : sequent V L ⇒
provable (GC_n_set V L 1)
(reordered_sequent_list_set
(map (subst_sequent rsigma) (assumptions r)))
(subst_sequent rho ca))
(assumptions cr)
→
every_nth (provable (GR_n_set rules (S n)) (empty_sequent_set V L))
(map (subst_sequent (subst_compose inj_sigma rho)) (assumptions cr)).
Lemma head_contraction_closed_provable_subst_n_conclusions_ind :
∀(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 →
(∀(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) →
head_contraction_closed
(provable_subst_n_conclusions rules (2 + n) (lt_0_Sn (S n))).
Lemma syntactic_GR_n_contraction_ind :
∀(rules : set (sequent_rule V L))(n : nat)
(s : sequent V L)(f : lambda_formula V L),
countably_infinite V →
one_step_rule_set rules →
absorbs_congruence rules →
absorbs_contraction op_eq v_eq rules →
(∀(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) →
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).
Lemma syntactic_support_contraction_ind :
∀(rules : set (sequent_rule V L))(n : nat)(s1 s2 : sequent V L),
(∀(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)) →
provable (GR_n_set rules n) (empty_sequent_set V L) (s1 ++ s2) →
incl s1 s2 →
provable (GR_n_set rules n) (empty_sequent_set V L) s2.
Lemma syntactic_support_contraction :
∀(rules : set (sequent_rule V L))(n : nat)(s : sequent V L),
(∀(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)) →
provable (GR_n_set rules n) (empty_sequent_set V L) s →
provable (GR_n_set rules n) (empty_sequent_set V L)
(sequent_support op_eq v_eq s).
End Contraction_ind.