K example, Soundness, Completeness, 4.6, page 18
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.
Lemma k_rules_one_step_sound :
classical_logic →
one_step_sound 0 (k_lambda pred_ext) k_rules one_step_rule_set_k_rules.
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.
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.
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.