By "Parameter free Zermelo" I mean a theory defined in the language of set theory that has exactly Zermelo set theory axioms except the axiom scheme of Separation which is replaced by parameter free separation scheme, the later is formally written as:

Parameter free separation scheme: if $\phi(y)$ is a formula in which only the symbol "$y$" occur free, then:

$\forall A \space \exists x \space \forall y \space (y \in x \iff y \in A \wedge \phi(y))$

is an axiom.

My question: is there a known result about provability of Cantor's theorem (that a set is strictly smaller than its power) in this parameter free Zermelo?

I personally think it is not provable and that Parameter free Zermelo is consistent with the axiom that all sets are countable? I tried to search for that result but I didn't see it mentioned anywhere.

  • 1
    $\begingroup$ At least in the case of ZF, it is an old theorem that Replacement without parameters is sufficient for proving full Replacement. I'm inclined to believe this is to be the case in Z with the Separation schema. Although this is just a semi-educated guess. $\endgroup$
    – Asaf Karagila
    Oct 28, 2016 at 15:48
  • 2
    $\begingroup$ A proof that "ZFC without parameters" (in particular: with the parameter-free versions of Replacement and Separation) implies "ZFC with parameters" (in particular: the full replacement axiom) can be found in Ralf Schindler's collection of notes and preprints: wwwmath.uni-muenster.de/u/rds/ZFC_without_parameters.pdf $\endgroup$
    – Goldstern
    Oct 29, 2016 at 0:22
  • 1
    $\begingroup$ @Azad, Cantor's theorem is among the central theorems in set theory and foundations; whether it can be proved if we get parameters out of Separation seemed to be interesting to me in its own right. I was a little bit surprised when I didn't see a clear reference to this issue. If parameter free Z doesn't prove Cantor's theorem, then what exactly is its consistency strength? $\endgroup$ Oct 29, 2016 at 4:05
  • 1
    $\begingroup$ @MortezaAzad I deleted my answer because it was wrong - I misread the question, and thought we were allowed to use $Y$ as a parameter. $\endgroup$ Oct 29, 2016 at 4:42
  • 1
    $\begingroup$ @Noah, I still see it an interesting answer! you could have written it as an answer to a 'RELATED' question that allows the symbol for the principal set (the set we are separating from) to be a parameter. Truly it is not the question I've asked but it is close to it. $\endgroup$ Oct 29, 2016 at 5:19

3 Answers 3


This is not an answer to the main question. However, the OP has asked that it remain up.

Call "almost parameter-free separation" the principle of separation where no parameters are allowed, except for a parameter for the set to which separation is being applied. Almost parameter-free separation, it turns out, is enough to prove Cantor's theorem.

Here's a proof that relies on Foundation:

Suppose $f$ is a map from $X$ to $\mathcal{P}(X)$; we want to show that $f$ is not surjective. We can't directly build the diagonal subset by applying separation to $X$, so instead consider the set $Y=X\cup\{f\}$. Note that there is exactly one $a\in Y$ satisfying the formula:

$(\Psi)\quad$"$a$ is a function with domain $Y\setminus a$"

(clearly there is at least one - namely $f$ - and Foundation ensures that this is the only one).

Now I'll apply almost parameter-free separation to $Y$. Let $$Z=\{y\in Y: \exists a\in Y(a\not=y \wedge \Psi(a)\wedge y\not\in a(y))\};$$ $Z$ is defined via almost parameter-free Separation applied to $Y$, and we can now prove that $Z=\{x\in X: x\not\in f(x)\}$, and so $Z$ is not in the range of $f$ and hence $f$ is not surjective.

In my argument above, I used Foundation to conclude that the formula $\Psi$ picked out a unique element of $Y$. What if we drop Foundation?

It turns out Foundation isn't necessary, as long as the singleton operation works properly - that is, as long as the following holds:

$(*)\quad$ If $A$ is a set, then $\{\{a\}: a\in A\}$ is a set.

Note that $(*)$ is a consequence of Powerset and almost parameter-free Separation, or of Replacement.

Here's how we use this axiom in lieu of Foundation. WLOG, $X$ has at least two elements. Letting $f: X\rightarrow\mathcal{P}(X)$, define (via $(*)$) the set $$Y'=\{\{x\}: x\in X\}\cup\{f\}.$$ Since $X$ has at least two elements, $f$ must also have at least two elements (indeed $\vert f\vert=\vert X\vert$), so we may distinguish $f$ from each $\{x\}$ in a parameter-free way. We'll use this to do a variant of the trick above: let $$Z'=\{z\in Y': \exists a\in Y'[\vert a\vert>1\wedge \exists w(\{w\}=z\wedge \langle w, w\rangle\not\in a)]\},$$ which exists via almost parameter-free Separation. Now, $Z'$ is almost the diagonal set - namely, we have $$Z'=\{\{w\}: w\not\in f(w)\}.$$ To get the genuine diagonal set, we use the axiom of Unions: $$\bigcup Z'=\{w: w\not\in f(w)\},$$ and we are done.

