diff options
Diffstat (limited to 'theories/Logic')
| -rw-r--r-- | theories/Logic/ClassicalFacts.v | 33 | ||||
| -rw-r--r-- | theories/Logic/HLevels.v | 146 |
2 files changed, 172 insertions, 7 deletions
diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v index 2a9e15ab37..8538b54c08 100644 --- a/theories/Logic/ClassicalFacts.v +++ b/theories/Logic/ClassicalFacts.v @@ -29,7 +29,7 @@ Table of contents: 3. Weak classical axioms -3.1. Weak excluded middle +3.1. Weak excluded middle and classical de Morgan law 3.2. Gödel-Dummett axiom and right distributivity of implication over disjunction @@ -514,7 +514,7 @@ End Weak_proof_irrelevance_CCI. (** * Weak classical axioms *) (** We show the following increasing in the strength of axioms: - - weak excluded-middle + - weak excluded-middle and classical De Morgan's law - right distributivity of implication over disjunction and Gödel-Dummett axiom - independence of general premises and drinker's paradox - excluded-middle @@ -523,11 +523,15 @@ End Weak_proof_irrelevance_CCI. (** ** Weak excluded-middle *) (** The weak classical logic based on [~~A \/ ~A] is referred to with - name KC in [[ChagrovZakharyaschev97]] + name KC in [[ChagrovZakharyaschev97]]. See [[SorbiTerwijn11]] for + a short survey. [[ChagrovZakharyaschev97]] Alexander Chagrov and Michael Zakharyaschev, "Modal Logic", Clarendon Press, 1997. -*) + + [[SorbiTerwijn11]] Andrea Sorbi and Sebastiaan A. Terwijn, + "Generalizations of the weak law of the excluded-middle", Notre + Dame J. Formal Logic, vol 56(2), pp 321-331, 2015. *) Definition weak_excluded_middle := forall A:Prop, ~~A \/ ~A. @@ -539,16 +543,21 @@ Definition weak_excluded_middle := Definition weak_generalized_excluded_middle := forall A B:Prop, ((A -> B) -> B) \/ (A -> B). +(** Classical De Morgan's law *) + +Definition classical_de_morgan_law := + forall A B:Prop, ~(A /\ B) -> ~A \/ ~B. + (** ** Gödel-Dummett axiom *) (** [(A->B) \/ (B->A)] is studied in [[Dummett59]] and is based on [[Gödel33]]. [[Dummett59]] Michael A. E. Dummett. "A Propositional Calculus - with a Denumerable Matrix", In the Journal of Symbolic Logic, Vol - 24 No. 2(1959), pp 97-103. + with a Denumerable Matrix", In the Journal of Symbolic Logic, vol + 24(2), pp 97-103, 1959. [[Gödel33]] Kurt Gödel. "Zum intuitionistischen Aussagenkalkül", - Ergeb. Math. Koll. 4 (1933), pp. 34-38. + Ergeb. Math. Koll. 4, pp. 34-38, 1933. *) Definition GodelDummett := forall A B:Prop, (A -> B) \/ (B -> A). @@ -590,6 +599,16 @@ Proof. right; intro HA; apply (HAnotA HA HA). Qed. +(** The weak excluded middle is equivalent to the classical De Morgan's law *) + +Lemma weak_excluded_middle_iff_classical_de_morgan_law : + weak_excluded_middle <-> classical_de_morgan_law. +Proof. + split; [intro WEM|intro CDML]; intros A *. + - destruct (WEM A); tauto. + - destruct (CDML A (~A)); tauto. +Qed. + (** ** Independence of general premises and drinker's paradox *) (** Independence of general premises is the unconstrained, non diff --git a/theories/Logic/HLevels.v b/theories/Logic/HLevels.v new file mode 100644 index 0000000000..010c4aad6f --- /dev/null +++ b/theories/Logic/HLevels.v @@ -0,0 +1,146 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** The first three levels of homotopy type theory: homotopy propositions, + homotopy sets and homotopy one types. For more information, + https://github.com/HoTT/HoTT + and + https://homotopytypetheory.org/book + + Univalence is not assumed here, and equality is Coq's usual inductive + type eq in sort Prop. This is a little different from HoTT, where + sort Prop does not exist and equality is directly in sort Type. *) + + +(* It is almost impossible to prove that a type is a homotopy proposition + without funext, so we assume it here. *) +Require Import Coq.Logic.FunctionalExtensionality. + +(* A homotopy proposition is a type that has at most one element. + Its unique inhabitant, when it exists, is to be interpreted as the + proof of the homotopy proposition. + Homotopy propositions are therefore an alternative to the sort Prop, + to select which types represent mathematical propositions. *) +Definition IsHProp (P : Type) : Prop + := forall p q : P, p = q. + +(* A homotopy set is a type such as each equality type x = y is a + homotopy proposition. For example, any type which equality is + decidable in sort Prop is a homotopy set, as shown in file + Coq.Logic.Eqdep_dec.v. *) +Definition IsHSet (X : Type) : Prop + := forall (x y : X) (p q : x = y), p = q. + +Definition IsHOneType (X : Type) : Prop + := forall (x y : X) (p q : x = y) (r s : p = q), r = s. + +Lemma forall_hprop : forall (A : Type) (P : A -> Prop), + (forall x:A, IsHProp (P x)) + -> IsHProp (forall x:A, P x). +Proof. + intros A P H p q. apply functional_extensionality_dep. + intro x. apply H. +Qed. + +(* Homotopy propositions are stable by conjunction, but not by disjunction, + which can have a proof by the left and another proof by the right. *) +Lemma and_hprop : forall P Q : Prop, + IsHProp P -> IsHProp Q -> IsHProp (P /\ Q). +Proof. + intros. intros p q. destruct p,q. + replace p0 with p. replace q0 with q. reflexivity. + apply H0. apply H. +Qed. + +Lemma impl_hprop : forall P Q : Prop, + IsHProp Q -> IsHProp (P -> Q). +Proof. + intros P Q H p q. apply functional_extensionality. + intros. apply H. +Qed. + +Lemma false_hprop : IsHProp False. +Proof. + intros p q. contradiction. +Qed. + +Lemma true_hprop : IsHProp True. +Proof. + intros p q. destruct p,q. reflexivity. +Qed. + +(* All negations are homotopy propositions. *) +Lemma not_hprop : forall P : Type, IsHProp (P -> False). +Proof. + intros P p q. apply functional_extensionality. + intros. contradiction. +Qed. + +(* Homotopy propositions are included in homotopy sets. + They are the first 2 levels of a cumulative hierarchy of types + indexed by the natural numbers. In homotopy type theory, + homotopy propositions are call (-1)-types and homotopy + sets 0-types. *) +Lemma hset_hprop : forall X : Type, + IsHProp X -> IsHSet X. +Proof. + intros X H. + assert (forall (x y z:X) (p : y = z), eq_trans (H x y) p = H x z). + { intros. unfold eq_trans, eq_ind. destruct p. reflexivity. } + assert (forall (x y z:X) (p : y = z), + p = eq_trans (eq_sym (H x y)) (H x z)). + { intros. rewrite <- (H0 x y z p). unfold eq_trans, eq_sym, eq_ind. + destruct p, (H x y). reflexivity. } + intros x y p q. + rewrite (H1 x x y p), (H1 x x y q). reflexivity. +Qed. + +Lemma eq_trans_cancel : forall {X : Type} {x y z : X} (p : x = y) (q r : y = z), + (eq_trans p q = eq_trans p r) -> q = r. +Proof. + intros. destruct p. simpl in H. destruct r. + simpl in H. rewrite eq_trans_refl_l in H. exact H. +Qed. + +Lemma hset_hOneType : forall X : Type, + IsHSet X -> IsHOneType X. +Proof. + intros X f x y p q. + pose (fun a => f x y p a) as g. + assert (forall a (r : q = a), eq_trans (g q) r = g a). + { intros. destruct a. subst q. reflexivity. } + intros r s. pose proof (H p (eq_sym r)). + pose proof (H p (eq_sym s)). + rewrite <- H1 in H0. apply eq_trans_cancel in H0. + rewrite <- eq_sym_involutive. rewrite <- (eq_sym_involutive r). + rewrite H0. reflexivity. +Qed. + +(* "IsHProp X" sounds like a proposition, because it asserts + a property of the type X. And indeed: *) +Lemma hprop_hprop : forall X : Type, + IsHProp (IsHProp X). +Proof. + intros X p q. + apply forall_hprop. intro x. + apply forall_hprop. intro y. intros f g. + apply (hset_hprop X p). +Qed. + +Lemma hprop_hset : forall X : Type, + IsHProp (IsHSet X). +Proof. + intros X f g. + apply functional_extensionality_dep. intro x. + apply functional_extensionality_dep. intro y. + apply functional_extensionality_dep. intro a. + apply functional_extensionality_dep. intro b. + apply (hset_hOneType). exact f. +Qed. |