In particular, you have made sufficient assumptions to prove that almost all real numbers that exist can never be specified in any possible finite description. In what sense do they exist? You also wind up with weirder things. Such as well-specified finite problems that provably have a polynomial time algorithm to solve...but for which it is impossible to find or verify that algorithm, or put an upper bound on the constants in the algorithm. In what sense does that algorithm exist, and is finite?
Does that sound impossible? An example of an open problem whose algorithm may have those characteristics is an algorithm to decide which graphs can be drawn on a torus without any self-crossings.
If our notion of "exists" is "constructable", all possible mathematical things can fit inside of a countable universe. No set can have more than that.
Errr, I'm just assuming the axioms of ZFC. That's literally all I'm doing.
> In what sense do [numbers that can't be finitely specified] exist?
In the sense that we can describe rules that lead to them, and describe how to work with them.
I understand that you're trying to tie the notion of "existence" to constructability, and that's fine. That's one way to play the game. Another is to use ZFC and be fine with "weird, unintuitive to laypeople" outcomes. Both are interesting and valid things to do IMO. I'm just not sure why one is obviously "better" or "more real" or something. At the end, it's all just coming up with rules and figuring out what comes out of them.
On the other hand, I think it's really cool to teach laypeople about things like "sizes of infinities", etc. They are deep math concepts that can be taught with relatively simple analogies that most people understand, and they're interesting things to know. I know that I personally loved learning about them as a kid, before I had almost any knowledge of math - it's one of the reasons that while I initially didn't connect with other areas of math, I found set theory delightful as a kid.
I just feel like if you need to first walk people through a bunch of philosophical back and forth on constructionism, you'll never get to the fun stuff.
ZFC (and its underlying classical logic) is precisely the problem here though
I'm saying that to go from the uncountability of the reals to the idea that this implies that the infinity of the reals is larger, requires making some important philosophical assumptions. Constructivism demonstrates that uncountable need not mean more.
On the algorithm example, you could have asked what I was referring to.
The result that I was referencing follows from the https://en.wikipedia.org/wiki/Robertson%E2%80%93Seymour_theo.... The theorem says that any class of finite graphs which is closed under graph minors, must be completely characterized by a finite set of forbidden minors. Given that set of forbidden minors, we can construct a polynomial time test for membership in the class - just test each forbidden minor in turn.
The problem is that the theorem is nonconstructive. While it classically proves that the set exists, it provides no way to find it. Worse yet, it can be proven that in general there is no way to find or verify the minimal solution. Or even to provide an upper bound on the number of forbidden minors that will be required.
This need not hold in special cases. For example planar graphs are characterized by 2 forbidden minors.
For the toroidal graphs, as https://en.wikipedia.org/wiki/Toroidal_graph will verify, the list of known forbidden minors currently has 17,523 graphs. We have no idea how many more there will be. Nor do we have any reason to believe that it is possible to verify the complete list in ZFC. Therefore the polynomial time algorithm that Robinson-Seymour says must exist, does not seem to exist in any meaningful and useful way. Such as, for example, being findable or provably correct from ZFC.
In the sense that all statements of non-constructive "existence" are made, viz. "you can't prove that they don't exist in the general case", so you are allowed to work under the stronger assumption that they also exist constructively, without any contradiction resulting. That can certainly be useful in some applications.
But the fact that such systems don't create contradictions emphatically *DOES NOT* demonstrate the constructive existence of such an oracle. Doubly not given that in various usual constructivist systems, it is easily provable that nothing that exists can serve as such an oracle.
If the only questions you accept as meaningful are the decidable ones, then you can trust its answers for all the questions you accept as meaningful and for which it has answers.
Also, “provable that nothing that exists can serve as such an oracle” seems pretty presumptive about what things can exist? Shouldn’t that be more like, “nothing which can be given in such-and-such way (essentially, no computable procedure) can be such an oracle”?
Why treat it as axiomatic that nothing that isn’t Turing-computable can exist? It seems unlikely that any finite physical object can compute any deterministic non-Turing-computable function (because it seems like state spaces for bounded regions of space have bounded dimension), but that’s not something that should be a priori, I think.
I guess it wouldn’t really be verifiable if such a machine did exist, because we would have no way to confirm that it never errs? Ah, wait, no, maybe using the MIP* = RE result, maybe we could in principle use that to test it?
Of course, but it shows that you can assume that such an oracle exists whenever you are working under additional conditions where the existence of such a "special case" oracle makes sense to you, even though you can't show its existence in the general case. This outlook generalizes to all non-constructive existence statements (and disjunctive statements, as appropriate). It's emphatically not the same as constructive existence, but it can nonetheless be useful.
John Horton Conway:
> It's a funny thing that happens with mathematicians. What's the ontology of mathematical things? How do they exist? In what sense do they exist? There's no doubt that they do exist but you can't poke and prod them except by thinking about them. It's quite astonishing and I still don't understand it, having been a mathematician all my life. How can things be there without actually being there? There's no doubt that 2 is there or 3 or the square root of omega. They're very real things. I still don't know the sense in which mathematical objects exist, but they do. Of course, it's hard to say in what sense a cat is out there, too, but we know it is, very definitely. Cats have a stubborn reality but maybe numbers are stubborner still. You can't push a cat in a direction it doesn't want to go. You can't do it with a number either.
