Results on propositional logic

High-level misc results

The name of this module is a bad choice. This module contains some utility results that need to go into a separate file because of module dependencies. There is:

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 module osr_cut.
Construct a proof for finite disjunction.
Sequent axiom

Require Export weakening.

Section Generic_cut.

Variable V : Type.
Variable L : modal_operators.

Cut elimination relative to cut elimination at head position

  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

The following is case a) 1 and b) 1 in 5.6.3 cut elimination: The cut formula is in the weakening context of a one-step rule, so one can easily add the other rule into the context.

  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).

Proof finite disjunction

  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 ].

Proof ~(\/ G), G

  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.