Since I am not currently aware of any interesting set theories in which $(*)$ fails, this seems a reasonable stopping point.

  • 2
    $\begingroup$ (+1) Particularly because of the addendum on the Foundation Axiom. $\endgroup$ Oct 28, 2016 at 20:26
  • 1
    $\begingroup$ As far as I can see, the defining formula for Z uses Y as a parameter, not just as the set from which we separate. Or am I missing something? $\endgroup$ Oct 28, 2016 at 20:55
  • $\begingroup$ @EmilJeřábek You are quite right, and I have edited to make this clear. $\endgroup$ Oct 29, 2016 at 5:39
  • $\begingroup$ All right, thanks for the clarification. $\endgroup$ Oct 31, 2016 at 10:01
  • 1
    $\begingroup$ Your $(*)$ is a consequence of the full power set axiom and Parameter Free Separation. So it is a theorem of a version of Parameter free Zermelo that has a full axiom of Power set. $\endgroup$ Nov 16, 2016 at 11:32

This is a possible answer, it is not mine, it is due to David Libert. So I'll quote it here and I'll present the link to it.

(Note: the restricted separation mentioned in the following quote is the same parameter free separation that I've presented here)


If I have not made a mistake, I can prove that there models of Z (Zermelo's) set theory with separation replaced by your restricted form, satisfying that there are countably many reals: that is there is a function from omega surjecting onto all reals.

If that proof is correct, it does show there is indeed no proof of omega uncountable using only your restricted separation axiom replacing the usual separation axiom of Z.

I will begin by describing a construction of models of your restricted Z theory. It is similar to the definition of Godel's L model, but weakened to correspond to your weaker restricted separation axiom.

We begin at stage 0 (ordinal 0) with some initial transitive starting set T, and consider the structure (T, epsilon) .

The next step of Godel's L would form all subsets of (T, epsilon) definable in (T, epsilon) by formulas with parameters. Instead we throw in only subsets of sets from the structure definable by pure formulas with only one variable free: no side parameters. We also add explicitly pairs {x,y} and the union axiom union(x) for all x,y since we lost these by restricting the previous formulas.

At ordinal successor steps we do that same step to the last structure as I just said on (T, epsilon). At limit ordinals take unions of all structures.

Iterate out to the successor ordinal of #T. This gives a stabilization, where a formula on the resulting structure acting on the members of a set has a uniform across that set relativization to a bounded stage which is equivalent. This is like the proofs about Godel's L.

I want to find an instance of a construction as above producing a model of restricted Z with P(omega) countable.

For simplicity of exposition, I will first do the easier case of explicitly assuming Con(ZF), and then I will return to how to modify that argument to be a proof in just ZF not assuming Con(ZF).

So to start, assume Con(ZF). So ZFC has a countable model M. (Godel's L result to get ZFC model assuming Con(ZF)).

Use Cohen's forcing to produce M' model extending M making the original reals^M countable.

Inside M', define T to be the transitive closure of the set of all functions from omega onto reals^M. Do the construction I described above inside M'.

This construction is purely definable in M'. Since I threw into T all surjections and not merely a single generic surjection produced by the forcing the definition of T does not depend on any parameters.

From the theory of forcing, when we collapse the reals to countable as usual, any real definable in the resulting M' model in fact came M the ground model.

Each successor step of my construction only added reals definable from the previous structure, since the formulas doing separation didn't use parameters. So in M', each real added at each successor stage is definable in M' from the ordinal for that stage, since the overall construction is M' definable.

The same forcing result, reals definable in M' from only an ordinal parameter are in fact from M.

T put in only reals from M. And all later growth of my construction only added M reals. So even though the construction went on in M', since no parameters were used to define reals all the reals the construction makes are from M.

T provided many surjections from omega to reals^M. So these are in my construction. And since my construction never added any reals from outside M, the Z model of my construction sees these as surjecting onto its reals.

This concludes the Con(ZF) version of the argument.

Regarding arguing from just ZF. We only needed a fragemt of ZF, out to some bounded (in the Levy hierarchy Sigma_n, n finite) instances of replacement. ZF proves M models for such fragments, specifically M models with enough ordinals to have the reflection principal for all Levy level axioms from such a ZFC fragment. This is enough to do a version of the theory of forcing for that fragment.

So in meta theory ZF, you can have Levy-bounded ZF fragment models, and forcing over them. So redo my argument above for M and M' replaced by such fragments, and we can do everything in ZFC, without needing Con(ZF).

So you can defeat Cantor's argument with your restricted separation. But don't celebrate too much. This restricted separation theory is not a reasonable system for set theory. It is too restricted.

Cantor's argument is so simple, and so broadly applicable. I think it a lost cause to try to elude it. If you weaken things to avoid it, you end up throwing out the baby with the bathwater.

Cantor's argument gives the diagonal real as a function from {(n, n) | n in omega}.

To get the same diagonal real as an actual function from omega, we would need to replace that index set by {n | n in omega}.

This trivial reindexing is defeated by the restriction on separation. And that is the only way Cantor's argument fails.

source: Google groups discussion


There is an answer to this question of mine in the following article that was refered to here by Goldstern, see theorem 0.7. Although the author stated it in $ZC^o$, but the argument makes no use of Choice whatsoever. Here is the link:


The reason why such a proof was possible relied on a version of Zermelo that can define pairs of arbitrary sets and also defines set union of any set and of course power set of any set without resorting to Separation in the first place. If we take Zermelo to be the theory axiomatized by the axioms of ZF presented in the Wikipedia at:


taking out from them the Schema of Replament and Axiom of Choice. Then clearly we'll be needing full spearation (i.e. with parameters) in order to define pairs, unions and powers. So if by Parameter free Zermelo it is meant Zermelo so axiomatized but with replacing Separation by a parameter free version of it, then it appears to me that the above proof would be blocked. And I think David Libert's construction provides a counter-example to it.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.