Completeness and semantic cut admissibility, 4.13 - 4.15


Require Export prop_mod weakening cut_properties
               propositional_completeness sound step_semantics
               backward_substitution.

Section Completeness.

  Variable V : Type.
  Variable L : modal_operators.
  Variable T : functor.

Need a decidable equality on propositional constants for the proof construction.
  Variable v_eq : eq_type V.

Towards rank-n completeness, Prop 4.13

rank-n completeness for top_mod sequents

This is the heart of the proof of 4.13

  Definition subst_osr_conclusions_with_ax(nonempty_v : V)
               (LS : lambda_structure L T)(rules : set (sequent_rule V L))
               (osr : one_step_rule_set rules)(tau : lambda_subst V L)
               (n : nat)(rank_tau : rank_subst (S n) tau)
                                                      : set (sequent V L) :=
    union (subst_Ax_n_set tau (2 + n))
          (subst_sequent_set tau
             (valid_subst_n_conclusions nonempty_v rules osr
                (n_step_subst_coval LS tau n rank_tau))).

Part with cut
  Lemma top_mod_n_completeness :
    ∀(enum_V : enumerator V)(LS : lambda_structure L T)
          (rules : set (sequent_rule V L))
          (osr : one_step_rule_set rules)
          (n : nat)(s : sequent V L)(rank : rank_sequent (2 + n) s),
      non_trivial_functor T →
      one_step_complete (enum_elem enum_V) LS rules osr →
      (∀(s : sequent V L)(rank : rank_sequent (S n) s),
        step_semantics_valid (enum_elem enum_V) LS s n rank →
          provable (GRC_n_set rules (S n)) (empty_sequent_set V L) s) →
      top_modal_sequent s →
      step_semantics_valid (enum_elem enum_V) LS s (S n) rank →
        provable (GRC_n_set rules (2 + n)) (empty_sequent_set V L) s .

Part without cut
  Lemma top_mod_n_cut_free_completeness :
    ∀(enum_V : enumerator V)(LS : lambda_structure L T)
          (rules : set (sequent_rule V L))
          (osr : one_step_rule_set rules)
          (n : nat)(s weak_cont : sequent V L)
          (rank_s : rank_sequent (2 + n) s),
      non_trivial_functor T →
      one_step_cut_free_complete (enum_elem enum_V) LS rules osr →
      (∀(s : sequent V L)(rank : rank_sequent (S n) s),
        step_semantics_valid (enum_elem enum_V) LS s n rank →
          provable (GR_n_set rules (S n)) (empty_sequent_set V L) s) →
      top_modal_sequent s →
      step_semantics_valid (enum_elem enum_V) LS s (S n) rank_s →
      rank_sequent (2 + n) weak_cont →
        provable (GR_n_set rules (2 + n)) (empty_sequent_set V L)
                 (s ++ weak_cont).

Build proof up to non-decomposable formulas

The following instantiates the generic build_proof to do a propositional proof search. This is used to decompose the sequent into sequents of non-decomposable formulas. (The statement about the inversion lemma in the paper is nonsense.) These non-decomposable formulas appear as hypothesis in the proof search, such that build_proof is guaranteed to succeed.
Hypothesis for the proof search.
  Definition simple_4_13_sequent : set (sequent V L) :=
    intersection (prop_or_mod_sequent V L)
                 (set_inverse simple_tautology).

  Definition mod_prop_hyp_oracle :
                       hypotheses_oracle_type V L simple_4_13_sequent :=
    fun(s : sequent V L) ⇒
      match find_trivial v_eq s s 0 as ft
        return find_trivial v_eq s s 0 = ft → option (simple_4_13_sequent s)
      with
        | None ⇒ fun(ftn : find_trivial v_eq s s 0 = None) ⇒
          match dprop_or_mod_sequent s as res
            return dprop_or_mod_sequent s = res
                         → option (simple_4_13_sequent s)
          with
            | true ⇒ fun(p : dprop_or_mod_sequent s = true) ⇒
              Some (conj (iff_left (prop_or_mod_sequent_prop _) p)
                         (find_trivial_none v_eq _ ftn))
            | false ⇒ fun _ ⇒ None
          end (eq_refl (dprop_or_mod_sequent s))
        | Some _ ⇒ fun _ ⇒ None
      end (eq_refl (find_trivial v_eq s s 0)).

  Definition prop_Gn_oracle(n : nat) :
                              rule_oracle_type V L (G_n_set V L n) :=
    fun(s : sequent V L) ⇒
    match prop_G_oracle v_eq s with
      | None ⇒ None
      | Some (dep_conj r (conj in_rules concl_prop)) ⇒
        let comp_res := Compare_dec.leb (minimal_rule_rank r) n in
        match comp_res as cr
          return comp_res = cr
                    → rule_oracle_result V L (G_n_set V L n) s
        with
          | true ⇒ fun(H : comp_res = true) ⇒
            Some(dep_conj _ _ r
                   (conj
                      (rank_rules_minimal_rule_rank (G_set V L) r n
                          in_rules (leb_complete _ _ H))
                      concl_prop))
          | false ⇒ fun _ ⇒ None
        end (eq_refl comp_res)
    end.

  Lemma well_founded_Gn_oracle : ∀(n : nat),
    well_founded_rule_oracle (prop_Gn_oracle n) sequent_measure.

