The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Thu, Nov 8, 2012 at 1:15 PM, Jonas Oberhauser 
<s9joober AT gmail.com>
 wrote:
> One thing that has opened my eyes a little bit was this provable proposition
> that Smolka and CE Brown showed to me:
>
> Goal forall X, forall f : X -> (X -> Prop),  exists g, forall x, f x <> g.
>
> What does this mean? Does it mean that there are more "sets of X" than there
> are "elements of X"? Or does it just mean that there is no procedure (in the
> Coq-World) that gives every procedure in (X -> Prop) a unique object of X?
> Certainly you can only write down countably many procedures (or "sets") in
> Coq, but the number of sets of e.g. natural numbers is much larger.

I'm not sure exactly what you're trying to get at with this example.
Of course it's easy to prove this without axioms:

Definition same_set {X} (A B:X->Prop) : Prop :=
forall x:X, A x <-> B x.

Lemma Cantor_diag: forall {X} (f:X -> (X->Prop)),
  exists B:X->Prop, forall x:X, ~ same_set (f x) B.

But this is just a refinement of the statement that every
undergraduate math major learns.  And since it's also easy to prove
A=B -> same_set A B, so ~ same_set A B -> A <> B, your statement is an
easy corollary.

The way I tend to look at functional extensionality is: x=y is
equivalent to Leibniz equality, i.e. forall P, P x <-> P y or
equivalently forall P, P x -> P y.  The statement that functional
extensionality is consistent, to me, means that for propositions you
can build within Coq, there's no proposition which distinguishes f
from g if all their values are equal.  And adding functional
extensionality as an axiom is essentially a promise that you won't add
any other axioms or parameters, like a "function introspection on the
reduction" operation, which would allow you to distinguish for example
between fun n => n and fun n => n+0.
-- 
Daniel Schepler