From 6b649aba925b6f7462da07599fe67ebb12a3460e Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Wed, 28 Jul 2004 21:54:47 +0000 Subject: Imported Upstream version 8.0pl1 --- theories/Logic/Berardi.v | 159 +++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 159 insertions(+) create mode 100644 theories/Logic/Berardi.v (limited to 'theories/Logic/Berardi.v') diff --git a/theories/Logic/Berardi.v b/theories/Logic/Berardi.v new file mode 100644 index 00000000..7e950c17 --- /dev/null +++ b/theories/Logic/Berardi.v @@ -0,0 +1,159 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* > *) + +Set Implicit Arguments. + +Section Berardis_paradox. + +(** Excluded middle *) +Hypothesis EM : forall P:Prop, P \/ ~ P. + +(** Conditional on any proposition. *) +Definition IFProp (P B:Prop) (e1 e2:P) := + match EM B with + | or_introl _ => e1 + | or_intror _ => e2 + end. + +(** Axiom of choice applied to disjunction. + Provable in Coq because of dependent elimination. *) +Lemma AC_IF : + forall (P B:Prop) (e1 e2:P) (Q:P -> Prop), + (B -> Q e1) -> (~ B -> Q e2) -> Q (IFProp B e1 e2). +Proof. +intros P B e1 e2 Q p1 p2. +unfold IFProp in |- *. +case (EM B); assumption. +Qed. + + +(** We assume a type with two elements. They play the role of booleans. + The main theorem under the current assumptions is that [T=F] *) +Variable Bool : Prop. +Variable T : Bool. +Variable F : Bool. + +(** The powerset operator *) +Definition pow (P:Prop) := P -> Bool. + + +(** A piece of theory about retracts *) +Section Retracts. + +Variables A B : Prop. + +Record retract : Prop := + {i : A -> B; j : B -> A; inv : forall a:A, j (i a) = a}. + +Record retract_cond : Prop := + {i2 : A -> B; j2 : B -> A; inv2 : retract -> forall a:A, j2 (i2 a) = a}. + + +(** The dependent elimination above implies the axiom of choice: *) +Lemma AC : forall r:retract_cond, retract -> forall a:A, j2 r (i2 r a) = a. +Proof. +intros r. +case r; simpl in |- *. +trivial. +Qed. + +End Retracts. + +(** This lemma is basically a commutation of implication and existential + quantification: (EX x | A -> P(x)) <=> (A -> EX x | P(x)) + which is provable in classical logic ( => is already provable in + intuitionnistic logic). *) + +Lemma L1 : forall A B:Prop, retract_cond (pow A) (pow B). +Proof. +intros A B. +elim (EM (retract (pow A) (pow B))). +intros [f0 g0 e]. +exists f0 g0. +trivial. + +intros hf. +exists (fun (x:pow A) (y:B) => F) (fun (x:pow B) (y:A) => F). +intros; elim hf; auto. +Qed. + + +(** The paradoxical set *) +Definition U := forall P:Prop, pow P. + +(** Bijection between [U] and [(pow U)] *) +Definition f (u:U) : pow U := u U. + +Definition g (h:pow U) : U := + fun X => let lX := j2 (L1 X U) in let rU := i2 (L1 U U) in lX (rU h). + +(** We deduce that the powerset of [U] is a retract of [U]. + This lemma is stated in Berardi's article, but is not used + afterwards. *) +Lemma retract_pow_U_U : retract (pow U) U. +Proof. +exists g f. +intro a. +unfold f, g in |- *; simpl in |- *. +apply AC. +exists (fun x:pow U => x) (fun x:pow U => x). +trivial. +Qed. + +(** Encoding of Russel's paradox *) + +(** The boolean negation. *) +Definition Not_b (b:Bool) := IFProp (b = T) F T. + +(** the set of elements not belonging to itself *) +Definition R : U := g (fun u:U => Not_b (u U u)). + + +Lemma not_has_fixpoint : R R = Not_b (R R). +Proof. +unfold R at 1 in |- *. +unfold g in |- *. +rewrite AC with (r := L1 U U) (a := fun u:U => Not_b (u U u)). +trivial. +exists (fun x:pow U => x) (fun x:pow U => x); trivial. +Qed. + + +Theorem classical_proof_irrelevence : T = F. +Proof. +generalize not_has_fixpoint. +unfold Not_b in |- *. +apply AC_IF. +intros is_true is_false. +elim is_true; elim is_false; trivial. + +intros not_true is_true. +elim not_true; trivial. +Qed. + +End Berardis_paradox. \ No newline at end of file -- cgit v1.2.3