Can the generalized continuum hypothesis be disguised as a principle of logic?

Question

A cool way to formulate the axiom of choice (AC) is:

AC. For all sets $X$ and $Y$ and all predicates $P : X \times Y \rightarrow \rm\{True,False\}$, we have: $$(\forall x:X)(\exists y:Y)P(x,y) \rightarrow (\exists f : X \rightarrow Y)(\forall x:X)P(x,f(x))$$

Note the that converse is a theorem of ZF, modulo certain notational issues.

Anyway, what I find cool about formulating AC this way is that, okay, maybe its just me, but this formulation really "feels" like a principle of logic, as opposed to set theory. I mean, its just saying that we can commute an existential quantifier $(\exists y:Y)$ left across a universal quantifier $(\forall x:X)$ so long as we replace existential quantification over the elements of $Y$ with existential quantification over functions from $X$ into $Y.$ And sure, "function" is a set-theoretic concept; nonetheless, this feels very logical to me.

Question. Can the generalized continuum hypothesis also be formulated in a similar way, so that it too feels like a principle of logic?

Obviously this is pretty subjective, so lets lay down some ground rules.

1. The axiom should be equivalent to the generalized continuum hypothesis over ZFC.
2. It has to be two lines or fewer. No sprawling 4-page axioms, thank you very much!
3. Use of concepts like "function" and "predicate" is good and desirable.
4. Use of the concepts injection/surjection/bijection is moderately frowned upon.
5. Completely disallowed: use of cardinality and/or cardinal numbers; use of ordinal numbers; mentioning $\mathbb{N}$ or $\omega$ or the words "finite" or "infinite."

Answer 1

Certainly, the Continuum Hypothesis (simple or generalised) can be formulated in the language of pure second-order logic.

This is done explicitly in Stewart Shapiro's wonderful book on second-order logic, Foundations without Foundationalism: see pp. 105-106.

The full story is a bit too long to give here. But as a taster, you start off by essentially using Dedekind's definition of infinity, so that you define Inf(X), for $X$ a property, as

$$\exists f[\forall x\forall y(fx = fy \to x = y) \land \forall x(Xx \to Xfx) \land \exists y(Xy \land \forall x(Xx \to fx \neq y))].$$

Ok, the first clause of this imposes the requirement that $f$ is injective: but we have done this in purely logical terms, so that shouldn't look worrying to someone looking for logical principles!

Now we can carry on through a sequence of such definitions until you get to a sentence, still in the pure language of second-order logic, which formulates CH. Then with a bit more work we can go on to construct a sentence which expresses GCH. Further details are spelt out in Shapiro.

However, as Asaf rightly points out below, it is one thing to say that a statement can be formulated in the language of pure second-order logic, and another thing to say that it is a logical principle. And it is indeed a nice question what that actually means. Still, we can say this much: as Shapiro notes, on a standard account of the semantics of full second-order logic it turns out that either CH or NCH (a certain natural formulation of the falsity of the continuum hypothesis) must be a logical truth of full second-order logic. But here's the snag: we don't know which!