Commit 855d84d3 authored by litak's avatar litak

stable shape after some edits

parent 7e4a131b
......@@ -65,8 +65,8 @@ Notation "{ Z + G } [-- A" := (KIbox Z G A) (at level 79).
(** * Equivalence Proofs for the Translations *)
(** In this section we prove that the given three translations result in equivalent formulas.
We will later refer to this fact as "the triangle", because one can view it as a triangle of equivalent formulas. *)
(** In this section we prove that the regular translations result in equivalent formulas.
In some parts of the proof script below, an old name for such translations as being "in the triangle" persisted. This name one can see the regular translations as lying in a triangle given by the refinement order on monotone modular ones. *)
Lemma eq_ggr_kur : forall Z f, KIbox Z [] ((ggr f) <<->> (kur f)).
Proof.
......@@ -206,15 +206,15 @@ Fixpoint dis_free_under_box (f : form) : Prop :=
(** * 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
([-+! p ->> p]), and introduces the notion of adequacy. A translation for a logic
defined by given axiom is adequate if the translation of a formula holds
intuitionistically iff the original formula holds classically. We show that
adequateness is equivalent for the translations in the triangle and that
adequacy is equivalent for the translations in the triangle and that
a system extended by an axiom is adequate iff the translation of the axioms holds
intuitionistically.
After that, we introduce the notion of envelopes to capture the properties,
axioms are required to have, in order to ensure adequateness of the resulting system.
axioms are required to have, in order to ensure adequacy of the resulting system.
Since the notion of an envelope is abstract, the next part shows examples of envelopes.
The last part explains which kind of envelopes result in an adequate system.
*)
......@@ -264,7 +264,7 @@ Proof.
Qed.
(* Definition and equivalence of adequateness *)
(* Definition and equivalence of adequacy *)
Definition adequate (f: form -> form) (Z : form) :=
forall G A, KIbox Z (map f G) (f A) <-> KClbox Z G A.
......@@ -461,7 +461,7 @@ Qed.
(** ** Definitions of pre-/post-/¬¬-envelopes for KIbox *)
(** Now we define different kinds of envelopes. They are used to
describe the required properties for adequateness in the next parts.
describe the required properties for adequacy in the next parts.
Note the small difference between ¬¬- and Kuroda-envelopes.
*)
......@@ -494,8 +494,8 @@ Qed.
(** ** 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.
(** Following are concrete examples of envelopes. Our first attempt at proving adequacy 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 adequacy 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.
*)
Lemma sub_vars_dneg_eq:
......@@ -611,7 +611,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 adequateness.
form a adequate system. Kuroda- and ¬¬-envelopes also guarantee adequacy.
*)
Theorem thenvimpl_kol:
......@@ -674,7 +674,7 @@ 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 a adequateness result from it as well,
becomes equivalent to 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
......
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