The Coq mailing list

[Jonas Oberhauser <s9joober AT gmail.com>]

Am 08.11.2012 23:03, schrieb Daniel Schepler:
> 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.

Maybe I was imprecise. Within the example, I was not arguing about any 
axioms at all. I was talking about meaning. What is the meaning of the 
proposition from above? As far as I can tell, we are not making any 
claims about the existence of a function. We are making claims about 
procedures.

As soon as you assume axioms, the meaning might change. Excluded middle 
is another good example. "P \/ ~ P", to me, means we can prove P or we 
can refute P. If we can prove this (by either giving a proof of P or 
refuting P), we can establish this claim. Once we assume excluded 
middle, the meaning of "P \/ ~P" somehow changes to "P is true or is 
false" because certainly we do not have a proof term for every 
proposition or its negation (like functional extensionality, which I 
think is independet of XM).

So when we assume axioms, we need to make sure we understand that we 
change the meaning of things. Otherwise, insanity ensues. Sometimes it 
is not clear in what way the meaning changes.

I have no reason to believe that two procedures that compute the same 
function are equal. I could argue, as you say, that I can not 
distinguish them by the means that Coq gives to me. Maybe that is enough 
to claim that they are leibniz-equal in Coq, but then again, as with the 
example from before, how much impact does a proof of "f = g" then have 
in the real world? I have proven they are equal, but, you know, not 
really? Only in the countable Coq-world? I don't know about this...

As long as the fact that two procedures compute the same function is 
enough to clear the proof obligations, I would not assume such axioms. 
Maybe for some proof goal we have to, maybe it makes things easier. But 
still I have a bad feeling tingling down my spine.

Kind regards, Jonas