Syntactic cut elimination, Section 5
Absorbtion properties and non-atomic axioms, 5.1 - 5.6.1
Require Export factor_subst propositional_properties backward_substitution
cut_properties.
Section Absorbtion.
Variable V : Type.
Variable L : modal_operators.
Need decidable equalities on operators and variables
for the support in absorbs_contraction.
Two properties about one-step rules
Lemma one_step_rule_simple_modal_conclusion_subst_reorder :
∀(rules : set (sequent_rule V L))(sigma : lambda_subst V L)
(r : sequent_rule V L)(s : sequent V L),
one_step_rule_set rules →
rules r →
renaming sigma →
list_reorder s (subst_sequent sigma (conclusion r)) →
simple_modal_sequent s.
Lemma one_step_rule_propositional_subst_assumptions :
∀(rules : set (sequent_rule V L))(sigma : lambda_subst V L)
(r : sequent_rule V L),
one_step_rule_set rules →
rules r →
renaming sigma →
every_nth propositional_sequent
(map (subst_sequent sigma) (assumptions r)).
Towards absorbs congruence, Definition 5.1
Definition congruence_assumption_list(pv qv : list (lambda_formula V L))
: list (list (lambda_formula V L)) :=
let pqv := combine pv qv
in
(map (fun pq ⇒ [lf_neg (fst pq); snd pq]) pqv) ++
(map (fun pq ⇒ [fst pq; lf_neg (snd pq)]) pqv).
Definition congruence_assumptions(n : nat)
(pv qv : counted_list (lambda_formula V L) n)
: set (sequent V L) :=
reordered_sequent_list_set
(congruence_assumption_list (list_of_counted_list pv)
(list_of_counted_list qv)).
Lemma congruence_assumptions_char :
∀(n : nat)(args : counted_list (lambda_formula V L) n)
(s : sequent V L),
every_nth prop_form (list_of_counted_list args) →
congruence_assumptions n args args s →
(∃(v : V), s = [lf_neg (lf_prop v); lf_prop v] ∨
s = [lf_prop v; lf_neg (lf_prop v)]
) ∧ rank_sequent 1 s.
Lemma rank_sequent_set_congruence_assumptions :
∀(n : nat)(args : counted_list (lambda_formula V L) n),
every_nth prop_form (list_of_counted_list args) →
rank_sequent_set 1 (congruence_assumptions n args args).
Lemma congruence_assumptions_subset :
∀(n r : nat)(args : counted_list (lambda_formula V L) n)
(sigma : lambda_subst V L),
rank_subst (S r) sigma →
every_nth prop_form (list_of_counted_list args) →
subset (subst_sequent_set sigma (congruence_assumptions n args args))
(subst_Ax_n_set sigma (2 + r)).
Lemma congruence_assumptions_provable_with_ax :
∀(rules : set (sequent_rule V L))(n : nat)
(args : counted_list (lambda_formula V L) n)
(s : sequent V L),
subset (rank_rules 1 is_ax_rule) rules →
every_nth prop_form (list_of_counted_list args) →
(provable rules (congruence_assumptions n args args) s ↔
provable rules (empty_sequent_set V L) s).
: list (list (lambda_formula V L)) :=
let pqv := combine pv qv
in
(map (fun pq ⇒ [lf_neg (fst pq); snd pq]) pqv) ++
(map (fun pq ⇒ [fst pq; lf_neg (snd pq)]) pqv).
Definition congruence_assumptions(n : nat)
(pv qv : counted_list (lambda_formula V L) n)
: set (sequent V L) :=
reordered_sequent_list_set
(congruence_assumption_list (list_of_counted_list pv)
(list_of_counted_list qv)).
Lemma congruence_assumptions_char :
∀(n : nat)(args : counted_list (lambda_formula V L) n)
(s : sequent V L),
every_nth prop_form (list_of_counted_list args) →
congruence_assumptions n args args s →
(∃(v : V), s = [lf_neg (lf_prop v); lf_prop v] ∨
s = [lf_prop v; lf_neg (lf_prop v)]
) ∧ rank_sequent 1 s.
Lemma rank_sequent_set_congruence_assumptions :
∀(n : nat)(args : counted_list (lambda_formula V L) n),
every_nth prop_form (list_of_counted_list args) →
rank_sequent_set 1 (congruence_assumptions n args args).
Lemma congruence_assumptions_subset :
∀(n r : nat)(args : counted_list (lambda_formula V L) n)
(sigma : lambda_subst V L),
rank_subst (S r) sigma →
every_nth prop_form (list_of_counted_list args) →
subset (subst_sequent_set sigma (congruence_assumptions n args args))
(subst_Ax_n_set sigma (2 + r)).
Lemma congruence_assumptions_provable_with_ax :
∀(rules : set (sequent_rule V L))(n : nat)
(args : counted_list (lambda_formula V L) n)
(s : sequent V L),
subset (rank_rules 1 is_ax_rule) rules →
every_nth prop_form (list_of_counted_list args) →
(provable rules (congruence_assumptions n args args) s ↔
provable rules (empty_sequent_set V L) s).
Definition absorbs_congruence(rules : set (sequent_rule V L)) : Prop :=
∀(op : operator L)
(pv qv : counted_list (lambda_formula V L) (arity L op)),
every_nth prop_form (list_of_counted_list pv) →
every_nth prop_form (list_of_counted_list qv) →
∃(r : sequent_rule V L)(sigma : lambda_subst V L),
rules r ∧
rank_subst 1 sigma ∧
multi_subset (subst_sequent sigma (conclusion r))
[lf_neg (lf_modal op pv); lf_modal op qv]
∧
every_nth
(fun(s : sequent V L) ⇒
provable (GC_n_set V L 1)
(congruence_assumptions (arity L op) pv qv)
(subst_sequent sigma s))
(assumptions r).
∀(op : operator L)
(pv qv : counted_list (lambda_formula V L) (arity L op)),
every_nth prop_form (list_of_counted_list pv) →
every_nth prop_form (list_of_counted_list qv) →
∃(r : sequent_rule V L)(sigma : lambda_subst V L),
rules r ∧
rank_subst 1 sigma ∧
multi_subset (subst_sequent sigma (conclusion r))
[lf_neg (lf_modal op pv); lf_modal op qv]
∧
every_nth
(fun(s : sequent V L) ⇒
provable (GC_n_set V L 1)
(congruence_assumptions (arity L op) pv qv)
(subst_sequent sigma s))
(assumptions r).
Definition absorbs_contraction(rules : set (sequent_rule V L)) : Prop :=
∀(or : sequent_rule V L)(sigma : lambda_subst V L),
rules or →
renaming sigma →
∃(cr : sequent_rule V L)(rho : lambda_subst V L),
rules cr ∧ renaming rho ∧
multi_subset
(subst_sequent rho (conclusion cr))
(sequent_support op_eq v_eq (subst_sequent sigma (conclusion or)))
∧
every_nth
(fun ca ⇒
provable (GC_n_set V L 1)
(reordered_sequent_list_set
(map (subst_sequent sigma) (assumptions or)))
(subst_sequent rho ca))
(assumptions cr).
Lemma absorbs_contraction_head :
∀(rules : set (sequent_rule V L))(or : sequent_rule V L)
(sigma : lambda_subst V L)(f : lambda_formula V L)(s : sequent V L),
one_step_rule_set rules →
absorbs_contraction rules →
rules or →
renaming sigma →
list_reorder (f :: f :: s) (subst_sequent sigma (conclusion or)) →
∃(cr : sequent_rule V L)(rho : lambda_subst V L)
(delta : sequent V L),
rules cr ∧ renaming rho ∧ simple_modal_sequent delta ∧
list_reorder (f :: s) ((subst_sequent rho (conclusion cr)) ++ delta)
∧
every_nth
(fun ca ⇒
provable (GC_n_set V L 1)
(reordered_sequent_list_set
(map (subst_sequent sigma) (assumptions or)))
(subst_sequent rho ca))
(assumptions cr).
Definition absorbs_cut(rules : set (sequent_rule V L)) : Prop :=
∀(rl rr : sequent_rule V L)(sl sr : lambda_subst V L)(nl nr : nat)
(nl_less : nl < length (subst_sequent sl (conclusion rl)))
(nr_less : nr < length (subst_sequent sr (conclusion rr))),
rules rl → rules rr →
renaming sl → renaming sr →
lf_neg (nth (subst_sequent sl (conclusion rl)) nl nl_less) =
nth (subst_sequent sr (conclusion rr)) nr nr_less →
∃(rb : sequent_rule V L)(sb : lambda_subst V L),
rules rb ∧ renaming sb ∧
multi_subset
(sequent_support op_eq v_eq (subst_sequent sb (conclusion rb)))
((cutout_nth (subst_sequent sl (conclusion rl)) nl) ++
(cutout_nth (subst_sequent sr (conclusion rr)) nr)) ∧
every_nth
(fun ba ⇒
provable (GC_n_set V L 1)
(reordered_sequent_list_set
((map (subst_sequent sl) (assumptions rl)) ++
(map (subst_sequent sr) (assumptions rr))))
(subst_sequent sb ba))
(assumptions rb).
Lemma GR_n_non_atomic_axiom_head :
∀(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 →
rank_sequent (2 + n) s →
rank_formula (2 + n) f →
(∀ (s : sequent V L) (f : lambda_formula V L),
rank_sequent (S n) s →
rank_formula (S n) f →
provable (GR_n_set rules (S n)) (empty_sequent_set V L)
(f :: lf_neg f :: s)) →
provable (GR_n_set rules (2 + n)) (empty_sequent_set V L)
(f :: lf_neg f :: s).
∀(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 →
rank_sequent (2 + n) s →
rank_formula (2 + n) f →
(∀ (s : sequent V L) (f : lambda_formula V L),
rank_sequent (S n) s →
rank_formula (S n) f →
provable (GR_n_set rules (S n)) (empty_sequent_set V L)
(f :: lf_neg f :: s)) →
provable (GR_n_set rules (2 + n)) (empty_sequent_set V L)
(f :: lf_neg f :: s).
Lemma syntactic_GR_n_non_atomic_axioms :
∀(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 →
rank_sequent n s →
rank_formula n f →
provable (GR_n_set rules n) (empty_sequent_set V L)
(f :: (lf_neg f) :: s).
Lemma syntactic_GR_n_provable_subst_Ax :
∀(rules : set (sequent_rule V L))(hyp : set (sequent V L))
(sigma : lambda_subst V L)(n : nat)(s : sequent V L),
countably_infinite V →
one_step_rule_set rules →
absorbs_congruence rules →
rank_subst n sigma →
subst_Ax_n_set sigma n s →
provable (GR_n_set rules n) hyp s.
End Absorbtion.
Implicit Arguments absorbs_congruence [V L].
Implicit Arguments absorbs_contraction [V L].
Implicit Arguments absorbs_contraction_head [V L].
Implicit Arguments absorbs_cut [V L].
∀(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 →
rank_sequent n s →
rank_formula n f →
provable (GR_n_set rules n) (empty_sequent_set V L)
(f :: (lf_neg f) :: s).
Lemma syntactic_GR_n_provable_subst_Ax :
∀(rules : set (sequent_rule V L))(hyp : set (sequent V L))
(sigma : lambda_subst V L)(n : nat)(s : sequent V L),
countably_infinite V →
one_step_rule_set rules →
absorbs_congruence rules →
rank_subst n sigma →
subst_Ax_n_set sigma n s →
provable (GR_n_set rules n) hyp s.
End Absorbtion.
Implicit Arguments absorbs_congruence [V L].
Implicit Arguments absorbs_contraction [V L].
Implicit Arguments absorbs_contraction_head [V L].
Implicit Arguments absorbs_cut [V L].