[Haskell-cafe] Re: Re: Re[2]: Wikipedia on first-class object

[Albert Y. C. Lai]

Ben Franksen wrote:
> Of course this doesn't prove that humans can, in
> principle, decide equality for any pair of functions. But neither has the
> opposite been proved.

Premise: The human should still give the reasoning behind his/her 
decisions. The reasoning should be within a proof system chosen a 
priori, i.e., chosen before you answer any equality questions, uniform 
over all such questions, not amended ad hoc as you encounter new questions.

Then by incompleteness some answers are not supported by any reasoning 
within the chosen proof system. It is not that some proof is out there 
and the prover is too limited to find it. It is that among all valid 
proofs, none says yes and none says no. This is independent of the wit 
of the prover.

Now, you can refuse the premise, and I outline my reply.

(A) The human should still give the reasoning behind his/her decisions.

If you don't give the reasoning, well, to quote famous words, that is 
theology, that is not mathematics.

(Can computers do theology? I don't think anyone cares. We have enough 
human theologians as is, even in this mailing list, even in this thread, 
theologians attributing near-divine power of induction and deduction to 
humans. No, we don't need computers to become additional theologians.)

(B) The reasoning should be within a proof system chosen a priori.

Mathematicians do change their rules. It is part of their job: to 
explore what happens if you assume something more, or something less. 
But every time they do so, they have to convince their peers of the merit.

(If you don't have to convince of merits, well, even a computer can 
randomly change rules.)

But if you do this, you deviate from the original subject matter. The 
original subject matter is: can we decide equality questions? The 
deviation is: can we decide quality questions? It is really a different 
question. You should first use quality judgement to fix a proof system, 
then use the proof system to decide equality questions.

Can computers be programmed to decide quality questions? That hasn't 
been ruled out.