Can uncountable sets be proved to exist in this variant of ZFC with definability restrictions?

Question

If we restrict all parameters in the set building axioms of $\sf ZFC$ to definable sets, would the celebrated Cantor's theorem still apply? Can existence of uncountable sets be proven at all?

The set building axioms of $\sf ZFC$ are the axioms of: pairing, union, powerset, Separation and Replacement\Collection.

To clarify what I mean by this restriction, the idea is that the parameters to be definable by formulas having a single free variable, take the axiom of pairing for example, this would turn into the following scheme:

Pairing: if $\varphi; \psi$ are formulas in which "$x$" only occurs free, and that do not have a free variable other than "$x$"; then:

$\forall a \forall b \, \bigl(a=\{x \mid \varphi\} \land b=\{x \mid \psi \} \\\to \exists c \forall y \, (y \in c \leftrightarrow y=a \lor y=b )\bigr)$

In other words, is it consistent to add an axiom that all sets are countable?

Clarification: by parameters in the abovementioned set building axioms, I mean the variables quantified before [i.e., on the left of] the asserted to exist set.

One more remark, I noticed that there can be many versions of this question by easing those restrictions from some of the mentioned axioms. One version is to just remove that restriction from pairing, or just remove it from powerset axiom, or actually just remove it from both pairing and powerset axioms. We can also have similar partial easing with any of union or powerset, or any two of pairing, union, and powerset.

I think most interesting would be to limit definability of parameters to axioms of Set Union, Separation and Replacement\Collection.

An even less restrictive version is to just limit the condition of definability of parameters (in the above sense) to the instances of Separation and Replacement\Collection.

Answer 1

Parameter-free ZFC is equivalent to ZFC. See

• Ralf Schindler, Philipp Schlicht, ZFC without parameters.

Therefore, in parameter-free ZFC we can prove all the same theorems as in ZFC, including the existence of uncountable sets.

[Update. The OP evidently intends the question with a special understanding of the term "parameter", different from the usual meaning of that term, which makes this answer less relevant for the intended question.]

Answer 2

The proof below is due to George Boolos, and appears in his article Constructing Cantorian Counterexamples, Journal of Philosophical Logic, Vol. 26, No. 3 (Jun., 1997), pp. 237-23.  

Boolos gives an explicit proof that there cannot exist a one-to-one function from the powerset of a set into the same set.

A similar proof appears as Corollary 1.3 of the following paper (a copy of which is available here).

Akihiro Kanamori, David Pincus, Does GCH imply AC locally?, in Paul Erdős and his mathematics, II (Budapest, 1999)", Bolyai Soc. Math. Stud., 11, János Bolyai Math. Soc., Budapest, (2002), 413–426.

Suppose $f: \mathcal{P}(A)\rightarrow A$. We want to explicitly define subsets $B$ and $C$ of $A$ such that $B\ne C$ but $f(B) = f(C)$.

For any binary relation $r$, let $r_{x} = \{y: (y,x)\in r \land y\neq x \}$, and let $\mathrm{field}(r)$ be the field of $r$, i.e., the set of objects that appear as the first or second coordinate of an ordered pair in $r$.

Call a relation $r$ to be good iff $r$ is a reflexive well-ordering of a subset of $A$ and for every $x$ in $\mathrm{field}(r)$, $f(r_{x}) = x$. Let $R$ be the union of all good $r$.

If $r$ and $r'$ are good, then one of $r$ and $r'$ is an initial segment of the other; therefore $R$ is itself good. Let $C = \mathrm{field}(R)$. For $C \subseteq A$, Let $x = f(C)$, and let $B = R_{x}$.

Note that $C$, $x$, and $B$ are all explicitly defined from $f$.

If $x \notin C$, then $R \cup \{(y, x): y \in C \lor y = x \}$ is good, and therefore $x \in C$. So $x\in C$.

Since $x \not\in \{y: yRx \land y\neq x\} = B$, $B\neq C$.

Since $R$ is good, $x = f(R_{x}) = f (B)$. But $x = f (C)$. Thus $f$ is not one-one.

As noted by Boolos, since $R_{x} \subseteq \mathrm{field}(R)$, the above proof shows a nontrivial strengthening of the nonexistence of an injection of the powerset of $A$ into $A$, namely:

Theorem. If $f: \mathcal{P}(A) \rightarrow A$, then there are subsets $B$ and $C$ of $A$ such that $B\subsetneq C$ and $f (B) = f (C)$.