3 ms·

This is all true. It shows that no effectively computable set of axioms can prove all "true" computable functions computable (or in less metaphysical language,

This is all true. It shows that no effectively computable set of axioms can prove all "true" computable functions computable (or in less metaphysical language, that there are always functions we can show to be computable from "outside" our logical system, i.e. metalogically, while not being able to show it within that system). It's basically just a different variant of the incompleteness theorem. And another way to put it is that the set of computable functions is not recursively enumerable, and by extension, neither is the set of real numbers. But just because this set is not recursively enumerable, it doesn't mean that we can't talk about it and prove theorems about it, and not even a constructivist such as Bishop would go so far. He wouldn't even be able to define the real numbers if he did because there is no way of enumerating all the sequences that satisfy his definition of a real number. Your proposed definition of the set of real numbers (that kind of encode a proof of their own existence) is IMHO at odds with how constructivists themselves define them and IMHO also a totally unworkable definition for real analysis. Maybe there is some oddball mathematical framework that does what you want, but I'd certainly never want to work in a framework which doesn't even allow me to write down theorems of the form "for every decidable language, ..." just because I can't enumerate all the decidable languages, and similar.

btilly 3y ago
I agree that most constructivists define things differently than this. I brought up this example in https://news.ycombinator.com/item?id=37425642 https://news.ycombinator.com/item?id=37425642 to demonstrate that you were wrong in https://news.ycombinator.com/item?id=37423933 https://news.ycombinator.com/item?id=37423933 to claim that Cantor's argument necessarily must work constructively. It works in some constructive systems, and not in others. 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 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 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?
- Tainnor 3y ago
  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.
  - btilly 3y ago
    That's called moving the goalposts. 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-J-Groszek-7375828 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!
    - deleted 3y ago
      [deleted]

btilly 3y ago

I agree that most constructivists define things differently than this. I brought up this example in https://news.ycombinator.com/item?id=37425642 https://news.ycombinator.com/item?id=37425642 to demonstrate that you were wrong in https://news.ycombinator.com/item?id=37423933 https://news.ycombinator.com/item?id=37423933 to claim that Cantor's argument necessarily must work constructively. It works in some constructive systems, and not in others. 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 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 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?

Tainnor 3y ago
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.
- btilly 3y ago
  That's called moving the goalposts. 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-J-Groszek-7375828 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!
  - deleted 3y ago
    [deleted]