K example, Soundness, Completeness, 4.6, page 18

This module proves one-step soundness and one-step completeness for K and derives then soundness, completeness, cut-elimination and contraction for K by using the generic theorems.
Note that all assumptions from the generic theorems are discharched here (besides classical_logic, of course).

Require Export k_semantics complete.

Section K_sound.

  Hypothesis pred_ext : ∀(A : Type)(P Q : A → Prop),
   (∀(a : A), P a ↔ Q a) → P = Q.

One-step soundness


  Lemma k_rules_one_step_sound :
    classical_logic →
      one_step_sound 0 (k_lambda pred_ext) k_rules one_step_rule_set_k_rules.

Derive soundness


  Theorem sound_k_GRC : ∀(s : sequent KV KL),
    classical_logic →
    provable (GRC_set k_rules) (empty_sequent_set KV KL) s →
      valid_all_models 0 (k_lambda pred_ext) s.

  Theorem sound_k_GR : ∀(s : sequent KV KL),
    classical_logic →
    provable (GR_set k_rules) (empty_sequent_set KV KL) s →
      valid_all_models 0 (k_lambda pred_ext) s.

One-step completeness


  Lemma k_rules_one_step_cut_free_complete :
    classical_logic →
      one_step_cut_free_complete 0 (k_lambda pred_ext) k_rules
                                 one_step_rule_set_k_rules.

Derive completeness, cut-elimination and contraction


  Theorem k_complete : ∀(s : sequent KV KL),
    classical_logic →
    valid_all_models 0 (k_lambda pred_ext) s →
      provable (GR_set k_rules) (empty_sequent_set KV KL) s.

  Theorem k_semantic_cut :
    classical_logic →
      admissible_rule_set (GR_set k_rules) (empty_sequent_set KV KL)
                          is_cut_rule.

  Theorem k_semantic_contraction :
    classical_logic →
      admissible_rule_set (GR_set k_rules) (empty_sequent_set KV KL)
                          is_contraction_rule.

End K_sound.