I'm not arguing for attempting to work in such constructive systems. Merely pointing out that they exist. And their existence is a limitation on what diagonalization can prove a priori.
Also look at what you said in https://news.ycombinator.com/item?id=37427973. Now can you see that my point is not nonsense? Diagonalization really does add a layer of self-reference. And the fact that it does is why it doesn't work in the system that I described.
This also explains the point that I was making in https://news.ycombinator.com/item?id=37428468. Your Coq proof was fine for what it proved. But it was not looking at the key piece of my example. Which is the fact that the functions are not necessarily total functions. They are merely functions which we have a specific reason for believing that they might be total. Namely a proof from a particular set of axioms. And my whole point was that the diagonalized function in general doesn't have equivalent evidence of being total. Which is a point of complexity that your Coq proof did not address.
Are you still so certain that I don't know what I'm talking about?
Please give a reference to any textbook or paper that defines real numbers in such a purposefully useless way as you do it, and I'll reconsider my position. Otherwise I think you're just playing semantic games, trying to redefine well-known terms - in which case you should not be surprised that people don't understand you.
Now that you personally know how to trace the reasoning to see that my counterexample really was a counterexample, you'll only accept it as a counterexample if you see it in published research?
This is something that I worked through myself back in grad school back in the last millennium. https://www.researchgate.net/scientific-contributions/Marcia... gave me a number of leading hints, and confirmed my reasoning to me. In particular she was the one who commented, "A lot of people miss the importance of the fact that an axiom system proving that it proves something doesn't mean that it proves something." From her reactions at the time, I'm pretty sure she thought it was trivially obvious. And may well have known of prior research.
So no, I don't have published research using this formulation. Nor is it reasonable for you to demand published research to verify something learned through oral communication decades ago, which should be obvious to anyone in the field.
Doubly so given that my first description of the counterexample came with enough specific details that you SHOULD have been able to figure it out yourself. I not only told you what definition would create the problem. I also said why, and gave you an outline of the construction from which you could produce the proof!
I'm not arguing for attempting to work in such constructive systems. Merely pointing out that they exist. And their existence is a limitation on what diagonalization can prove a priori.
Also look at what you said in https://news.ycombinator.com/item?id=37427973. Now can you see that my point is not nonsense? Diagonalization really does add a layer of self-reference. And the fact that it does is why it doesn't work in the system that I described.
This also explains the point that I was making in https://news.ycombinator.com/item?id=37428468. Your Coq proof was fine for what it proved. But it was not looking at the key piece of my example. Which is the fact that the functions are not necessarily total functions. They are merely functions which we have a specific reason for believing that they might be total. Namely a proof from a particular set of axioms. And my whole point was that the diagonalized function in general doesn't have equivalent evidence of being total. Which is a point of complexity that your Coq proof did not address.
Are you still so certain that I don't know what I'm talking about?