[cubefox]

There is no bijection (surjection, to be more general) from A to P inside your ZFC model even if both A and P are assumed to be countable. The bijection we talk about here would be just another object inside the model. So you can't infer from the lack of such an object that P is uncountable.

[openasocket]

Yeah, Cantors theorem is a theorem written in the language of ZFC set theory. In other axiom systems it may not be true. But you can also say that about literally every theorem beyond, like, modus ponens. Is that the point you are trying to make?

[cubefox]

The point is simply that it doesn't imply the existence of uncountable sets in ZFC. Modus ponens is different. The semantic entailment relation ⊨ between (P→Q, P) and Q is valid iff there is no model such that the former is true and the latter is false. Which is a sentence in plain English. It doesn't require the existence of some object that is mapping the premises to the conclusion inside the model. It doesn't even require the existence of a syntactic deduction rule (⊢) that tells you from (P→Q, P) to infer Q.

[ginnungagap]

It is a theorem of ZFC that uncountable sets exist and every model of ZFC will have a set that the model believes to be uncountable. 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?).

[cubefox]

> It is a theorem of ZFC that uncountable sets exist

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.

[openasocket]

It is absolutely not false! This is taught in every undergraduate set theory course. Please point to me the step in the above proof where there is an error.

[cubefox]

Certainly not in every undergraduate class, though I don't doubt that the subtleties around these issues may often be taught wrong. I already did point you to the errors, and I included the reference to Shapiro's book.

[ginnungagap]

> This is simply false, as I already explained.

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

[cubefox]

> 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..."

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.