Soundness for propositional logic

This module proves the soundness part of 3.2.1. This result is also needed as induction base case for the soundness of coalgebraic logics.

Require Export propositional_models.

Section Propositional_soundness.

  Variable V : Type.
  Variable L : modal_operators.

Abbreviation for propositional G proofs
  Definition prop_proof_type : sequent V LType :=
    proof (prop_G_set V L) (empty_sequent_set V L).

Downward correct rules

  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 LProp)
                          (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 LProp)
          (prop_rules : propositional_rule_set rules)
          (hypotheses : sequent V LProp)
          (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.

Downward correctness of context rules

  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.

Downward correctness of G


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