The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Thu, Nov 8, 2012 at 2:45 PM, Jonas Oberhauser 
<s9joober AT gmail.com>
 wrote:
> 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

OK, I see your point.  And looking back at my argument, it seems to be
pointing more to ~(f <> g) than to f = g...

I guess what I was trying to say on your example is that I don't find
inequality to be quite as subject to interpretation as equality.
Proofs of inequality x <> y often essentially boil down to exhibiting
a condition P such that P x /\ ~ P y, which should be a
non-controversial style of argument.
-- 
Daniel Schepler