# Question about a list of ZF axioms and, in particular, SEP

In A.G. Hamilton's Logic for mathematicians, eight axioms of ZF are given: EXT, NULL, PAIR, UNION, POW, REP, INF and REG.

The Axiom Scheme of Replacement is formulated like this: $$(\forall x_1)(\exists! x_2)\mathscr{A}(x_1,x_2)\to(\forall x_3)(\exists x_4)(\forall x_5)(x_5\in x_4\leftrightarrow(\exists x_6)(x_6\in x_3\wedge\mathscr{A}(x_6,x_5)))$$

My question is:

Since SEP is not taken as an axiom, shouldn't REP be formulated $$(\forall x_1)((\forall x_2)(x_2\in x_1\to(\exists! x_3)\mathscr{A}(x_2,x_3))\to(\exists x_4)(\forall x_5)(x_5\in x_4\leftrightarrow(\exists x_6)(x_6\in x_1\wedge\mathscr{A}(x_6,x_5))))$$

• See this post for a derivation of SEP from REP – Mauro ALLEGRANZA Sep 16 '15 at 17:18
• What is this reformulation intended to accomplish? Changing the scope of the first two quantifiers like that is a weird move... – Malice Vidrine Sep 16 '15 at 17:30
• @MaliceVidrine Instead of requiring $\mathscr{A}$ to be functional in $x_1$ on the class of all sets, we require it to be functional in $x_1$ on a given set $x_2$. In some places the condition $x_1\in x_2$ in the antecedent of the implication is not given (e.g. in Hamilton's book). I was reading a proof of PAIR in Suppes' Axiomatic Set Theory (p. 237) from POW and REP but he gives REP as in my question. I was not able to translate the proof with the first formulation of REP because using his $\mathscr{A}$ the antecedent is not true without the condition $x_1\in x_2$. – Guest Sep 16 '15 at 17:37
• In fact I'm pretty sure the reformulation must be false. If you instantiate $x_1$ as the empty set and $x_2$ as a set having at least one member besides the empty set, and $\mathscr{A}(x,y)$ as "$y$ is the same size as $x$", then it says that a set containing the empty set and every set the same size as any other member of $x_2$ will exist. – Malice Vidrine Sep 16 '15 at 17:43
• @MaliceVidrine Indeed I think I messed up. I think what I want is this: $(\forall x_1)((\forall x_2)(x_2\in x_1\to(\exists! x_3)\mathscr{A}(x_2,x_3))\to(\exists x_4)(\forall x_5)(x_5\in x_4\leftrightarrow(\exists x_6)(x_6\in x_1\wedge\mathscr{A}(x_6,x_5))))$ – Guest Sep 16 '15 at 18:03

If I understood your reformulation correctly, you're trying to capture the idea that we must first have a set in order to be able of specifying (or separating) a further set by a property (if that's not the idea, ignore my answer). That "patch", however, is not necessary: the consequent of the axiom already specify that the "values" of the function-like expression must belong to a set in order for there to be a further set containing their "images". Notice that the existential quantifier $\exists x_6$ is dependent on the previous quantifier $\forall x_3$; this means that the consequent states: for every set $x_3$, there is a further set $x_4$ such that for every set $x_5$, $x_5$ is an element of $x_4$ iff there is an element $x_6$ of $x_3$ such that $\mathscr{A}(x_6, x_5)$.

As for Suppes, note that he's working in a set-theory with urelements (objects which are not sets). That's why he includes a free variable (not bound, as in your case) for sets in his formulation of the axiom.

• I think you understood. I understood what you wrote in your first paragraph. My concern was essentially to know whether the first formulation of REP, call it REP1, implied the second one, call it REP2. A link posted in the comments seems to suggest that REP1$\implies$SEP and from SEP and REP1 I think it is clear that we have REP2. So if I understand correctly, Hamilton's approach is correct. As for Suppes, I don't understand your second paragraph. I thought that letting a variable free or not in an axiom does not matter, both formulations being equivalent? – Guest Sep 16 '15 at 18:22

This is confusing. Did you use actual individual variables of the formal language to write the axiom? Or perhaps are $x_1$ to $x_6$ metavariables (metamathematical variables)? If these are individual variables, then this wff is not the REP scheme (without parameters), because the metamathematical variable $\mathscr{A}$ (which represents some wff) has fixed individual variables $x_1$ and $x_2,$ being functional on $x_2$ with $x_1$, and one cannot introduce $x_5$ and $x_6$ in the consequent, except in the case of substitutions of variables (and perhaps this is what you meant whith the brackets "$\mathscr{A}(x_6,x_5)$"), but this is unnecessary. Being $x_1$ to $x_6$ individual variables, of course they are all distinct. Make sure $x_4$ is not free in $\mathscr{A}$ and just repeat $x_2$ and $x_1$ in the consequent like this

$$((\forall x_1)(\exists! x_2) \mathscr{A}) \to (\forall x_3)(\exists x_4)(\forall x_2)((x_2 \in x_4) \leftrightarrow (\exists x_1)((x_1 \in x_3) \wedge \mathscr{A}))$$

and we are done.

Note that we can interchange the individual variables by others not occurring on the scheme by means of some alphabetic variant (meta)result.

On the other hand, if $x_1$, ..., $x_6$ are metavariables, then one has to make explicit they represent distinct individual variables, except that $x_6$ is $x_1$ and $x_5$ is $x_2$ or they are all distinct and the string $\mathscr{A}(x_6,x_5)$ is the wff obtained from the wff $\mathscr{A}(x_1,x_2)$ by replacing $x_1$ by $x_6$ and $x_2$ by $x_5$ where they are substitutable.