[cubefox]

You can't prove such a thing in ZFC [1]. ZFC's "power set axiom" is a misnomer. It doesn't imply the existence of infinite power sets. It just says if any set S exists and is a subset of an infinite set A, then S is element of a set P (the supposed "power set"). But the axiom doesn't imply the existence of "all" subsets of A. There is no way for first-order logic to state "every possible combination of elements of A forms a set". And 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. [2]

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

[4death4]

> But the axiom doesn't imply the existence of "all" subsets of A.

I feel like that would be a consequence of the axiom of choice.

[cubefox]

At the moment I don't remember enough of the axiom of choice to comment on it in detail, but we can infer from the Downward Löwenheim-Skolem theorem (roughly, every first-order theory, including ZFC, has a countable model) that the Choice axiom can't imply uncountable sets.

[4death4]

Admittedly I know nothing about the theorem you’re referring to, but is there a compelling reason to limit ourselves to first-order logic?

[cubefox]

The main reason people like first-order logic is Gödel's completeness theorem. It says that for first-order logic there is a proof system such that it proves a sentence if and only if it is true in every model. That is, the proof system is both sound and complete. This doesn't work for second or higher order logic. If we want a second-order proof system to be sound (proves no false things), it must be incomplete, i.e. not prove some true statements.

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.

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