diff options
Diffstat (limited to 'theories/Logic/ClassicalFacts.v')
| -rw-r--r-- | theories/Logic/ClassicalFacts.v | 452 |
1 files changed, 228 insertions, 224 deletions
diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v index 70da74d3..dd911db6 100644 --- a/theories/Logic/ClassicalFacts.v +++ b/theories/Logic/ClassicalFacts.v @@ -7,39 +7,39 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ClassicalFacts.v 8892 2006-06-04 17:59:53Z herbelin $ i*) +(*i $Id: ClassicalFacts.v 9245 2006-10-17 12:53:34Z notin $ i*) -(** ** Some facts and definitions about classical logic +(** Some facts and definitions about classical logic Table of contents: -A. Propositional degeneracy = excluded-middle + propositional extensionality +1. Propositional degeneracy = excluded-middle + propositional extensionality -B. Classical logic and proof-irrelevance +2. Classical logic and proof-irrelevance -B. 1. CC |- prop. ext. + A inhabited -> (A = A->A) -> A has fixpoint +2.1. CC |- prop. ext. + A inhabited -> (A = A->A) -> A has fixpoint -B. 2. CC |- prop. ext. + dep elim on bool -> proof-irrelevance +2.2. CC |- prop. ext. + dep elim on bool -> proof-irrelevance -B. 3. CIC |- prop. ext. -> proof-irrelevance +2.3. CIC |- prop. ext. -> proof-irrelevance -B. 4. CC |- excluded-middle + dep elim on bool -> proof-irrelevance +2.4. CC |- excluded-middle + dep elim on bool -> proof-irrelevance -B. 5. CIC |- excluded-middle -> proof-irrelevance +2.5. CIC |- excluded-middle -> proof-irrelevance -C. Weak classical axioms +3. Weak classical axioms -C. 1. Weak excluded middle +3.1. Weak excluded middle -C. 2. Gödel-Dummet axiom and right distributivity of implication over +3.2. Gödel-Dummet axiom and right distributivity of implication over disjunction -C. 3. Independence of general premises and drinker's paradox +3 3. Independence of general premises and drinker's paradox *) (************************************************************************) -(** *** A. Prop degeneracy = excluded-middle + prop extensionality *) +(** * Prop degeneracy = excluded-middle + prop extensionality *) (** i.e. [(forall A, A=True \/ A=False) <-> @@ -61,41 +61,41 @@ Definition excluded_middle := forall A:Prop, A \/ ~ A. Lemma prop_degen_ext : prop_degeneracy -> prop_extensionality. Proof. -intros H A B [Hab Hba]. -destruct (H A); destruct (H B). - rewrite H1; exact H0. - absurd B. - rewrite H1; exact (fun H => H). - apply Hab; rewrite H0; exact I. - absurd A. - rewrite H0; exact (fun H => H). - apply Hba; rewrite H1; exact I. - rewrite H1; exact H0. + intros H A B [Hab Hba]. + destruct (H A); destruct (H B). + rewrite H1; exact H0. + absurd B. + rewrite H1; exact (fun H => H). + apply Hab; rewrite H0; exact I. + absurd A. + rewrite H0; exact (fun H => H). + apply Hba; rewrite H1; exact I. + rewrite H1; exact H0. Qed. Lemma prop_degen_em : prop_degeneracy -> excluded_middle. Proof. -intros H A. -destruct (H A). - left; rewrite H0; exact I. - right; rewrite H0; exact (fun x => x). + intros H A. + destruct (H A). + left; rewrite H0; exact I. + right; rewrite H0; exact (fun x => x). Qed. Lemma prop_ext_em_degen : - prop_extensionality -> excluded_middle -> prop_degeneracy. + prop_extensionality -> excluded_middle -> prop_degeneracy. Proof. -intros Ext EM A. -destruct (EM A). - left; apply (Ext A True); split; - [ exact (fun _ => I) | exact (fun _ => H) ]. - right; apply (Ext A False); split; [ exact H | apply False_ind ]. + intros Ext EM A. + destruct (EM A). + left; apply (Ext A True); split; + [ exact (fun _ => I) | exact (fun _ => H) ]. + right; apply (Ext A False); split; [ exact H | apply False_ind ]. Qed. (************************************************************************) -(** *** B. Classical logic and proof-irrelevance *) +(** * Classical logic and proof-irrelevance *) (************************************************************************) -(** **** B. 1. CC |- prop ext + A inhabited -> (A = A->A) -> A has fixpoint *) +(** ** CC |- prop ext + A inhabited -> (A = A->A) -> A has fixpoint *) (** We successively show that: @@ -110,41 +110,41 @@ Qed. Definition inhabited (A:Prop) := A. Lemma prop_ext_A_eq_A_imp_A : - prop_extensionality -> forall A:Prop, inhabited A -> (A -> A) = A. + prop_extensionality -> forall A:Prop, inhabited A -> (A -> A) = A. Proof. -intros Ext A a. -apply (Ext (A -> A) A); split; [ exact (fun _ => a) | exact (fun _ _ => a) ]. + intros Ext A a. + apply (Ext (A -> A) A); split; [ exact (fun _ => a) | exact (fun _ _ => a) ]. Qed. Record retract (A B:Prop) : Prop := {f1 : A -> B; f2 : B -> A; f1_o_f2 : forall x:B, f1 (f2 x) = x}. Lemma prop_ext_retract_A_A_imp_A : - prop_extensionality -> forall A:Prop, inhabited A -> retract A (A -> A). + prop_extensionality -> forall A:Prop, inhabited A -> retract A (A -> A). Proof. -intros Ext A a. -rewrite (prop_ext_A_eq_A_imp_A Ext A a). -exists (fun x:A => x) (fun x:A => x). -reflexivity. + intros Ext A a. + rewrite (prop_ext_A_eq_A_imp_A Ext A a). + exists (fun x:A => x) (fun x:A => x). + reflexivity. Qed. Record has_fixpoint (A:Prop) : Prop := {F : (A -> A) -> A; Fix : forall f:A -> A, F f = f (F f)}. Lemma ext_prop_fixpoint : - prop_extensionality -> forall A:Prop, inhabited A -> has_fixpoint A. + prop_extensionality -> forall A:Prop, inhabited A -> has_fixpoint A. Proof. -intros Ext A a. -case (prop_ext_retract_A_A_imp_A Ext A a); intros g1 g2 g1_o_g2. -exists (fun f => (fun x:A => f (g1 x x)) (g2 (fun x => f (g1 x x)))). -intro f. -pattern (g1 (g2 (fun x:A => f (g1 x x)))) at 1 in |- *. -rewrite (g1_o_g2 (fun x:A => f (g1 x x))). -reflexivity. + intros Ext A a. + case (prop_ext_retract_A_A_imp_A Ext A a); intros g1 g2 g1_o_g2. + exists (fun f => (fun x:A => f (g1 x x)) (g2 (fun x => f (g1 x x)))). + intro f. + pattern (g1 (g2 (fun x:A => f (g1 x x)))) at 1 in |- *. + rewrite (g1_o_g2 (fun x:A => f (g1 x x))). + reflexivity. Qed. (************************************************************************) -(** **** B. 2. CC |- prop_ext /\ dep elim on bool -> proof-irrelevance *) +(** ** CC |- prop_ext /\ dep elim on bool -> proof-irrelevance *) (** [proof_irrelevance] asserts equality of all proofs of a given formula *) Definition proof_irrelevance := forall (A:Prop) (a1 a2:A), a1 = a2. @@ -161,44 +161,44 @@ Definition proof_irrelevance := forall (A:Prop) (a1 a2:A), a1 = a2. Section Proof_irrelevance_gen. -Variable bool : Prop. -Variable true : bool. -Variable false : bool. -Hypothesis bool_elim : forall C:Prop, C -> C -> bool -> C. -Hypothesis - bool_elim_redl : forall (C:Prop) (c1 c2:C), c1 = bool_elim C c1 c2 true. -Hypothesis - bool_elim_redr : forall (C:Prop) (c1 c2:C), c2 = bool_elim C c1 c2 false. -Let bool_dep_induction := + Variable bool : Prop. + Variable true : bool. + Variable false : bool. + Hypothesis bool_elim : forall C:Prop, C -> C -> bool -> C. + Hypothesis + bool_elim_redl : forall (C:Prop) (c1 c2:C), c1 = bool_elim C c1 c2 true. + Hypothesis + bool_elim_redr : forall (C:Prop) (c1 c2:C), c2 = bool_elim C c1 c2 false. + Let bool_dep_induction := forall P:bool -> Prop, P true -> P false -> forall b:bool, P b. -Lemma aux : prop_extensionality -> bool_dep_induction -> true = false. -Proof. -intros Ext Ind. -case (ext_prop_fixpoint Ext bool true); intros G Gfix. -set (neg := fun b:bool => bool_elim bool false true b). -generalize (refl_equal (G neg)). -pattern (G neg) at 1 in |- *. -apply Ind with (b := G neg); intro Heq. -rewrite (bool_elim_redl bool false true). -change (true = neg true) in |- *; rewrite Heq; apply Gfix. -rewrite (bool_elim_redr bool false true). -change (neg false = false) in |- *; rewrite Heq; symmetry in |- *; - apply Gfix. -Qed. - -Lemma ext_prop_dep_proof_irrel_gen : - prop_extensionality -> bool_dep_induction -> proof_irrelevance. -Proof. -intros Ext Ind A a1 a2. -set (f := fun b:bool => bool_elim A a1 a2 b). -rewrite (bool_elim_redl A a1 a2). -change (f true = a2) in |- *. -rewrite (bool_elim_redr A a1 a2). -change (f true = f false) in |- *. -rewrite (aux Ext Ind). -reflexivity. -Qed. + Lemma aux : prop_extensionality -> bool_dep_induction -> true = false. + Proof. + intros Ext Ind. + case (ext_prop_fixpoint Ext bool true); intros G Gfix. + set (neg := fun b:bool => bool_elim bool false true b). + generalize (refl_equal (G neg)). + pattern (G neg) at 1 in |- *. + apply Ind with (b := G neg); intro Heq. + rewrite (bool_elim_redl bool false true). + change (true = neg true) in |- *; rewrite Heq; apply Gfix. + rewrite (bool_elim_redr bool false true). + change (neg false = false) in |- *; rewrite Heq; symmetry in |- *; + apply Gfix. + Qed. + + Lemma ext_prop_dep_proof_irrel_gen : + prop_extensionality -> bool_dep_induction -> proof_irrelevance. + Proof. + intros Ext Ind A a1 a2. + set (f := fun b:bool => bool_elim A a1 a2 b). + rewrite (bool_elim_redl A a1 a2). + change (f true = a2) in |- *. + rewrite (bool_elim_redr A a1 a2). + change (f true = f false) in |- *. + rewrite (aux Ext Ind). + reflexivity. + Qed. End Proof_irrelevance_gen. @@ -208,29 +208,30 @@ End Proof_irrelevance_gen. *) Section Proof_irrelevance_Prop_Ext_CC. - -Definition BoolP := forall C:Prop, C -> C -> C. -Definition TrueP : BoolP := fun C c1 c2 => c1. -Definition FalseP : BoolP := fun C c1 c2 => c2. -Definition BoolP_elim C c1 c2 (b:BoolP) := b C c1 c2. -Definition BoolP_elim_redl (C:Prop) (c1 c2:C) : - c1 = BoolP_elim C c1 c2 TrueP := refl_equal c1. -Definition BoolP_elim_redr (C:Prop) (c1 c2:C) : - c2 = BoolP_elim C c1 c2 FalseP := refl_equal c2. - -Definition BoolP_dep_induction := - forall P:BoolP -> Prop, P TrueP -> P FalseP -> forall b:BoolP, P b. - -Lemma ext_prop_dep_proof_irrel_cc : - prop_extensionality -> BoolP_dep_induction -> proof_irrelevance. -Proof - ext_prop_dep_proof_irrel_gen BoolP TrueP FalseP BoolP_elim BoolP_elim_redl - BoolP_elim_redr. + + Definition BoolP := forall C:Prop, C -> C -> C. + Definition TrueP : BoolP := fun C c1 c2 => c1. + Definition FalseP : BoolP := fun C c1 c2 => c2. + Definition BoolP_elim C c1 c2 (b:BoolP) := b C c1 c2. + Definition BoolP_elim_redl (C:Prop) (c1 c2:C) : + c1 = BoolP_elim C c1 c2 TrueP := refl_equal c1. + Definition BoolP_elim_redr (C:Prop) (c1 c2:C) : + c2 = BoolP_elim C c1 c2 FalseP := refl_equal c2. + + Definition BoolP_dep_induction := + forall P:BoolP -> Prop, P TrueP -> P FalseP -> forall b:BoolP, P b. + + Lemma ext_prop_dep_proof_irrel_cc : + prop_extensionality -> BoolP_dep_induction -> proof_irrelevance. + Proof. + exact (ext_prop_dep_proof_irrel_gen BoolP TrueP FalseP BoolP_elim BoolP_elim_redl + BoolP_elim_redr). + Qed. End Proof_irrelevance_Prop_Ext_CC. (************************************************************************) -(** **** B. 3. CIC |- prop. ext. -> proof-irrelevance *) +(** ** CIC |- prop. ext. -> proof-irrelevance *) (** In the Calculus of Inductive Constructions, inductively defined booleans enjoy dependent case analysis, hence directly proof-irrelevance from @@ -238,21 +239,22 @@ End Proof_irrelevance_Prop_Ext_CC. *) Section Proof_irrelevance_CIC. - -Inductive boolP : Prop := - | trueP : boolP - | falseP : boolP. -Definition boolP_elim_redl (C:Prop) (c1 c2:C) : - c1 = boolP_ind C c1 c2 trueP := refl_equal c1. -Definition boolP_elim_redr (C:Prop) (c1 c2:C) : - c2 = boolP_ind C c1 c2 falseP := refl_equal c2. -Scheme boolP_indd := Induction for boolP Sort Prop. - -Lemma ext_prop_dep_proof_irrel_cic : prop_extensionality -> proof_irrelevance. -Proof - fun pe => - ext_prop_dep_proof_irrel_gen boolP trueP falseP boolP_ind boolP_elim_redl - boolP_elim_redr pe boolP_indd. + + Inductive boolP : Prop := + | trueP : boolP + | falseP : boolP. + Definition boolP_elim_redl (C:Prop) (c1 c2:C) : + c1 = boolP_ind C c1 c2 trueP := refl_equal c1. + Definition boolP_elim_redr (C:Prop) (c1 c2:C) : + c2 = boolP_ind C c1 c2 falseP := refl_equal c2. + Scheme boolP_indd := Induction for boolP Sort Prop. + + Lemma ext_prop_dep_proof_irrel_cic : prop_extensionality -> proof_irrelevance. + Proof. + exact (fun pe => + ext_prop_dep_proof_irrel_gen boolP trueP falseP boolP_ind boolP_elim_redl + boolP_elim_redr pe boolP_indd). + Qed. End Proof_irrelevance_CIC. @@ -267,12 +269,12 @@ End Proof_irrelevance_CIC. cannot be refined. [[Berardi90]] Stefano Berardi, "Type dependence and constructive - mathematics", Ph. D. thesis, Dipartimento Matematica, Università di + mathematics", Ph. D. thesis, Dipartimento Matematica, Università di Torino, 1990. *) (************************************************************************) -(** **** B. 4. CC |- excluded-middle + dep elim on bool -> proof-irrelevance *) +(** ** CC |- excluded-middle + dep elim on bool -> proof-irrelevance *) (** This is a proof in the pure Calculus of Construction that classical logic in [Prop] + dependent elimination of disjunction entails @@ -293,60 +295,61 @@ End Proof_irrelevance_CIC. Require Import Hurkens. Section Proof_irrelevance_EM_CC. - -Variable or : Prop -> Prop -> Prop. -Variable or_introl : forall A B:Prop, A -> or A B. -Variable or_intror : forall A B:Prop, B -> or A B. -Hypothesis or_elim : forall A B C:Prop, (A -> C) -> (B -> C) -> or A B -> C. -Hypothesis - or_elim_redl : + + Variable or : Prop -> Prop -> Prop. + Variable or_introl : forall A B:Prop, A -> or A B. + Variable or_intror : forall A B:Prop, B -> or A B. + Hypothesis or_elim : forall A B C:Prop, (A -> C) -> (B -> C) -> or A B -> C. + Hypothesis + or_elim_redl : forall (A B C:Prop) (f:A -> C) (g:B -> C) (a:A), f a = or_elim A B C f g (or_introl A B a). -Hypothesis - or_elim_redr : + Hypothesis + or_elim_redr : forall (A B C:Prop) (f:A -> C) (g:B -> C) (b:B), g b = or_elim A B C f g (or_intror A B b). -Hypothesis - or_dep_elim : + Hypothesis + or_dep_elim : forall (A B:Prop) (P:or A B -> Prop), (forall a:A, P (or_introl A B a)) -> (forall b:B, P (or_intror A B b)) -> forall b:or A B, P b. - -Hypothesis em : forall A:Prop, or A (~ A). -Variable B : Prop. -Variables b1 b2 : B. - -(** [p2b] and [b2p] form a retract if [~b1=b2] *) - -Definition p2b A := or_elim A (~ A) B (fun _ => b1) (fun _ => b2) (em A). -Definition b2p b := b1 = b. - -Lemma p2p1 : forall A:Prop, A -> b2p (p2b A). -Proof. - unfold p2b in |- *; intro A; apply or_dep_elim with (b := em A); - unfold b2p in |- *; intros. - apply (or_elim_redl A (~ A) B (fun _ => b1) (fun _ => b2)). - destruct (b H). -Qed. -Lemma p2p2 : b1 <> b2 -> forall A:Prop, b2p (p2b A) -> A. -Proof. - intro not_eq_b1_b2. - unfold p2b in |- *; intro A; apply or_dep_elim with (b := em A); - unfold b2p in |- *; intros. - assumption. - destruct not_eq_b1_b2. - rewrite <- (or_elim_redr A (~ A) B (fun _ => b1) (fun _ => b2)) in H. - assumption. -Qed. - -(** Using excluded-middle a second time, we get proof-irrelevance *) - -Theorem proof_irrelevance_cc : b1 = b2. -Proof. - refine (or_elim _ _ _ _ _ (em (b1 = b2))); intro H. + + Hypothesis em : forall A:Prop, or A (~ A). + Variable B : Prop. + Variables b1 b2 : B. + + (** [p2b] and [b2p] form a retract if [~b1=b2] *) + + Definition p2b A := or_elim A (~ A) B (fun _ => b1) (fun _ => b2) (em A). + Definition b2p b := b1 = b. + + Lemma p2p1 : forall A:Prop, A -> b2p (p2b A). + Proof. + unfold p2b in |- *; intro A; apply or_dep_elim with (b := em A); + unfold b2p in |- *; intros. + apply (or_elim_redl A (~ A) B (fun _ => b1) (fun _ => b2)). + destruct (b H). + Qed. + + Lemma p2p2 : b1 <> b2 -> forall A:Prop, b2p (p2b A) -> A. + Proof. + intro not_eq_b1_b2. + unfold p2b in |- *; intro A; apply or_dep_elim with (b := em A); + unfold b2p in |- *; intros. + assumption. + destruct not_eq_b1_b2. + rewrite <- (or_elim_redr A (~ A) B (fun _ => b1) (fun _ => b2)) in H. + assumption. + Qed. + + (** Using excluded-middle a second time, we get proof-irrelevance *) + + Theorem proof_irrelevance_cc : b1 = b2. + Proof. + refine (or_elim _ _ _ _ _ (em (b1 = b2))); intro H. trivial. - apply (paradox B p2b b2p (p2p2 H) p2p1). -Qed. + apply (paradox B p2b b2p (p2p2 H) p2p1). + Qed. End Proof_irrelevance_EM_CC. @@ -357,7 +360,7 @@ End Proof_irrelevance_EM_CC. *) (************************************************************************) -(** **** B. 5. CIC |- excluded-middle -> proof-irrelevance *) +(** ** CIC |- excluded-middle -> proof-irrelevance *) (** Since, dependent elimination is derivable in the Calculus of @@ -367,18 +370,19 @@ End Proof_irrelevance_EM_CC. Section Proof_irrelevance_CCI. -Hypothesis em : forall A:Prop, A \/ ~ A. - -Definition or_elim_redl (A B C:Prop) (f:A -> C) (g:B -> C) - (a:A) : f a = or_ind f g (or_introl B a) := refl_equal (f a). -Definition or_elim_redr (A B C:Prop) (f:A -> C) (g:B -> C) - (b:B) : g b = or_ind f g (or_intror A b) := refl_equal (g b). -Scheme or_indd := Induction for or Sort Prop. - -Theorem proof_irrelevance_cci : forall (B:Prop) (b1 b2:B), b1 = b2. -Proof - proof_irrelevance_cc or or_introl or_intror or_ind or_elim_redl - or_elim_redr or_indd em. + Hypothesis em : forall A:Prop, A \/ ~ A. + + Definition or_elim_redl (A B C:Prop) (f:A -> C) (g:B -> C) + (a:A) : f a = or_ind f g (or_introl B a) := refl_equal (f a). + Definition or_elim_redr (A B C:Prop) (f:A -> C) (g:B -> C) + (b:B) : g b = or_ind f g (or_intror A b) := refl_equal (g b). + Scheme or_indd := Induction for or Sort Prop. + + Theorem proof_irrelevance_cci : forall (B:Prop) (b1 b2:B), b1 = b2. + Proof. + exact (proof_irrelevance_cc or or_introl or_intror or_ind or_elim_redl + or_elim_redr or_indd em). + Qed. End Proof_irrelevance_CCI. @@ -388,16 +392,16 @@ End Proof_irrelevance_CCI. [em : forall A:Prop, {A}+{~A}] in the Set-impredicative CCI. *) -(** *** C. Weak classical axioms *) +(** * Weak classical axioms *) (** We show the following increasing in the strength of axioms: - weak excluded-middle - - right distributivity of implication over disjunction and Gödel-Dummet axiom + - right distributivity of implication over disjunction and Gödel-Dummet axiom - independence of general premises and drinker's paradox - excluded-middle *) -(** **** C. 1. Weak excluded-middle *) +(** ** Weak excluded-middle *) (** The weak classical logic based on [~~A \/ ~A] is referred to with name KC in {[ChagrovZakharyaschev97]] @@ -411,20 +415,20 @@ Definition weak_excluded_middle := (** The interest in the equivalent variant [weak_generalized_excluded_middle] is that it holds even in logic - without a primitive [False] connective (like Gödel-Dummett axiom) *) + without a primitive [False] connective (like Gödel-Dummett axiom) *) Definition weak_generalized_excluded_middle := forall A B:Prop, ((A -> B) -> B) \/ (A -> B). -(** **** C. 2. Gödel-Dummett axiom *) +(** ** Gödel-Dummett axiom *) -(** [(A->B) \/ (B->A)] is studied in [[Dummett59]] and is based on [[Gödel33]]. +(** [(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. - [[Gödel33]] Kurt Gödel. "Zum intuitionistischen Aussagenkalkül", + [[Gödel33]] Kurt Gödel. "Zum intuitionistischen Aussagenkalkül", Ergeb. Math. Koll. 4 (1933), pp. 34-38. *) @@ -432,7 +436,7 @@ Definition GodelDummett := forall A B:Prop, (A -> B) \/ (B -> A). Lemma excluded_middle_Godel_Dummett : excluded_middle -> GodelDummett. Proof. -intros EM A B. destruct (EM B) as [HB|HnotB]. + intros EM A B. destruct (EM B) as [HB|HnotB]. left; intros _; exact HB. right; intros HB; destruct (HnotB HB). Qed. @@ -446,15 +450,15 @@ Definition RightDistributivityImplicationOverDisjunction := Lemma Godel_Dummett_iff_right_distr_implication_over_disjunction : GodelDummett <-> RightDistributivityImplicationOverDisjunction. Proof. -split. - intros GD A B C HCAB. - destruct (GD B A) as [HBA|HAB]; [left|right]; intro HC; - destruct (HCAB HC) as [HA|HB]; [ | apply HBA | apply HAB | ]; assumption. - intros Distr A B. - destruct (Distr A B (A\/B)) as [HABA|HABB]. - intro HAB; exact HAB. - right; intro HB; apply HABA; right; assumption. - left; intro HA; apply HABB; left; assumption. + split. + intros GD A B C HCAB. + destruct (GD B A) as [HBA|HAB]; [left|right]; intro HC; + destruct (HCAB HC) as [HA|HB]; [ | apply HBA | apply HAB | ]; assumption. + intros Distr A B. + destruct (Distr A B (A\/B)) as [HABA|HABB]. + intro HAB; exact HAB. + right; intro HB; apply HABA; right; assumption. + left; intro HA; apply HABB; left; assumption. Qed. (** [(A->B) \/ (B->A)] is stronger than the weak excluded middle *) @@ -462,12 +466,12 @@ Qed. Lemma Godel_Dummett_weak_excluded_middle : GodelDummett -> weak_excluded_middle. Proof. -intros GD A. destruct (GD (~A) A) as [HnotAA|HAnotA]. - left; intro HnotA; apply (HnotA (HnotAA HnotA)). - right; intro HA; apply (HAnotA HA HA). + intros GD A. destruct (GD (~A) A) as [HnotAA|HAnotA]. + left; intro HnotA; apply (HnotA (HnotAA HnotA)). + right; intro HA; apply (HAnotA HA HA). Qed. -(** **** C. 3. Independence of general premises and drinker's paradox *) +(** ** Independence of general premises and drinker's paradox *) (** Independence of general premises is the unconstrained, non constructive, version of the Independence of Premises as @@ -475,13 +479,13 @@ Qed. It is a generalization to predicate logic of the right distributivity of implication over disjunction (hence of - Gödel-Dummett axiom) whose own constructive form (obtained by a + Gödel-Dummett axiom) whose own constructive form (obtained by a restricting the third formula to be negative) is called Kreisel-Putnam principle [[KreiselPutnam57]]. [[KreiselPutnam57]], Georg Kreisel and Hilary Putnam. "Eine - Unableitsbarkeitsbeweismethode für den intuitionistischen - Aussagenkalkül". Archiv für Mathematische Logik und + Unableitsbarkeitsbeweismethode für den intuitionistischen + Aussagenkalkül". Archiv für Mathematische Logik und Graundlagenforschung, 3:74- 78, 1957. [[Troelstra73]], Anne Troelstra, editor. Metamathematical @@ -499,33 +503,33 @@ Lemma independence_general_premises_right_distr_implication_over_disjunction : IndependenceOfGeneralPremises -> RightDistributivityImplicationOverDisjunction. Proof. -intros IP A B C HCAB. -destruct (IP bool (fun b => if b then A else B) C true) as ([|],H). - intro HC; destruct (HCAB HC); [exists true|exists false]; assumption. - left; assumption. - right; assumption. + intros IP A B C HCAB. + destruct (IP bool (fun b => if b then A else B) C true) as ([|],H). + intro HC; destruct (HCAB HC); [exists true|exists false]; assumption. + left; assumption. + right; assumption. Qed. Lemma independence_general_premises_Godel_Dummett : IndependenceOfGeneralPremises -> GodelDummett. Proof. -destruct Godel_Dummett_iff_right_distr_implication_over_disjunction. -auto using independence_general_premises_right_distr_implication_over_disjunction. + destruct Godel_Dummett_iff_right_distr_implication_over_disjunction. + auto using independence_general_premises_right_distr_implication_over_disjunction. Qed. (** Independence of general premises is equivalent to the drinker's paradox *) Definition DrinkerParadox := forall (A:Type) (P:A -> Prop), - inhabited A -> exists x, (exists x, P x) -> P x. + inhabited A -> exists x, (exists x, P x) -> P x. Lemma independence_general_premises_drinker : IndependenceOfGeneralPremises <-> DrinkerParadox. Proof. -split. - intros IP A P InhA; apply (IP A P (exists x, P x) InhA); intro Hx; exact Hx. - intros Drinker A P Q InhA H; destruct (Drinker A P InhA) as (x,Hx). - exists x; intro HQ; apply (Hx (H HQ)). + split. + intros IP A P InhA; apply (IP A P (exists x, P x) InhA); intro Hx; exact Hx. + intros Drinker A P Q InhA H; destruct (Drinker A P InhA) as (x,Hx). + exists x; intro HQ; apply (Hx (H HQ)). Qed. (** Independence of general premises is weaker than (generalized) @@ -537,9 +541,9 @@ Definition generalized_excluded_middle := Lemma excluded_middle_independence_general_premises : generalized_excluded_middle -> DrinkerParadox. Proof. -intros GEM A P x0. -destruct (GEM (exists x, P x) (P x0)) as [(x,Hx)|Hnot]. - exists x; intro; exact Hx. - exists x0; exact Hnot. + intros GEM A P x0. + destruct (GEM (exists x, P x) (P x0)) as [(x,Hx)|Hnot]. + exists x; intro; exact Hx. + exists x0; exact Hnot. Qed. |