Results on propositional logic
High-level misc results
- Derive general cut elimination from cut elimination at head position. This is needed in the propositional cut-elimination proof.
- Prove cut elimination in the weakening contest of a one-step
rule. This is needed in module
mixed_cut and moduleosr_cut . - Construct a proof for finite disjunction.
- Sequent axiom
Lemma cut_admissibile_from_head_elim :
∀(rules : set (sequent_rule V L))(n : nat),
rule_multiset rules →
(∀(f : lambda_formula V L)(q r : sequent V L),
provable (rank_rules n rules) (empty_sequent_set V L)
(f :: q) →
provable (rank_rules n rules) (empty_sequent_set V L)
((lf_neg f) :: r) →
provable (rank_rules n rules) (empty_sequent_set V L) (q ++ r))
→
admissible_rule_set (rank_rules n rules) (empty_sequent_set V L)
(bounded_cut_rules V L n).
Lemma provable_GRC_n_GR_n_from_head_elim :
∀(rules : set (sequent_rule V L))(n : nat)(s : sequent V L),
one_step_rule_set rules →
(∀(f : lambda_formula V L)(q r : sequent V L),
provable (GR_n_set rules n) (empty_sequent_set V L)
(f :: q) →
provable (GR_n_set rules n) (empty_sequent_set V L)
((lf_neg f) :: r) →
provable (GR_n_set rules n) (empty_sequent_set V L) (q ++ r)) →
provable (GRC_n_set rules n) (empty_sequent_set V L) s →
provable (GR_n_set rules n) (empty_sequent_set V L) s.
Cut elimination in the context of one-step rules
Lemma cut_elimination_osr_context :
∀(rules : set (sequent_rule V L))(n : nat)(ssn_pos : 0 < 2 + n)
(f : lambda_formula V L)(q r : sequent V L)
(rb : sequent_rule V L)(sigma : lambda_subst V L)
(delta delta_tl : sequent V L),
one_step_rule_set rules →
rules rb →
rank_subst (S n) sigma →
rank_sequent (2 + n) delta →
list_reorder (f :: q)
((subst_sequent sigma (conclusion rb)) ++ delta) →
list_reorder (f :: delta_tl) delta →
every_nth
(provable (GR_n_set rules (S n)) (empty_sequent_set V L))
(map (subst_sequent sigma) (assumptions rb)) →
rank_sequent (2 + n) r →
provable_subst_n_conclusions rules (2 + n) ssn_pos (q ++ r).
∀(rules : set (sequent_rule V L))(n : nat)(ssn_pos : 0 < 2 + n)
(f : lambda_formula V L)(q r : sequent V L)
(rb : sequent_rule V L)(sigma : lambda_subst V L)
(delta delta_tl : sequent V L),
one_step_rule_set rules →
rules rb →
rank_subst (S n) sigma →
rank_sequent (2 + n) delta →
list_reorder (f :: q)
((subst_sequent sigma (conclusion rb)) ++ delta) →
list_reorder (f :: delta_tl) delta →
every_nth
(provable (GR_n_set rules (S n)) (empty_sequent_set V L))
(map (subst_sequent sigma) (assumptions rb)) →
rank_sequent (2 + n) r →
provable_subst_n_conclusions rules (2 + n) ssn_pos (q ++ r).
Lemma provable_or_formula_of_ne_sequent :
∀(rules : set (sequent_rule V L))(hyp : set (sequent V L))
(n : nat)(s : sequent V L)(nonempty_s : s ≠ []),
rank_sequent_set n hyp →
subset (G_n_set V L n) (rank_rules n rules) →
provable (rank_rules n rules) hyp s →
provable (rank_rules n rules) hyp
[or_formula_of_ne_sequent s nonempty_s].
Lemma provable_sequent_axiom_ind :
∀(rules : set (sequent_rule V L))(hyp : set (sequent V L))
(f : lambda_formula V L)(s1 s2 : sequent V L)(n : nat),
rule_multiset rules →
sequent_multiset hyp →
subset (G_n_set V L n) (rank_rules n rules) →
rank_formula n f →
rank_sequent n (rev s1) →
rank_sequent n s2 →
incl (f :: s1) s2 →
(∀(f : lambda_formula V L)(s : sequent V L),
rank_formula n f →
rank_sequent n s →
provable (rank_rules n rules) hyp (f :: lf_neg f :: s))
→
provable (rank_rules n rules) hyp
((lf_neg (or_formula_of_sequent_iter f (rev s1))) :: s2).
Lemma provable_sequent_axiom :
∀(rules : set (sequent_rule V L))(hyp : set (sequent V L))
(s1 s2 : sequent V L)(nonempty_s1 : s1 ≠ [])(n : nat),
rule_multiset rules →
sequent_multiset hyp →
subset (G_n_set V L n) (rank_rules n rules) →
rank_sequent n s1 →
rank_sequent n s2 →
incl s1 s2 →
(∀(f : lambda_formula V L)(s : sequent V L),
rank_formula n f →
rank_sequent n s →
provable (rank_rules n rules) hyp (f :: lf_neg f :: s))
→
provable (rank_rules n rules) hyp
((lf_neg (or_formula_of_ne_sequent s1 nonempty_s1)) :: s2).
End Generic_cut.