1) Parameter free Z is Zermelo set theory with its axioms formulated exactly as:
Extensionality: as usually presented
Pairing: for all a,b Exists x (x={a,b})
Union: for all a Exists x: x={y|Exist z in a (y e z)}
Power: for all a Exists x: x={y| y subset_of a}
Infinity: as usually presented
Separation: If phi(y) is a formula in which only the symbol
"y" occurs free, then "forall A Exists x : x={y| y e A ^ phi(y)}" is an axiom.
/
Now this theory is equivalent to the theory that formulizes Zermelo with phi(y) having free variables other than y, which are called as parameters.
Proof: the trick is easy for any string of parameters w1,..,wn we can easily apply pairing and binary union sufficiently many times to have the set, S={{1,w1},..,{n,wn}} , we take w1,..,wn to be not ordinals <n+1, since if any one of them was an ordinal <n+1 then it would be parameter free definable and we'd have no problem in getting rid of it from the list of parameters, so we are only concerned with when all of them are not ordinals < n+1. Notice that the set S is a set of doubletons. Now we take the set P1(A) of all singleton subsets of the set A (where A is the set we want to apply separation upon). P1(A) is definable in parameter free separation by separating on P(A) using the formula "..is a singleton". Now we take P1(A) U S and take the set of all sets {{y},{1,w1},..,{n,wn}} were y in A i.e. the set of all sets that are unions of S and a singleton subset of P1(A), call this set S*. Of course this seems to use S and P1(A) as parameters, but there is no need for that since S* is definable by separating on P(P1(A) U S) using the formula "..is a set having n+1 members with exactly only ONE of them being a singleton".
Now we Separate on S* using the following formula:
Exists y,w1,..,wn (k={{y},{1,w1},..,{n,wn}} ^ Phi(y,w1,..,wn))
notice that this formula is parameter free.
Lets call this set as S**
Now clearly taking the union of S** and separating on it using "..is singleton" to get the set S*** and then taking the union of S*** which would be the desired set provable from parameterized separation, i.e. the set of all elements y of the set A that satisfy Phi(y,w1,..,wn).
QED
2) ZF with replacement formulated without the use of parameters is equivalent to ZF with the full parameterized version of replacement.
The parameter free version of replacement (Rep0) is:
Ax e A E!y (phi(x,y)) -> EB Ay (y e B <-> ExeAphi(x,y))
where phi(x,y) only have "x" and "y" symbols occurring
free in it.
Proof: We first prove that Sep0 follows from Rep0 in the usual manner.
Let phi(x,y) <-> [(phi(x) ^ y={x}) or (~phi(x) ^ y=0)]
where phi(x) has only the symbol "x" occurring free in it.
Now replace on A in Rep0 shown above, and we'll get B being
the set of all singletons of elements of A satisfying phi and of 0. Now clearly the union of this set is the separated set from A whose elements fulfill the parameter free formula phi(x).
Now the rest of the proof is easy.
First for parameters w1,..,wn we build the set
S={{1,w1},..,{n,wn}} using pairing and binary union
applied sufficiently many times, again we are
interested in w1,..,wn all being not ordinals <n+1
so S is a set of doubletons.
Now we take the union of S and the set P1(A) of all singleton subsets of A. Lets call that set S*, now we
take the power of S* and separate on it using the formula
".. has n+1 elements with exactly only ONE of them
being a singleton set". Now this will be the set of all
sets {{x},{1,w1},..,{n,wn}} were x in A and w1,..,wn are the parameters. Now call this set as A*.
Now what we do is to use Rep0 and replace from A* along the following formula on the right of the biconditional:
ExeA* ^ Em,w1,..,xn (x={{m},{1,w1},..,{n,wn}} ^ phi(y,m,w1,..,wn))
clearly the formula after ExeA* only has x,y as its sole free variables.
It is clear that the set of all y's satisfying the above formula is the set B asserted by parameterized replacement from A using parameters w1,..,wn after replacement formula phi(y,x,w1,..,wn).
QED