Soundness, 4.7

This module proves the soundness theorem for coalgebraic logics.
I use two definitions of downward correct rules here. The first and weaker one is needed for one-step rules. The second is based on the simplified sequent semantics. It is simpler but also slightly stronger. This second definition is used for the propositional rules and also for contraction.

Require Export classic one_step_conditions.

Section Soundness.

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

Downward validity


  Definition downward_correct_rule(nonempty_v : V)
                    (LS : lambda_structure L T)(r : sequent_rule V L) : Prop :=
    ∀(m : model V T),
      every_nth (valid_all_states nonempty_v LS m) (assumptions r) →
        valid_all_states nonempty_v LS m (conclusion r).

  Definition downward_correct_rule_set(nonempty_v : V)
          (LS : lambda_structure L T)(rules : set (sequent_rule V L)) : Prop :=
    ∀(r : sequent_rule V L),
      rules r → downward_correct_rule nonempty_v LS r.

  Lemma sound_derivation :
    ∀(nonempty_v : V)(LS : lambda_structure L T)
          (rules : set (sequent_rule V L))(hypotheses : set (sequent V L))
          (m : model V T)(s : sequent V L),
      downward_correct_rule_set nonempty_v LS rules →
      (∀(h : sequent V L),
         hypotheses h → valid_all_states nonempty_v LS m h) →
      proof rules hypotheses s →
        valid_all_states nonempty_v LS m s.

Stronger downward validity


  Definition strong_downward_correct_rule(LS : lambda_structure L T)
                                              (r : sequent_rule V L) : Prop :=
    ∀(m : model V T)(x : state m),
      every_nth (state_seq_semantics LS m x) (assumptions r) →
        state_seq_semantics LS m x (conclusion r).

  Definition downward_correct_rule_strengthen :
    ∀(nonempty_v : V)(LS : lambda_structure L T)(r : sequent_rule V L),
      strong_downward_correct_rule LS r →
        downward_correct_rule nonempty_v LS r.

  Lemma assumption_add_context_state_seq_semantics :
    ∀(LS : lambda_structure L T)(m : model V T)(x : state m)
          (sl sr : sequent V L)(sml : list (sequent V L)),
      sml ≠ [] →
      every_nth (state_seq_semantics LS m x)
                (map (add_context sl sr) sml) →
        ¬ ( ¬ (state_seq_semantics LS m x sl) ∧
            ¬ (state_seq_semantics LS m x sr) ∧
            ¬ (every_nth (state_seq_semantics LS m x) sml)).

  Lemma strong_downward_correct_context :
    ∀(LS : lambda_structure L T)
          (r : sequent_rule V L)(sl sr : sequent V L),
      conclusion r ≠ [] →
      strong_downward_correct_rule LS r →
        strong_downward_correct_rule LS (rule_add_context sl sr r).

Strong downward correctness of G


  Lemma strong_downward_correct_ax :
    ∀(LS : lambda_structure L T)(r : sequent_rule V L),
      is_ax_rule r →
        strong_downward_correct_rule LS r.

  Lemma strong_downward_correct_and :
    ∀(LS : lambda_structure L T)(r : sequent_rule V L),
      is_and_rule r → strong_downward_correct_rule LS r.

  Lemma strong_downward_correct_neg_and :
    ∀(LS : lambda_structure L T)(r : sequent_rule V L),
      is_neg_and_rule r → strong_downward_correct_rule LS r.

  Lemma strong_downward_correct_neg_neg :
    ∀(LS : lambda_structure L T)(r : sequent_rule V L),
      is_neg_neg_rule r → strong_downward_correct_rule LS r.

Downward correctness other rules

The cut rule is not sound in intuitionistic logic, because it permits to derive B from A and ~A, B , which amounts to A /\ ~(~~A /\ ~B) -> B from which one can derive classical logic, see classic_axiom_sound_cut_left in module classic.
  Lemma strong_downward_correct_cut :
    ∀(LS : lambda_structure L T)(r : sequent_rule V L),
      classical_logic →
      is_cut_rule r →
        strong_downward_correct_rule LS r.

  Lemma downward_correct_one_step_rule :
    ∀(nonempty_v : V)(LS : lambda_structure L T)
          (rules : set (sequent_rule V L))(osr : one_step_rule_set rules)
          (r : sequent_rule V L),
      one_step_sound nonempty_v LS rules osr →
      weaken_subst_rule rules r →
        downward_correct_rule nonempty_v LS r.

The contraction rule is not part of the soundness theorem, but its soundness is needed for the semantics admissibility proof in Theorem 4.15.
Contraction is not sound in intuitionistic logic, because, with empty Gamma, it amounts to ~(~A /\ ~A) -> A, which implies classical logic, see classic_axiom_sound_contraction in module classic.
  Lemma downward_correct_contraction :
    ∀(nonempty_v : V)(LS : lambda_structure L T)(r : sequent_rule V L),
      classical_logic →
      is_contraction_rule r →
        downward_correct_rule nonempty_v LS r.

Towards soundness, theorem 4.7


  Lemma downward_correct_GR :
    ∀(nonempty_v : V)(LS : lambda_structure L T)
          (rules : set (sequent_rule V L))(osr : one_step_rule_set rules),
      one_step_sound nonempty_v LS rules osr →
        downward_correct_rule_set nonempty_v LS (GR_set rules).

  Lemma downward_correct_GRC :
    ∀(nonempty_v : V)(LS : lambda_structure L T)
          (rules : set (sequent_rule V L))(osr : one_step_rule_set rules),
      classical_logic →
      one_step_sound nonempty_v LS rules osr →
        downward_correct_rule_set nonempty_v LS (GRC_set rules).

Soundness theorem 4.7, GRC part

Soundness for GRC is only provable in classical logic because of the cut rule.
  Theorem sound_GRC :
    ∀(nonempty_v : V)(LS : lambda_structure L T)
          (rules : set (sequent_rule V L))(osr : one_step_rule_set rules)
          (s : sequent V L),
      classical_logic →
      one_step_sound nonempty_v LS rules osr →
      provable (GRC_set rules) (empty_sequent_set V L) s →
        valid_all_models nonempty_v LS s.

soundness theorem 4.7, GR part

Soundness of GR can be proven in intuitionistic logic.
  Theorem sound_GR :
    ∀(nonempty_v : V)(LS : lambda_structure L T)
          (rules : set (sequent_rule V L))(osr : one_step_rule_set rules)
          (s : sequent V L),
      one_step_sound nonempty_v LS rules osr →
      provable (GR_set rules) (empty_sequent_set V L) s →
        valid_all_models nonempty_v LS s.

End Soundness.

Implicit Arguments downward_correct_rule_set [V L T].
Implicit Arguments downward_correct_rule_strengthen [V L T].
Implicit Arguments strong_downward_correct_cut [V L T].
Implicit Arguments sound_GR [V L T].