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.