Inversion, 3.12 - 3.13
Need decidable equality on propositional constants
for the unused Lemma inversion_admissible_GR_n (3.13)
Definition conj_head_inversion_closed(ss : set (sequent V L)) : Prop :=
∀(sr : sequent V L)(f1 f2 : lambda_formula V L),
ss ((lf_and f1 f2) :: sr) →
ss (f1 :: sr) ∧ ss (f2 :: sr).
Definition disj_head_inversion_closed(ss : set (sequent V L)) : Prop :=
∀(sr : sequent V L)(f1 f2 : lambda_formula V L),
ss ((lf_neg (lf_and f1 f2)) :: sr) →
ss ((lf_neg f1) :: (lf_neg f2) :: sr).
Definition neg_head_inversion_closed(ss : set (sequent V L)) : Prop :=
∀(sr : sequent V L)(f : lambda_formula V L),
ss ((lf_neg (lf_neg f)) :: sr) →
ss (f :: sr).
Definition head_inversion_closed(ss : set (sequent V L)) : Prop :=
conj_head_inversion_closed ss ∧
disj_head_inversion_closed ss ∧
neg_head_inversion_closed ss.
Lemma head_inversion_closed_empty :
head_inversion_closed (empty_sequent_set V L).
Lemma sequent_other_axiom_G_n_set :
∀(n : nat)(f1 : lambda_formula V L)(s1 s2 : sequent V L),
simple_tautology (f1 :: s1) →
rank_sequent n (f1 :: s1) →
(rank_formula n f1 → rank_sequent n s2) →
(not (neg_form_maybe prop_form f1)) →
G_n_set V L n {| assumptions := []; conclusion := s2 ++ s1 |}.
Lemma other_axiom_G_n_set :
∀(n : nat)(f1 f2 : lambda_formula V L)(s : sequent V L),
simple_tautology (f1 :: s) →
rank_sequent n (f1 :: s) →
(rank_formula n f1 → rank_formula n f2) →
(not (neg_form_maybe prop_form f1)) →
G_n_set V L n {| assumptions := []; conclusion := f2 :: s |}.
Lemma list_subproofs_head_admissible :
∀(hyp : set (sequent V L))(n d : nat)
(f : lambda_formula V L)(sl sr new_ass : sequent V L)
(ass : list (sequent V L))
(pl : dep_list (sequent V L) (proof (G_n_set V L n) hyp)
(map (add_context (f :: sl) sr) ass)),
every_dep_nth
(fun(s : sequent V L)(p : proof (G_n_set V L n) hyp s) ⇒
proof_depth p ≤ d)
(map (add_context (f :: sl) sr) ass) pl →
every_dep_nth
(fun(a : sequent V L)(p_a : proof (G_n_set V L n) hyp a) ⇒
∀(d : nat)(a_tl : sequent V L),
a = f :: a_tl →
proof_depth p_a ≤ d →
∃(op : proof (G_n_set V L n) hyp (new_ass ++ a_tl)),
proof_depth op ≤ d)
(map (add_context (f :: sl) sr) ass)
pl
→
∃(opl : dep_list (sequent V L) (proof (G_n_set V L n) hyp)
(map (add_context (new_ass ++ sl) sr) ass)),
every_dep_nth
(fun(s : sequent V L)(p : proof (G_n_set V L n) hyp s) ⇒
proof_depth p ≤ d)
(map (add_context (new_ass ++ sl) sr) ass) opl.
Lemma subproofs_head_admissible :
∀(hyp : set (sequent V L))(n d : nat)
(f1 f2 : lambda_formula V L)(sl sr : sequent V L)
(ass : list (sequent V L))
(pl : dep_list (sequent V L) (proof (G_n_set V L n) hyp)
(map (add_context (f1 :: sl) sr) ass)),
every_dep_nth
(fun(s : sequent V L)(p : proof (G_n_set V L n) hyp s) ⇒
proof_depth p ≤ d)
(map (add_context (f1 :: sl) sr) ass) pl →
every_dep_nth
(fun(a : sequent V L)(p_a : proof (G_n_set V L n) hyp a) ⇒
∀(d : nat)(a_tl : sequent V L),
a = f1 :: a_tl →
proof_depth p_a ≤ d →
∃(op : proof (G_n_set V L n) hyp (f2 :: a_tl)),
proof_depth op ≤ d)
(map (add_context (f1 :: sl) sr) ass)
pl
→
∃(opl : dep_list (sequent V L) (proof (G_n_set V L n) hyp)
(map (add_context (f2 :: sl) sr) ass)),
every_dep_nth
(fun(s : sequent V L)(p : proof (G_n_set V L n) hyp s) ⇒
proof_depth p ≤ d)
(map (add_context (f2 :: sl) sr) ass) opl.
Lemma conj_left_head_Gn_admissible :
∀(n : nat)(hyp : set (sequent V L))(gamma : sequent V L)
(f1 f2 : lambda_formula V L),
conj_head_inversion_closed hyp →
∀(p_and : proof (G_n_set V L n) hyp gamma)
(d : nat)(gamma_tl : sequent V L),
gamma = (lf_and f1 f2) :: gamma_tl →
proof_depth p_and ≤ d →
∃(p : proof (G_n_set V L n) hyp (f1 :: gamma_tl)),
proof_depth p ≤ d.
Lemma conj_right_head_Gn_admissible :
∀(n : nat)(hyp : set (sequent V L))(gamma : sequent V L)
(f1 f2 : lambda_formula V L),
conj_head_inversion_closed hyp →
∀(p_and : proof (G_n_set V L n) hyp gamma)
(d : nat)(gamma_tl : sequent V L),
gamma = (lf_and f1 f2) :: gamma_tl →
proof_depth p_and ≤ d →
∃(p : proof (G_n_set V L n) hyp (f2 :: gamma_tl)),
proof_depth p ≤ d.
Lemma neg_and_inv_head_Gn_admissible_ind :
∀(n : nat)(hyp : set (sequent V L))(gamma : sequent V L)
(f1 f2 : lambda_formula V L),
disj_head_inversion_closed hyp →
∀(p_or : proof (G_n_set V L n) hyp gamma)
(d : nat)(gamma_tl : sequent V L),
gamma = (lf_neg (lf_and f1 f2)) :: gamma_tl →
proof_depth p_or ≤ d →
∃(p : proof (G_n_set V L n) hyp
((lf_neg f1) :: (lf_neg f2) :: gamma_tl)),
proof_depth p ≤ d.
Lemma neg_and_inv_head_Gn_depth_admissible :
∀(hyp : set (sequent V L))(n d : nat)
(f1 f2 : lambda_formula V L)(s : sequent V L),
disj_head_inversion_closed hyp →
provable_at_depth (G_n_set V L n) hyp d ((lf_neg (lf_and f1 f2)) :: s) →
provable_at_depth (G_n_set V L n) hyp d
((lf_neg f1) :: (lf_neg f2) :: s).
Lemma neg_and_inv_head_G_n_hyp_admissible :
∀(hyp : set (sequent V L))(n : nat)
(f1 f2 : lambda_formula V L)(s : sequent V L),
disj_head_inversion_closed hyp →
provable (G_n_set V L n) hyp ((lf_neg (lf_and f1 f2)) :: s) →
provable (G_n_set V L n) hyp ((lf_neg f1) :: (lf_neg f2) :: s).
Lemma neg_inv_head_Gn_depth_admissible_ind :
∀(n : nat)(hyp : set (sequent V L))(gamma : sequent V L)
(f : lambda_formula V L),
neg_head_inversion_closed hyp →
∀(p_neg : proof (G_n_set V L n) hyp gamma)
(d : nat)(gamma_tl : sequent V L),
gamma = (lf_neg (lf_neg f)) :: gamma_tl →
proof_depth p_neg ≤ d →
∃(p : proof (G_n_set V L n) hyp (f :: gamma_tl)),
proof_depth p ≤ d.
Lemma neg_inv_head_Gn_depth_admissible :
∀(hyp : set (sequent V L))(n d : nat)
(f : lambda_formula V L)(s : sequent V L),
neg_head_inversion_closed hyp →
provable_at_depth (G_n_set V L n) hyp d ((lf_neg (lf_neg f)) :: s) →
provable_at_depth (G_n_set V L n) hyp d (f :: s).
Lemma neg_inv_head_Gn_hyp_admissible :
∀(hyp : set (sequent V L))(n : nat)
(f : lambda_formula V L)(s : sequent V L),
neg_head_inversion_closed hyp →
provable (G_n_set V L n) hyp ((lf_neg (lf_neg f)) :: s) →
provable (G_n_set V L n) hyp (f :: s).
Lemma inversion_depth_preserving_admissible_Gn_H :
∀(n : nat)(hyp : set (sequent V L)),
sequent_multiset hyp →
head_inversion_closed hyp →
depth_preserving_admissible_rule_set (G_n_set V L n) hyp
(inversion_rules V L).
Lemma inversion_admissible_Gn_H :
∀(n : nat)(hyp : set (sequent V L)),
sequent_multiset hyp →
head_inversion_closed hyp →
admissible_rule_set (G_n_set V L n) hyp (inversion_rules V L).
Towards Inversion Lemma 3.13 for GR_n
Lemma non_modal_weaken_subst_formula :
∀(sigma : lambda_subst V L)(r : sequent_rule V L)
(f : lambda_formula V L)(s delta : sequent V L),
one_step_rule r →
not (top_modal_form f) →
list_reorder (f :: s) (subst_sequent sigma (conclusion r) ++ delta) →
∃(delta_l delta_r : sequent V L),
delta = delta_l ++ f :: delta_r.
Lemma change_sequent_provable_subst_n_conclusion :
∀(rules : set (sequent_rule V L))(n : nat)(npos : 0 < n)
(f : lambda_formula V L)(s1 s2 : sequent V L),
one_step_rule_set rules →
not (top_modal_form f) →
provable_subst_n_conclusions rules n npos (f :: s1) →
rank_sequent n s2 →
provable_subst_n_conclusions rules n npos (s2 ++ s1).
Lemma change_form_provable_subst_n_conclusion :
∀(rules : set (sequent_rule V L))(n : nat)(npos : 0 < n)
(f1 f2 : lambda_formula V L)(s : sequent V L),
one_step_rule_set rules →
not (top_modal_form f1) →
provable_subst_n_conclusions rules n npos (f1 :: s) →
rank_formula n f2 →
provable_subst_n_conclusions rules n npos (f2 :: s).
Lemma provable_subst_n_conclusions_rank_non_modal :
∀(rules : set (sequent_rule V L))(n : nat)(npos : 0 < n)
(f : lambda_formula V L)(s : sequent V L),
one_step_rule_set rules →
not (top_modal_form f) →
provable_subst_n_conclusions rules n npos (f :: s) →
rank_formula n f.
Lemma head_inversion_provable_subst_n_conclusion :
∀(rules : set (sequent_rule V L))(n : nat)(npos : 0 < n),
one_step_rule_set rules →
head_inversion_closed (provable_subst_n_conclusions rules n npos).
Lemma inversion_admissible_GR_n :
∀(nonempty_V : V)(rules : set (sequent_rule V L))(n : nat),
0 < n →
one_step_rule_set rules →
admissible_rule_set
(GR_n_set rules n) (empty_sequent_set V L)
(rank_rules n (inversion_rules V L)).
Theorem inversion_admissible_GR :
∀(nonempty_V : V)(rules : set (sequent_rule V L)),
one_step_rule_set rules →
admissible_rule_set
(GR_set rules) (empty_sequent_set V L)
(inversion_rules V L).
End Inversion.
Implicit Arguments conj_head_inversion_closed [V L].
Implicit Arguments disj_head_inversion_closed [V L].
Implicit Arguments neg_head_inversion_closed [V L].
Implicit Arguments head_inversion_closed [V L].
Implicit Arguments conj_left_head_Gn_admissible [V L].
Implicit Arguments conj_right_head_Gn_admissible [V L].
∀(nonempty_V : V)(rules : set (sequent_rule V L)),
one_step_rule_set rules →
admissible_rule_set
(GR_set rules) (empty_sequent_set V L)
(inversion_rules V L).
End Inversion.
Implicit Arguments conj_head_inversion_closed [V L].
Implicit Arguments disj_head_inversion_closed [V L].
Implicit Arguments neg_head_inversion_closed [V L].
Implicit Arguments head_inversion_closed [V L].
Implicit Arguments conj_left_head_Gn_admissible [V L].
Implicit Arguments conj_right_head_Gn_admissible [V L].