Library Coq.Logic.Berardi
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} }
Excluded middle
Conditional on any proposition.
Definition IFProp (P B:Prop) (e1 e2:P) :=
match EM B with
| or_introl _ => e1
| or_intror _ => e2
end.
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).
forall (P B:Prop) (e1 e2:P) (Q:P -> Prop),
(B -> Q e1) -> (~ B -> Q e2) -> Q (IFProp B e1 e2).
We assume a type with two elements. They play the role of booleans.
The main theorem under the current assumptions is that T=F
The powerset operator
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}.
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:
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).
The paradoxical set
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).
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.
Encoding of Russel's paradox
The boolean negation.
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).
Theorem classical_proof_irrelevance : T = F.
#[deprecated(since = "8.8", note = "Use classical_proof_irrelevance instead.")]
Notation classical_proof_irrelevence := classical_proof_irrelevance.
End Berardis_paradox.
Lemma not_has_fixpoint : R R = Not_b (R R).
Theorem classical_proof_irrelevance : T = F.
#[deprecated(since = "8.8", note = "Use classical_proof_irrelevance instead.")]
Notation classical_proof_irrelevence := classical_proof_irrelevance.
End Berardis_paradox.