Require Export prop_mod weakening cut_properties
propositional_completeness sound step_semantics
backward_substitution.
Section Completeness.
Variable V : Type.
Variable L : modal_operators.
Variable T : functor.
Need a decidable equality on propositional constants for
the proof construction.
Towards rank-n completeness, Prop 4.13
rank-n completeness for top_mod sequents
This is the heart of the proof of 4.13Definition subst_osr_conclusions_with_ax(nonempty_v : V)
(LS : lambda_structure L T)(rules : set (sequent_rule V L))
(osr : one_step_rule_set rules)(tau : lambda_subst V L)
(n : nat)(rank_tau : rank_subst (S n) tau)
: set (sequent V L) :=
union (subst_Ax_n_set tau (2 + n))
(subst_sequent_set tau
(valid_subst_n_conclusions nonempty_v rules osr
(n_step_subst_coval LS tau n rank_tau))).
Part with cut
Lemma top_mod_n_completeness :
∀(enum_V : enumerator V)(LS : lambda_structure L T)
(rules : set (sequent_rule V L))
(osr : one_step_rule_set rules)
(n : nat)(s : sequent V L)(rank : rank_sequent (2 + n) s),
non_trivial_functor T →
one_step_complete (enum_elem enum_V) LS rules osr →
(∀(s : sequent V L)(rank : rank_sequent (S n) s),
step_semantics_valid (enum_elem enum_V) LS s n rank →
provable (GRC_n_set rules (S n)) (empty_sequent_set V L) s) →
top_modal_sequent s →
step_semantics_valid (enum_elem enum_V) LS s (S n) rank →
provable (GRC_n_set rules (2 + n)) (empty_sequent_set V L) s .
∀(enum_V : enumerator V)(LS : lambda_structure L T)
(rules : set (sequent_rule V L))
(osr : one_step_rule_set rules)
(n : nat)(s : sequent V L)(rank : rank_sequent (2 + n) s),
non_trivial_functor T →
one_step_complete (enum_elem enum_V) LS rules osr →
(∀(s : sequent V L)(rank : rank_sequent (S n) s),
step_semantics_valid (enum_elem enum_V) LS s n rank →
provable (GRC_n_set rules (S n)) (empty_sequent_set V L) s) →
top_modal_sequent s →
step_semantics_valid (enum_elem enum_V) LS s (S n) rank →
provable (GRC_n_set rules (2 + n)) (empty_sequent_set V L) s .
Part without cut
Lemma top_mod_n_cut_free_completeness :
∀(enum_V : enumerator V)(LS : lambda_structure L T)
(rules : set (sequent_rule V L))
(osr : one_step_rule_set rules)
(n : nat)(s weak_cont : sequent V L)
(rank_s : rank_sequent (2 + n) s),
non_trivial_functor T →
one_step_cut_free_complete (enum_elem enum_V) LS rules osr →
(∀(s : sequent V L)(rank : rank_sequent (S n) s),
step_semantics_valid (enum_elem enum_V) LS s n rank →
provable (GR_n_set rules (S n)) (empty_sequent_set V L) s) →
top_modal_sequent s →
step_semantics_valid (enum_elem enum_V) LS s (S n) rank_s →
rank_sequent (2 + n) weak_cont →
provable (GR_n_set rules (2 + n)) (empty_sequent_set V L)
(s ++ weak_cont).
∀(enum_V : enumerator V)(LS : lambda_structure L T)
(rules : set (sequent_rule V L))
(osr : one_step_rule_set rules)
(n : nat)(s weak_cont : sequent V L)
(rank_s : rank_sequent (2 + n) s),
non_trivial_functor T →
one_step_cut_free_complete (enum_elem enum_V) LS rules osr →
(∀(s : sequent V L)(rank : rank_sequent (S n) s),
step_semantics_valid (enum_elem enum_V) LS s n rank →
provable (GR_n_set rules (S n)) (empty_sequent_set V L) s) →
top_modal_sequent s →
step_semantics_valid (enum_elem enum_V) LS s (S n) rank_s →
rank_sequent (2 + n) weak_cont →
provable (GR_n_set rules (2 + n)) (empty_sequent_set V L)
(s ++ weak_cont).
Build proof up to non-decomposable formulas
Definition simple_4_13_sequent : set (sequent V L) :=
intersection (prop_or_mod_sequent V L)
(set_inverse simple_tautology).
Definition mod_prop_hyp_oracle :
hypotheses_oracle_type V L simple_4_13_sequent :=
fun(s : sequent V L) ⇒
match find_trivial v_eq s s 0 as ft
return find_trivial v_eq s s 0 = ft → option (simple_4_13_sequent s)
with
| None ⇒ fun(ftn : find_trivial v_eq s s 0 = None) ⇒
match dprop_or_mod_sequent s as res
return dprop_or_mod_sequent s = res
→ option (simple_4_13_sequent s)
with
| true ⇒ fun(p : dprop_or_mod_sequent s = true) ⇒
Some (conj (iff_left (prop_or_mod_sequent_prop _) p)
(find_trivial_none v_eq _ ftn))
| false ⇒ fun _ ⇒ None
end (eq_refl (dprop_or_mod_sequent s))
| Some _ ⇒ fun _ ⇒ None
end (eq_refl (find_trivial v_eq s s 0)).
Definition prop_Gn_oracle(n : nat) :
rule_oracle_type V L (G_n_set V L n) :=
fun(s : sequent V L) ⇒
match prop_G_oracle v_eq s with
| None ⇒ None
| Some (dep_conj r (conj in_rules concl_prop)) ⇒
let comp_res := Compare_dec.leb (minimal_rule_rank r) n in
match comp_res as cr
return comp_res = cr
→ rule_oracle_result V L (G_n_set V L n) s
with
| true ⇒ fun(H : comp_res = true) ⇒
Some(dep_conj _ _ r
(conj
(rank_rules_minimal_rule_rank (G_set V L) r n
in_rules (leb_complete _ _ H))
concl_prop))
| false ⇒ fun _ ⇒ None
end (eq_refl comp_res)
end.
Lemma well_founded_Gn_oracle : ∀(n : nat),
well_founded_rule_oracle (prop_Gn_oracle n) sequent_measure.
intersection (prop_or_mod_sequent V L)
(set_inverse simple_tautology).
Definition mod_prop_hyp_oracle :
hypotheses_oracle_type V L simple_4_13_sequent :=
fun(s : sequent V L) ⇒
match find_trivial v_eq s s 0 as ft
return find_trivial v_eq s s 0 = ft → option (simple_4_13_sequent s)
with
| None ⇒ fun(ftn : find_trivial v_eq s s 0 = None) ⇒
match dprop_or_mod_sequent s as res
return dprop_or_mod_sequent s = res
→ option (simple_4_13_sequent s)
with
| true ⇒ fun(p : dprop_or_mod_sequent s = true) ⇒
Some (conj (iff_left (prop_or_mod_sequent_prop _) p)
(find_trivial_none v_eq _ ftn))
| false ⇒ fun _ ⇒ None
end (eq_refl (dprop_or_mod_sequent s))
| Some _ ⇒ fun _ ⇒ None
end (eq_refl (find_trivial v_eq s s 0)).
Definition prop_Gn_oracle(n : nat) :
rule_oracle_type V L (G_n_set V L n) :=
fun(s : sequent V L) ⇒
match prop_G_oracle v_eq s with
| None ⇒ None
| Some (dep_conj r (conj in_rules concl_prop)) ⇒
let comp_res := Compare_dec.leb (minimal_rule_rank r) n in
match comp_res as cr
return comp_res = cr
→ rule_oracle_result V L (G_n_set V L n) s
with
| true ⇒ fun(H : comp_res = true) ⇒
Some(dep_conj _ _ r
(conj
(rank_rules_minimal_rule_rank (G_set V L) r n
in_rules (leb_complete _ _ H))
concl_prop))
| false ⇒ fun _ ⇒ None
end (eq_refl comp_res)
end.
Lemma well_founded_Gn_oracle : ∀(n : nat),
well_founded_rule_oracle (prop_Gn_oracle n) sequent_measure.
build_proof instantiation with a type that permits failure.
Definition prop_mod_build_proof_maybe(n : nat)(s : sequent V L) :
(proof (G_n_set V L n) simple_4_13_sequent s) + (sequent V L) :=
build_proof (S (sequent_measure s))
mod_prop_hyp_oracle (prop_Gn_oracle n) s.
(proof (G_n_set V L n) simple_4_13_sequent s) + (sequent V L) :=
build_proof (S (sequent_measure s))
mod_prop_hyp_oracle (prop_Gn_oracle n) s.
Proof that the proof search will always succeed.
Lemma prop_mod_build_proof_left : ∀(n : nat)(s : sequent V L),
rank_sequent n s →
is_inl (prop_mod_build_proof_maybe n s).
rank_sequent n s →
is_inl (prop_mod_build_proof_maybe n s).
Valid subset of the hypotheses
Definition valid_simple_4_13_sequent(nonempty_v : V)
(LS : lambda_structure L T)(n : nat) : set (sequent V L) :=
intersection simple_4_13_sequent
(step_semantics_valid_at_rank nonempty_v LS n).
Lemma valid_simple_4_13_sequent_list_reorder :
∀(nonempty_v : V)(LS : lambda_structure L T)(n : nat)
(s1 s2 : sequent V L),
list_reorder s1 s2 →
valid_simple_4_13_sequent nonempty_v LS n s1 →
valid_simple_4_13_sequent nonempty_v LS n s2.
(LS : lambda_structure L T)(n : nat) : set (sequent V L) :=
intersection simple_4_13_sequent
(step_semantics_valid_at_rank nonempty_v LS n).
Lemma valid_simple_4_13_sequent_list_reorder :
∀(nonempty_v : V)(LS : lambda_structure L T)(n : nat)
(s1 s2 : sequent V L),
list_reorder s1 s2 →
valid_simple_4_13_sequent nonempty_v LS n s1 →
valid_simple_4_13_sequent nonempty_v LS n s2.
Restrict the proof building in two ways: First, guarantee
success by type, second restrict hypotheses to valid sequents.
Definition prop_mod_build_proof(classic : classical_logic)(nonempty_v : V)
(LS : lambda_structure L T)
(n : nat)(s : sequent V L)(rank : rank_sequent (S n) s)
(valid : step_semantics_valid nonempty_v LS s n rank)
: proof (G_n_set V L (S n))
(valid_simple_4_13_sequent nonempty_v LS n) s :=
match prop_mod_build_proof_maybe (S n) s
as pmaybe
return is_inl pmaybe →
proof (G_n_set V L (S n))
(valid_simple_4_13_sequent nonempty_v LS n) s
with
| inl p ⇒ fun _ ⇒
restrict_hypothesis (step_semantics_valid_at_rank nonempty_v LS n)
(step_semantics_valid_G_rule_inductive nonempty_v LS n classic)
s
(dep_conj (rank_sequent (S n) s)
(step_semantics_valid nonempty_v LS s n)
rank valid)
p
| inr _ ⇒ fun(H : False) ⇒ False_rect _ H
end (prop_mod_build_proof_left (S n) s rank).
(LS : lambda_structure L T)
(n : nat)(s : sequent V L)(rank : rank_sequent (S n) s)
(valid : step_semantics_valid nonempty_v LS s n rank)
: proof (G_n_set V L (S n))
(valid_simple_4_13_sequent nonempty_v LS n) s :=
match prop_mod_build_proof_maybe (S n) s
as pmaybe
return is_inl pmaybe →
proof (G_n_set V L (S n))
(valid_simple_4_13_sequent nonempty_v LS n) s
with
| inl p ⇒ fun _ ⇒
restrict_hypothesis (step_semantics_valid_at_rank nonempty_v LS n)
(step_semantics_valid_G_rule_inductive nonempty_v LS n classic)
s
(dep_conj (rank_sequent (S n) s)
(step_semantics_valid nonempty_v LS s n)
rank valid)
p
| inr _ ⇒ fun(H : False) ⇒ False_rect _ H
end (prop_mod_build_proof_left (S n) s rank).
Lemma split_prop_mod :
∀(nonempty_v : V)(LS : lambda_structure L T)
(prop_s mod_s : sequent V L)
(n : nat)(rank : rank_sequent (2 + n) (mod_s ++ prop_s)),
classical_logic →
non_trivial_functor T →
prop_sequent prop_s →
top_modal_sequent mod_s →
¬ (simple_tautology prop_s) →
step_semantics_valid nonempty_v LS (mod_s ++ prop_s) (S n) rank →
step_semantics_valid nonempty_v LS mod_s (S n)
(rank_sequent_append_left _ _ _ rank).
Lemma n_completeness :
∀(enum_V : enumerator V)(LS : lambda_structure L T)
(rules : set (sequent_rule V L))
(osr : one_step_rule_set rules)
(n : nat)(s : sequent V L)(rank : rank_sequent (S n) s),
classical_logic →
non_trivial_functor T →
one_step_complete (enum_elem enum_V) LS rules osr →
step_semantics_valid (enum_elem enum_V) LS s n rank →
provable (GRC_n_set rules (S n)) (empty_sequent_set V L) s.
∀(enum_V : enumerator V)(LS : lambda_structure L T)
(rules : set (sequent_rule V L))
(osr : one_step_rule_set rules)
(n : nat)(s : sequent V L)(rank : rank_sequent (S n) s),
classical_logic →
non_trivial_functor T →
one_step_complete (enum_elem enum_V) LS rules osr →
step_semantics_valid (enum_elem enum_V) LS s n rank →
provable (GRC_n_set rules (S n)) (empty_sequent_set V L) s.
4.13, cut-free part
Lemma n_cut_free_completeness :
∀(enum_V : enumerator V)(LS : lambda_structure L T)
(rules : set (sequent_rule V L))
(osr : one_step_rule_set rules)
(n : nat)(s : sequent V L)(rank : rank_sequent (S n) s),
classical_logic →
non_trivial_functor T →
one_step_cut_free_complete (enum_elem enum_V) LS rules osr →
step_semantics_valid (enum_elem enum_V) LS s n rank →
provable (GR_n_set rules (S n)) (empty_sequent_set V L) s.
∀(enum_V : enumerator V)(LS : lambda_structure L T)
(rules : set (sequent_rule V L))
(osr : one_step_rule_set rules)
(n : nat)(s : sequent V L)(rank : rank_sequent (S n) s),
classical_logic →
non_trivial_functor T →
one_step_cut_free_complete (enum_elem enum_V) LS rules osr →
step_semantics_valid (enum_elem enum_V) LS s n rank →
provable (GR_n_set rules (S n)) (empty_sequent_set V L) s.
Lemma completeness :
∀(enum_V : enumerator V)(LS : lambda_structure L T)
(rules : set (sequent_rule V L))
(osr : one_step_rule_set rules)
(s : sequent V L),
classical_logic →
non_trivial_functor T →
one_step_complete (enum_elem enum_V) LS rules osr →
valid_all_models (enum_elem enum_V) LS s →
provable (GRC_set rules) (empty_sequent_set V L) s.
∀(enum_V : enumerator V)(LS : lambda_structure L T)
(rules : set (sequent_rule V L))
(osr : one_step_rule_set rules)
(s : sequent V L),
classical_logic →
non_trivial_functor T →
one_step_complete (enum_elem enum_V) LS rules osr →
valid_all_models (enum_elem enum_V) LS s →
provable (GRC_set rules) (empty_sequent_set V L) s.
4.14, cut-free part
Lemma cut_free_completeness :
∀(enum_V : enumerator V)(LS : lambda_structure L T)
(rules : set (sequent_rule V L))
(osr : one_step_rule_set rules)
(s : sequent V L),
classical_logic →
non_trivial_functor T →
one_step_cut_free_complete (enum_elem enum_V) LS rules osr →
valid_all_models (enum_elem enum_V) LS s →
provable (GR_set rules) (empty_sequent_set V L) s.
∀(enum_V : enumerator V)(LS : lambda_structure L T)
(rules : set (sequent_rule V L))
(osr : one_step_rule_set rules)
(s : sequent V L),
classical_logic →
non_trivial_functor T →
one_step_cut_free_complete (enum_elem enum_V) LS rules osr →
valid_all_models (enum_elem enum_V) LS s →
provable (GR_set rules) (empty_sequent_set V L) s.
Lemma semantic_admissible_rules :
∀(enum_V : enumerator V)(LS : lambda_structure L T)
(osr rules : set (sequent_rule V L))
(osr_prop : one_step_rule_set osr),
classical_logic →
non_trivial_functor T →
one_step_sound (enum_elem enum_V) LS osr osr_prop →
one_step_cut_free_complete (enum_elem enum_V) LS osr osr_prop →
downward_correct_rule_set (enum_elem enum_V) LS rules →
admissible_rule_set (GR_set osr) (empty_sequent_set V L) rules.
Theorem semantic_admissible_cut :
∀(enum_V : enumerator V)(LS : lambda_structure L T)
(rules : set (sequent_rule V L))
(osr_prop : one_step_rule_set rules),
classical_logic →
non_trivial_functor T →
one_step_sound (enum_elem enum_V) LS rules osr_prop →
one_step_cut_free_complete (enum_elem enum_V) LS rules osr_prop →
admissible_rule_set (GR_set rules) (empty_sequent_set V L)
is_cut_rule.
∀(enum_V : enumerator V)(LS : lambda_structure L T)
(rules : set (sequent_rule V L))
(osr_prop : one_step_rule_set rules),
classical_logic →
non_trivial_functor T →
one_step_sound (enum_elem enum_V) LS rules osr_prop →
one_step_cut_free_complete (enum_elem enum_V) LS rules osr_prop →
admissible_rule_set (GR_set rules) (empty_sequent_set V L)
is_cut_rule.
Theorem semantic_admissible_contraction :
∀(enum_V : enumerator V)(LS : lambda_structure L T)
(osr : set (sequent_rule V L))
(osr_prop : one_step_rule_set osr),
classical_logic →
non_trivial_functor T →
one_step_sound (enum_elem enum_V) LS osr osr_prop →
one_step_cut_free_complete (enum_elem enum_V) LS osr osr_prop →
admissible_rule_set (GR_set osr) (empty_sequent_set V L)
is_contraction_rule.
End Completeness.
∀(enum_V : enumerator V)(LS : lambda_structure L T)
(osr : set (sequent_rule V L))
(osr_prop : one_step_rule_set osr),
classical_logic →
non_trivial_functor T →
one_step_sound (enum_elem enum_V) LS osr osr_prop →
one_step_cut_free_complete (enum_elem enum_V) LS osr osr_prop →
admissible_rule_set (GR_set osr) (empty_sequent_set V L)
is_contraction_rule.
End Completeness.