Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <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)         *)
(************************************************************************)
This file formalizes Berardi's paradox which says that in the calculus of constructions, excluded middle (EM) and axiom of choice (AC) imply proof irrelevance (PI). Here, the axiom of choice is not necessary because of the use of inductive types. 
@article{Barbanera-Berardi:JFP96,
   author    = {F. Barbanera and S. Berardi},
   title     = {Proof-irrelevance out of Excluded-middle and Choice
                in the Calculus of Constructions},
   journal   = {Journal of Functional Programming},
   year      = {1996},
   volume    = {6},
   number    = {3},
   pages     = {519-525}
}

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. 
EM:forall P : Prop, P \/ ~ P
forall (P B : Prop) (e1 e2 : P) (Q : P -> Prop),
(B -> Q e1) -> (~ B -> Q e2) -> Q (IFProp B e1 e2)


EM:forall P : Prop, P \/ ~ P
forall (P B : Prop) (e1 e2 : P) (Q : P -> Prop),
(B -> Q e1) -> (~ B -> Q e2) -> Q (IFProp B e1 e2)


EM:forall P0 : Prop, P0 \/ ~ P0
P, B:Prop
e1, e2:P
Q:P -> Prop
p1:B -> Q e1
p2:~ B -> Q e2
Q (IFProp B e1 e2)


EM:forall P0 : Prop, P0 \/ ~ P0
P, B:Prop
e1, e2:P
Q:P -> Prop
p1:B -> Q e1
p2:~ B -> Q e2
Q
  match EM B with
  | or_introl _ => e1
  | or_intror _ => e2
  end

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: 
EM:forall P : Prop, P \/ ~ P
Bool:Prop
T, F:Bool
A, B:Prop
forall r : retract_cond,
retract -> forall a : A, j2 r (i2 r a) = a


EM:forall P : Prop, P \/ ~ P
Bool:Prop
T, F:Bool
A, B:Prop
forall r : retract_cond,
retract -> forall a : A, j2 r (i2 r a) = a
 
EM:forall P : Prop, P \/ ~ P
Bool:Prop
T, F:Bool
A, B:Prop
r:retract_cond
retract -> forall a : A, j2 r (i2 r a) = a
 exact (inv2 r). 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 intuitionistic logic). 
EM:forall P : Prop, P \/ ~ P
Bool:Prop
T, F:Bool
forall A B : Prop, retract_cond (pow A) (pow B)


EM:forall P : Prop, P \/ ~ P
Bool:Prop
T, F:Bool
forall A B : Prop, retract_cond (pow A) (pow B)


EM:forall P : Prop, P \/ ~ P
Bool:Prop
T, F:Bool
A, B:Prop
retract_cond (pow A) (pow B)


EM:forall P : Prop, P \/ ~ P
Bool:Prop
T, F:Bool
A, B:Prop
f0:pow A -> pow B
g0:pow B -> pow A
e:forall a : pow A, g0 (f0 a) = a
retract_cond (pow A) (pow B)
EM:forall P : Prop, P \/ ~ P
Bool:Prop
T, F:Bool
A, B:Prop
hf:~ retract (pow A) (pow B)
retract_cond (pow A) (pow B)


EM:forall P : Prop, P \/ ~ P
Bool:Prop
T, F:Bool
A, B:Prop
f0:pow A -> pow B
g0:pow B -> pow A
e:forall a : pow A, g0 (f0 a) = a
retract_cond (pow A) (pow B)
 exists f0 g0; trivial.

EM:forall P : Prop, P \/ ~ P
Bool:Prop
T, F:Bool
A, B:Prop
hf:~ retract (pow A) (pow B)
retract_cond (pow A) (pow B)
 exists (fun (x:pow A) (y:B) => F) (fun (x:pow B) (y:A) => F); intros;
    destruct 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. 
EM:forall P : Prop, P \/ ~ P
Bool:Prop
T, F:Bool
retract (pow U) U


EM:forall P : Prop, P \/ ~ P
Bool:Prop
T, F:Bool
retract (pow U) U


EM:forall P : Prop, P \/ ~ P
Bool:Prop
T, F:Bool
forall a : pow U, f (g a) = a


EM:forall P : Prop, P \/ ~ P
Bool:Prop
T, F:Bool
a:pow U
f (g a) = a


EM:forall P : Prop, P \/ ~ P
Bool:Prop
T, F:Bool
a:pow U
j2 (L1 U U) (i2 (L1 U U) a) = a


EM:forall P : Prop, P \/ ~ P
Bool:Prop
T, F:Bool
a:pow U
retract (pow U) (pow U)
 

EM:forall P : Prop, P \/ ~ P
Bool:Prop
T, F:Bool
a:pow U
forall a0 : pow U, a0 = a0

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)).



EM:forall P : Prop, P \/ ~ P
Bool:Prop
T, F:Bool
R R = Not_b (R R)


EM:forall P : Prop, P \/ ~ P
Bool:Prop
T, F:Bool
R R = Not_b (R R)


EM:forall P : Prop, P \/ ~ P
Bool:Prop
T, F:Bool
g (fun u : U => Not_b (u U u)) R = Not_b (R R)


EM:forall P : Prop, P \/ ~ P
Bool:Prop
T, F:Bool
j2 (L1 U U) (i2 (L1 U U) (fun u : U => Not_b (u U u)))
  R = Not_b (R R)


EM:forall P : Prop, P \/ ~ P
Bool:Prop
T, F:Bool
Not_b (R R) = Not_b (R R)
EM:forall P : Prop, P \/ ~ P
Bool:Prop
T, F:Bool
retract (pow U) (pow U)


EM:forall P : Prop, P \/ ~ P
Bool:Prop
T, F:Bool
Not_b (R R) = Not_b (R R)
 trivial.

EM:forall P : Prop, P \/ ~ P
Bool:Prop
T, F:Bool
retract (pow U) (pow U)
 
EM:forall P : Prop, P \/ ~ P
Bool:Prop
T, F:Bool
forall a : pow U, a = a

  trivial.
Qed.



EM:forall P : Prop, P \/ ~ P
Bool:Prop
T, F:Bool
T = F


EM:forall P : Prop, P \/ ~ P
Bool:Prop
T, F:Bool
T = F


EM:forall P : Prop, P \/ ~ P
Bool:Prop
T, F:Bool
R R = Not_b (R R) -> T = F


EM:forall P : Prop, P \/ ~ P
Bool:Prop
T, F:Bool
R R = IFProp (R R = T) F T -> T = F


EM:forall P : Prop, P \/ ~ P
Bool:Prop
T, F:Bool
R R = T -> R R = F -> T = F
EM:forall P : Prop, P \/ ~ P
Bool:Prop
T, F:Bool
R R <> T -> R R = T -> T = F


EM:forall P : Prop, P \/ ~ P
Bool:Prop
T, F:Bool
R R = T -> R R = F -> T = F
 
EM:forall P : Prop, P \/ ~ P
Bool:Prop
T, F:Bool
is_true:R R = T
is_false:R R = F
T = F

  elim is_true; elim is_false; trivial.


EM:forall P : Prop, P \/ ~ P
Bool:Prop
T, F:Bool
R R <> T -> R R = T -> T = F
 
EM:forall P : Prop, P \/ ~ P
Bool:Prop
T, F:Bool
not_true:R R <> T
is_true:R R = T
T = F

  elim not_true; trivial.
Qed.


Notation classical_proof_irrelevence := classical_proof_irrelevance (compat "8.8").

End Berardis_paradox.