Commit 28d67815 authored by litak's avatar litak

edits to fix terminology etc

parent 28fe2386
......@@ -387,7 +387,7 @@ Proof.
- apply andlist_dneg_help; trivial.
Qed.
Lemma heart_of_adequate_ggr:
Theorem regular_adequacy:
forall (Z : form) (G : context) (A : form),
KClbox Z G A ->
(KIbox Z [] (ggr Z)) ->
......@@ -421,8 +421,7 @@ Proof with trivial.
- apply_imp imp_dneg. eapply KIbox_orI2.
apply IHHGA...
- eauto 4 with KIboxDB.
- intuition.
apply box_dneg_rule with (G := map ggr G) (F := map ggr F); eauto.
- apply box_dneg_rule with (G := map ggr G) (F := map ggr F); eauto.
intros f Hf. rewrite in_map_iff in Hf.
destruct Hf as [fo [Hfo Hin]].
subst. eauto.
......@@ -442,7 +441,7 @@ intro Z. unfold adequate. split.
split; intros.
+ eapply eq_ded. apply eq_sym. apply cl_ggr_eq.
eapply map_eq. intros. apply cl_ggr_eq. apply int_to_cl. assumption.
+ apply heart_of_adequate_ggr; trivial.
+ apply regular_adequacy; trivial.
Qed.
......@@ -464,9 +463,8 @@ Qed.
(** ** Definitions of pre-/post-/¬¬-envelopes for KIbox *)
(** Now we define different kinds of envelopes. They are used to
(** Now we define the notion of pre-/post-/¬¬-envelopes. They are used to
describe the required properties for adequacy in the next parts.
Note the small difference between ¬¬- and Kuroda-envelopes.
*)
Definition sub_vars_dneg (A : form) := sub (fun n => -+! var n) A.
......@@ -480,8 +478,7 @@ Definition post_envelope (A : form) :=
Definition dneg_envelope (A : form) :=
forall Z, KIbox Z [] ((kol A) <<->> -+! (sub_vars_dneg A)).
Definition kuroda_envelope (Z : form) :=
forall A, KIbox Z [] ((kol A) <<->> -+! A).
(*
Definition gg_envelope (Z : form) :=
......@@ -620,7 +617,7 @@ Qed.
(** ** Enveloped Implications Theorem *)
(** Axioms of the form [(B ->> C)], where B is a post-envelope and C a pre-envelope,
form a adequate system. Kuroda- and ¬¬-envelopes also guarantee adequacy.
form a adequate system.
*)
Theorem thenvimpl_kol:
......@@ -666,16 +663,6 @@ Proof.
- eapply KIbox_impE. apply imp_dneg. apply KIbox_axiom.
Qed.
Theorem kuroda_envelope_adequate:
forall Z, kuroda_envelope Z -> adequate kol Z.
Proof.
unfold kuroda_envelope.
intros Z hip.
rewrite adequate_eq_kol.
eapply eq_ded.
- eapply eq_sym. apply hip.
- eapply KIbox_impE. apply imp_dneg. apply axiom_id.
Qed.
......@@ -683,12 +670,29 @@ Qed.
(** We introduce the Glivenko-translation, which is simply prefixing formulas by double negation.
Assuming [|[]| -+! A ->> -+! |[]| A], which is known as the Kuroda axiom, the Glivenko-translation
becomes equivalent to those in the triangle. We can thus deduct an adequacy result from it as well,
becomes equivalent to the regular ones (those ``in the triangle''). We can thus deduct an adequacy result from it as well,
of course still assuming the Kuroda axiom.
Additionally, we prove that Kuroda axiom follows from the axiom [p ->> |[]| p].
The final theorem states that a translation from the triangle or glv and an axiom [Z] are adequate if the
Kuroda axiom follows from [Z].
*)
*)
(** These results can be also stated using a suitable notion of envelope... *)
Definition kuroda_envelope (Z : form) :=
forall A, KIbox Z [] ((kol A) <<->> -+! A).
Theorem kuroda_envelope_adequate:
forall Z, kuroda_envelope Z -> adequate kol Z.
Proof.
unfold kuroda_envelope.
intros Z hip.
rewrite adequate_eq_kol.
eapply eq_ded.
- eapply eq_sym. apply hip.
- eapply KIbox_impE. apply imp_dneg. apply axiom_id.
Qed.
Definition glv (A : form) := -+! A.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment