[openasocket]

I’m uncertain what your point is. Like I said, in ZFC, there is no bijection from A to its power set. I don’t think anything you’ve stated contradicts that. Are there alternative axiom systems in which you can construct such a bijection?

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

[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