Soundness for propositional logic
Require Export propositional_models.
Section Propositional_soundness.
Variable V : Type.
Variable L : modal_operators.
Abbreviation for propositional G proofs
Definition prop_downward_correct_rule(r : sequent_rule V L)
(prop_r : propositional_rule r) : Prop :=
∀(m : prop_model V),
(∀(n : nat)(n_len : n < length (assumptions r)),
prop_sequent_interpretation m (nth (assumptions r) n n_len)
(prop_sequent_rule_ass_tcc r n n_len prop_r)) →
prop_sequent_interpretation m (conclusion r)
(prop_sequent_rule_concl_tcc r prop_r).
Lemma prop_downward_correct_rule_tcc_irr :
∀(r : sequent_rule V L)(prop_r1 prop_r2 : propositional_rule r),
prop_downward_correct_rule r prop_r1 →
prop_downward_correct_rule r prop_r2.
Definition prop_downward_correct_rule_set(rules : sequent_rule V L → Prop)
(prop_rules : propositional_rule_set rules) : Prop :=
∀(r : sequent_rule V L)(r_rule : rules r),
prop_downward_correct_rule r (prop_rules r r_rule).
Lemma propositional_correct_derivation :
∀(m : prop_model V)
(rules : sequent_rule V L → Prop)
(prop_rules : propositional_rule_set rules)
(hypotheses : sequent V L → Prop)
(prop_hyp : propositional_sequent_set hypotheses)
(l : sequent V L)(prop_l : propositional_sequent l),
prop_downward_correct_rule_set rules prop_rules →
(∀(h : sequent V L)(in_hyp : hypotheses h),
prop_sequent_interpretation m h (prop_hyp h in_hyp)) →
proof rules hypotheses l →
prop_sequent_interpretation m l prop_l.
Lemma assumption_add_context_interpretation :
∀(m : prop_model V)(sl sr : sequent V L)
(prop_sl : propositional_sequent sl)
(prop_sr : propositional_sequent sr)
(sml : list (sequent V L))
(prop_sml : every_nth propositional_sequent sml)
(prop_sml_context :
every_nth propositional_sequent (map (add_context sl sr) sml)),
sml ≠ [] →
(∀(n : nat)(n_len : n < length (map (add_context sl sr) sml)),
prop_sequent_interpretation m
(nth (map (add_context sl sr) sml) n n_len)
(prop_sml_context n n_len))
→
~(~(prop_sequent_interpretation m sl prop_sl) ∧
~(prop_sequent_interpretation m sr prop_sr) ∧
~(∀(n : nat)(n_less : n < length sml),
prop_sequent_interpretation m
(nth sml n n_less) (prop_sml n n_less))).
Lemma prop_downward_correct_context :
∀(r : sequent_rule V L)(sl sr : sequent V L)
(prop_sl_r_sr : propositional_rule (rule_add_context sl sr r)),
conclusion r ≠ [] →
prop_downward_correct_rule r
(propositional_rule_add_context_bare_rule r sl sr prop_sl_r_sr)
→
prop_downward_correct_rule (rule_add_context sl sr r) prop_sl_r_sr.
Lemma prop_downward_correct_ax :
∀(r : sequent_rule V L)(prop_r : propositional_rule r),
is_ax_rule r →
prop_downward_correct_rule r prop_r.
Lemma prop_downward_correct_and :
∀(r : sequent_rule V L)(prop_r : propositional_rule r),
is_and_rule r → prop_downward_correct_rule r prop_r.
Lemma prop_downward_correct_neg_and :
∀(r : sequent_rule V L)(prop_r : propositional_rule r),
is_neg_and_rule r → prop_downward_correct_rule r prop_r.
Lemma prop_downward_correct_neg_neg :
∀(r : sequent_rule V L)(prop_r : propositional_rule r),
is_neg_neg_rule r → prop_downward_correct_rule r prop_r.
Lemma prop_downward_correct_prop_G :
prop_downward_correct_rule_set (prop_G_set V L) propositional_prop_G_set.
Lemma propositional_correct_G_derivation :
∀(m : prop_model V)
(l : sequent V L)(prop_l : propositional_sequent l),
prop_proof_type l →
prop_sequent_interpretation m l prop_l.
Lemma propositional_sound_G :
∀(nonempty_v : V)(s : sequent V L)(prop_s : propositional_sequent s),
provable (prop_G_set V L) (empty_sequent_set V L) s →
prop_valid_sequent nonempty_v s prop_s.
End Propositional_soundness.
Implicit Arguments prop_proof_type [[V] [L]].
Implicit Arguments propositional_sound_G [V L].