Can Cantor's theorem be proved in Parameter Free Zermelo? 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.  
 A: 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)
Quote 

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
A: 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.
A: 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:
http://wwwmath.uni-muenster.de/u/rds/ZFC_without_parameters.pdf
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:
https://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_theory
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.