build_proof instantiation with a type that permits failure.
  Definition prop_mod_build_proof_maybe(n : nat)(s : sequent V L) :
              (proof (G_n_set V L n) simple_4_13_sequent s) + (sequent V L) :=
    build_proof (S (sequent_measure s))
      mod_prop_hyp_oracle (prop_Gn_oracle n) s.

Proof that the proof search will always succeed.
  Lemma prop_mod_build_proof_left : ∀(n : nat)(s : sequent V L),
    rank_sequent n s →
      is_inl (prop_mod_build_proof_maybe n s).

Valid subset of the hypotheses
  Definition valid_simple_4_13_sequent(nonempty_v : V)
                   (LS : lambda_structure L T)(n : nat) : set (sequent V L) :=
    intersection simple_4_13_sequent
                 (step_semantics_valid_at_rank nonempty_v LS n).

  Lemma valid_simple_4_13_sequent_list_reorder :
    ∀(nonempty_v : V)(LS : lambda_structure L T)(n : nat)
          (s1 s2 : sequent V L),
      list_reorder s1 s2 →
      valid_simple_4_13_sequent nonempty_v LS n s1 →
        valid_simple_4_13_sequent nonempty_v LS n s2.

Restrict the proof building in two ways: First, guarantee success by type, second restrict hypotheses to valid sequents.
  Definition prop_mod_build_proof(classic : classical_logic)(nonempty_v : V)
             (LS : lambda_structure L T)
             (n : nat)(s : sequent V L)(rank : rank_sequent (S n) s)
             (valid : step_semantics_valid nonempty_v LS s n rank)
                    : proof (G_n_set V L (S n))
                            (valid_simple_4_13_sequent nonempty_v LS n) s :=
    match prop_mod_build_proof_maybe (S n) s
      as pmaybe
      return is_inl pmaybe →
                 proof (G_n_set V L (S n))
                       (valid_simple_4_13_sequent nonempty_v LS n) s
    with
      | inl p ⇒ fun _ ⇒
        restrict_hypothesis (step_semantics_valid_at_rank nonempty_v LS n)
          (step_semantics_valid_G_rule_inductive nonempty_v LS n classic)
          s
          (dep_conj (rank_sequent (S n) s)
                    (step_semantics_valid nonempty_v LS s n)
             rank valid)
          p
      | inr _ ⇒ fun(H : False) ⇒ False_rect _ H
    end (prop_mod_build_proof_left (S n) s rank).

Split propositional part and retain a valid modal sequent


  Lemma split_prop_mod :
    ∀(nonempty_v : V)(LS : lambda_structure L T)
          (prop_s mod_s : sequent V L)
          (n : nat)(rank : rank_sequent (2 + n) (mod_s ++ prop_s)),
      classical_logic →
      non_trivial_functor T →
      prop_sequent prop_s →
      top_modal_sequent mod_s →
      ¬ (simple_tautology prop_s) →
      step_semantics_valid nonempty_v LS (mod_s ++ prop_s) (S n) rank →
        step_semantics_valid nonempty_v LS mod_s (S n)
          (rank_sequent_append_left _ _ _ rank).

