Commit 7e4a131b authored by litak's avatar litak

fixed names

parent 7066bd5c
......@@ -203,7 +203,7 @@ Fixpoint dis_free_under_box (f : form) : Prop :=
| _ => True
end.
(** * Towards Theorem 5 *)
(** * Towards Enveloped Implications Theorem *)
(** This sections defines KClbox, which is simply an extension of KIbox by the axiom
([-+! p ->> p]), and introduces the notion of adequateness. A translation for a logic
......@@ -492,7 +492,7 @@ Proof.
apply eq_split. split; assumption.
Qed.
(** ** Lemma 4 from the corrected ALCOP slides *)
(** ** Envelope Criteria Lemma *)
(** Following are concrete examples of envelopes. Our first attempt at proving adequateness was done with axioms being either disjunction free ([dis_free_under_box]) and [shallow] or completely [box_free].
It turned out that we could prove adequateness for an even less restrictive class of logics using envelopes. Still those stronger requirements are relevant for practical purpose and we will now show that our results apply to them as well.
......@@ -608,13 +608,13 @@ Proof.
eapply imp_rev. apply H.
Qed.
(** ** Theorem 5 from ALCOP slides *)
(** ** 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 adequateness.
*)
Theorem theorem5_kol:
Theorem thenvimpl_kol:
forall B C, post_envelope B -> pre_envelope C -> adequate kol (B ->> C).
Proof.
intros B C H H0.
......@@ -632,18 +632,18 @@ Proof.
Qed.
Corollary theorem5_ggr:
Corollary thenvimpl_ggr:
forall B C, post_envelope B -> pre_envelope C -> adequate ggr (B ->> C).
Proof.
intros B C H H0. eapply adequate_eq_ggr_kol.
apply theorem5_kol; trivial.
apply thenvimpl_kol; trivial.
Qed.
Corollary theorem5_kur:
Corollary thenvimpl_kur:
forall B C, post_envelope B -> pre_envelope C -> adequate kur (B ->> C).
Proof.
intros B C H H0. eapply adequate_eq_kol_kur.
apply theorem5_kol; trivial.
apply thenvimpl_kol; trivial.
Qed.
Theorem dneg_envelope_adequate:
......@@ -670,7 +670,7 @@ Qed.
(** * Towards Theorem 6 *)
(** * On the Kuroda axiom *)
(** 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
......@@ -780,7 +780,7 @@ Proof.
Qed.
Theorem theorem6_kol:
Theorem thkurax_kol:
forall Z, kuroda_axiom Z -> adequate kol Z.
Proof.
intros Z hip.
......@@ -800,21 +800,21 @@ Proof.
- apply ff_dneg.
Qed.
Corollary theorem6_glv:
Corollary thkurax_glv:
forall Z, kuroda_axiom Z -> adequate glv Z.
Proof.
intros Z H. rewrite <- adequate_triangle_glv; trivial.
rewrite adequate_eq_ggr_kol. apply theorem6_kol; trivial.
rewrite adequate_eq_ggr_kol. apply thkurax_kol; trivial.
Qed.
Corollary theorem6_ggr:
Corollary thkurax_ggr:
forall Z, kuroda_axiom Z -> adequate ggr Z.
Proof.
intros Z H. rewrite adequate_eq_ggr_kol. apply theorem6_kol; trivial.
intros Z H. rewrite adequate_eq_ggr_kol. apply thkurax_kol; trivial.
Qed.
Corollary theorem6_kur:
Corollary thkurax_kur:
forall Z, kuroda_axiom Z -> adequate kur Z.
Proof.
intros Z H. rewrite <- adequate_eq_kol_kur. apply theorem6_kol; trivial.
intros Z H. rewrite <- adequate_eq_kol_kur. apply thkurax_kol; trivial.
Qed.
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