Soundness, 4.7
Require Export classic one_step_conditions.
Section Soundness.
Variable V : Type.
Variable L : modal_operators.
Variable T : functor.
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.
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).
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
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.
∀(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.
∀(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.
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
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.
∀(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.
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].
∀(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].