Rank-n completeness, Prop 4.13

4.13, part with cut
  Lemma n_completeness :
    ∀(enum_V : enumerator V)(LS : lambda_structure L T)
          (rules : set (sequent_rule V L))
          (osr : one_step_rule_set rules)
          (n : nat)(s : sequent V L)(rank : rank_sequent (S n) s),
      classical_logic →
      non_trivial_functor T →
      one_step_complete (enum_elem enum_V) LS rules osr →
      step_semantics_valid (enum_elem enum_V) LS s n rank →
        provable (GRC_n_set rules (S n)) (empty_sequent_set V L) s.

4.13, cut-free part
  Lemma n_cut_free_completeness :
    ∀(enum_V : enumerator V)(LS : lambda_structure L T)
          (rules : set (sequent_rule V L))
          (osr : one_step_rule_set rules)
          (n : nat)(s : sequent V L)(rank : rank_sequent (S n) s),
      classical_logic →
      non_trivial_functor T →
      one_step_cut_free_complete (enum_elem enum_V) LS rules osr →
      step_semantics_valid (enum_elem enum_V) LS s n rank →
        provable (GR_n_set rules (S n)) (empty_sequent_set V L) s.

Completeness, Corollary 4.14

4.14, part with cut
  Lemma completeness :
    ∀(enum_V : enumerator V)(LS : lambda_structure L T)
          (rules : set (sequent_rule V L))
          (osr : one_step_rule_set rules)
          (s : sequent V L),
      classical_logic →
      non_trivial_functor T →
      one_step_complete (enum_elem enum_V) LS rules osr →
      valid_all_models (enum_elem enum_V) LS s →
        provable (GRC_set rules) (empty_sequent_set V L) s.

4.14, cut-free part
  Lemma cut_free_completeness :
    ∀(enum_V : enumerator V)(LS : lambda_structure L T)
          (rules : set (sequent_rule V L))
          (osr : one_step_rule_set rules)
          (s : sequent V L),
      classical_logic →
      non_trivial_functor T →
      one_step_cut_free_complete (enum_elem enum_V) LS rules osr →
      valid_all_models (enum_elem enum_V) LS s →
        provable (GR_set rules) (empty_sequent_set V L) s.

Towards admissibility of cut and contraction, 4.15

This is the semantic cut-elimination theorem

  Lemma semantic_admissible_rules :
    ∀(enum_V : enumerator V)(LS : lambda_structure L T)
          (osr rules : set (sequent_rule V L))
          (osr_prop : one_step_rule_set osr),
      classical_logic →
      non_trivial_functor T →
      one_step_sound (enum_elem enum_V) LS osr osr_prop →
      one_step_cut_free_complete (enum_elem enum_V) LS osr osr_prop →
      downward_correct_rule_set (enum_elem enum_V) LS rules →
        admissible_rule_set (GR_set osr) (empty_sequent_set V L) rules.

4.15, cut part

  Theorem semantic_admissible_cut :
    ∀(enum_V : enumerator V)(LS : lambda_structure L T)
          (rules : set (sequent_rule V L))
          (osr_prop : one_step_rule_set rules),
      classical_logic →
      non_trivial_functor T →
      one_step_sound (enum_elem enum_V) LS rules osr_prop →
      one_step_cut_free_complete (enum_elem enum_V) LS rules osr_prop →
        admissible_rule_set (GR_set rules) (empty_sequent_set V L)
          is_cut_rule.

4.15, contraction part

  Theorem semantic_admissible_contraction :
    ∀(enum_V : enumerator V)(LS : lambda_structure L T)
          (osr : set (sequent_rule V L))
          (osr_prop : one_step_rule_set osr),
      classical_logic →
      non_trivial_functor T →
      one_step_sound (enum_elem enum_V) LS osr osr_prop →
      one_step_cut_free_complete (enum_elem enum_V) LS osr osr_prop →
        admissible_rule_set (GR_set osr) (empty_sequent_set V L)
          is_contraction_rule.

End Completeness.