The diagonal argument was one of the most mind blowing moments of my maths degree
I feel that Cantor's theories are much the same way. They have severe logical shortcomings, which were highlighted over 100 years ago by the superior logician Skolem; namely that you can construct an uncountable set out of any countable set, and that every so-called uncountable set has a perfectly isomorphic countable model. Further, the diagonalization argument only works in the limit, with very generous use of ". . .", and the finitists have put together a number of very compelling arguments against it. People claim that Cantor's set theory might be a good foundation for mathematics, but it is at best a foundation made of sand. As with the nanotube, I feel that many researchers have spent countless hours -- millions, perhaps -- following an intellectual/scientific trend, and nothing good has come of it.
You are arguing that the ground moves to perfectly fit the shape of a puddle.
Zermelo was one of the first to reference "Cantor's theorem" in his papers.
HoL not having traditional NOT is an example.
Even in FoL, Peano arithmetic uses the SoL induction to be usable.
There is no free lunch.
Cantor's "diagonalization proof" showed that.
Turing extended to the computable numbers K, which can be conceptualized as a number where you can write a f(n) that returns the nth digit in a number.
The reals numbers are un-computable almost everywhere, this property holds for all real numbers in a set except a subset of measure zero, the computable reals K which is Aleph Zero, a countable infinity.
The set of computable reals is only as big as N, and can be mapped to N.
It is not 'non-standard numbers' that are inaccessible, it is most of the real line is inaccessible to any algorithm.
Note the following section for the first part.
"Non-Absoluteness of Truth in Second-Order Logic"
https://plato.stanford.edu/entries/logic-higher-order/#NonAb...
For example, why would one be able to create the diagonal set (those indices of the power set elements that do not contain that index as an element) and the enumeration of the power set (i.e. the entire list of possible sets of numbers) at the same time? The theorem proves that an enumeration of the power set cannot be made. Perhaps some sets cannot be constructed at will just by writing down its properties either?
In computer land, one would quickly run into self-referential problems when constructing sets like these. For mathematics of this kind, most people agree that this is all fine, and one can derive interesting things from it. But one can also reject the approach and still do some elementary fun stuff.
Then again, I might be completely misunderstanding all of this, and I love to be corrected.
Edit: wording
[1] Or any other theory of first-order logic.
[2] This is explained in more detail in Stewart Shapiro's book "Foundation without Foundationalism" p. 114f.
I feel like that would be a consequence of the axiom of choice.
On the other hand, the main advantage of second (and higher) order logic is that it allows for "categorical" theories. A theory, like second-order Peano arithmetic, is categorical when it only has one model up to isomorphism. For second-order PA this model is the natural numbers. First-order logic doesn't allow categorical theories, so the axiom of first-order PA can't rule out the existence of weird non-standard numbers. Categoricity of a theory means that the axioms of the theory "define" ("pin down") some model. First-order theories can't do that.
So naturally, first-order ZFC isn't categorical. It even allows for countable and uncountable models. It's interpretation (model) is highly indeterminate. However, second-order ZFC (unlike, say, second-order PA or second-order analysis) is also not categorical. It doesn't have a countable model anymore, but it is still has many non-isomorphic models. (Though I think it has some weaker property which means that it is at least "more categorical" in some sense.)
So second-order ZFC doesn't give us the main advantage that second-order logic allows (the possibility of categorical theories), while also not having the complete proof system of first-order logic.
However, we could simply not use ZFC at all and only use second (or rather: higher) order logic. Higher-order logic is powerful on its own to (often categorically) formalize mathematical theories, like PA, without the need of any set theory. Instead of sets we have properties ("being a real number" instead of the set of real numbers), relations, properties of properties etc.
Formal proof checkers like Isabelle actually use higher-order logic instead of first-order ZFC as a basis.
There is also some argument to be made that categoricity is more important than completeness, since completeness of a proof system turns out to be not a plausible property anymore once self-referential statements, like the Gödel sentence, get involved. But that would lead me too far afield, and it isn't the standard opinion, which favors completeness over categoricity.
This is simply false, as I already explained.
> and every model of ZFC will have a set that the model believes to be uncountable.
That is something else. (And I wouldn't use the nebulous term "believes" here, it's just that the model lacks an object which maps A to P.)
> It doesn't matter than the metatheory might believe that model to be countable (why should the metatheory have the correct notion of what it means to be countable anyway?).
"The meta theory" here is simply sentences expressed in natural language, or beliefs held by people expressing those sentences. It is the language in terms of which everything formal is ultimately defined. It's the only thing that ultimately matters.
> Then you said “Cantor's theorem stating that there is no mapping f from A onto P merely means that the mapping f itself can't exist inside a model of ZFC”. Which is literally identical to saying “under ZFC, there are uncountable sets”.
No, it only means that ZFC can't contain a function f from A to P in its model, which doesn't make P uncountable. (Things can be true even if the theory itself can't express them. E.g. Gödel's second incompleteness theorem says that a theory can't prove its own consistency, but that doesn't mean that the theory is inconsistent.)
I recommend you pick up a book on ZFC if you are interested in understanding set theory. I found Enderton’s “Elements of Set Theory” to be a really good introductory text.
I'm sorry but this is just wrong. Since you seem to like Shapiro's book more than traditional set theory books let me quote from page 144 that the existence of an uncountable set is a theorem of ZFC: "Let C be the statement of Cantor's theorem. It entails that the powerset of the collection of finite ordinals is not countable. Since C is a theorem of first-order ZFC..."
Also this is not how the metatheory is understood in mathematics, not even in Shapiro's book, who dedicates two whole chapters to the metatheory
You didn't finish reading the quote. It continues:
> "... Since C is a theorem of first-order ZFC, m ⊨ C, but, as just stated, m is itself countable and so are its elements. This, again, is the so-called Skolem paradox."
That is, he was making an (informal) contradictory statement in order to illustrate the paradox. But there is actually no contradiction (otherwise ZFC would have been proven inconsistent), so we already know the statement of the paradox must have been inaccurate. He then goes on to explain where the inaccuracy was. It turns out that it was mainly in the mistaken, but common, assumption that the "powerset axiom" implies the existence of a powerset:
> [The powerset axiom] is supposed[!] to assert the existence of the set of all subsets of each set. But the variables (like all first-order variables) range over the elements of the model. So the powerset axiom only guarantees the existence of a set of all subsets of (say) ω that are in the model. The subsets of ω that are 'guaranteed by the axioms' to exist in a given model m are those that are first-order m-definable, and only those. In some cases there are only countably many of them.
As I explained in a previous comment, you can't say in first-order logic "every possible combination of elements of this infinite set forms a set" (more precise expression of "all possible subsets exist"). ZFC's powerset axiom only states that all existing subsets are element of some set P, but it doesn't imply they exist in the first place. So it doesn't imply the existence of infinite powersets (finite powersets wouldn't require the axiom anyway). Indeed, only those subsets are implied to exist that are implied by the other axioms, which isn't very many. (See the Löwenheim-Skolem theorem.)
And Cantors theorem only states that inside the model no function f (which would be just another set) exists that maps A to its supposed powerset P, even if both A and P are countable. So there no contradiction between Cantor's theorem and the countability of P in ZFC.
> Also this is not how the metatheory is understood in mathematics, not even in Shapiro's book, who dedicates two whole chapters to the metatheory
See this (well-known) quote on page 254 where he talks about the metatheory of second-order logic:
> The language of set theory is employed, without apology, and no anti-realist interpretation or reduction its envisaged. Indeed, no explicit interpretation is envisaged at all. There is no perspective outside this language from which to discuss its interpretations, or its models, or at least none is contemplated. The set-theoretic universal quantifier reads 'for all sets' and the existential quantifier reads 'there is a set'. Thus sets are in the ontology of the background theory. If asked 'which sets?' or 'how many?', there is only one answer: 'all of them'. This is what it is to take the language literally.
Alternatively, one could already take the axioms of second-order logic as "rock bottom", insofar they are grounded in natural language (which he also offers arguments for). In any case, using other formal theories as a tower of meta- and meta-meta-theories only leads to an infinite regress. Everything bottoms out in natural language. Normal mathematicians don't bother with formal languages in the first place, it's only logicians which make this excursion, but even they resort to natural language on the (meta) meta level.
There are interesting physical differences between quantum systems whose spectra are discrete (countably infinite eigenvalues) and continuous (uncountably infinite spectrum) and even combinations of both.
You don't know that. Spacetime may be quantized.
Actually, doesn't the notion of Planck length / Planck time already suggest that shorter distances have no physical meaning?
Nope, we have absolutely no evidence of that. Space-time may be either discrete or continuous. Based on our current understanding we have no evidence either way.