I have been looking at how separation can be deduced from replacement. I have found already this question: Proving Separation from Replacement

It was very enlightening, but it caused some thoughts to arise. First of all, I have noticed that people have different versions of the axiom of replacement. Omitting for brevity the requirement on $P$ to be a functional predicate, the version I use is the following: $\forall A \, \exists B \, \forall C, (C \in B \leftrightarrow \exists D \,(D \in A \wedge P(D,C)))$

I noticed other people had a version with $\exists! B$. The thing that puzzles me is that if you take "my" version of the axiom and instantiate B with $X$ and then with $Y$, it is very easy to prove that $X=Y$ (without even using any set theory, just logic). And this means to me that there is no reason to have $\exists! B$ as an axiom, because it can be very easily derived. My first question would be: am I right or am I missing something?

Moving on, I seem to see two different proofs for the separation schema and one seems massively easier than the other one, so yet again I am puzzled. The easy one is proposed by Mauro in the page I linked. All he does is choosing an functional predicate $\phi(u) \land u = v$ to be used in the replacement axiom, where $\phi$ is the predicate we want to apply separation to. Then, everything follows relatively naturally.

I also see another more complicated way of doing this that I really do not understand. I see two different cases being tackled. The first case is when there actually exist values of $u$ in the starting set (say $A$) that satisfy $\phi$ and the second case is when they do not exist. Honestly, in Mauro's proof, I can't see a place where things don't work if you choose a $\phi$ that is not true for any $u \in A$.

The complex proof then uses a functional predicate that is $(\phi(u) \land v=u) \vee ((\neg\phi(u)) \land v=\bar{v})$, where $\bar{v}$ is one of the values for which $\phi$ holds.

I suppose this proof is well-known but the place where I found it is a youtube video: https://www.youtube.com/watch?v=AAJB9l-HAZs&t=3757s You can find it around minute 1:06:19.

My question is whether Mauro's proof is all I need or there is a reason that escapes me for the more complicated proof.

  • $\begingroup$ You found one question, that's a good start. On that question, on the right side of the page, you will find Linked with more questions and answers. $\endgroup$
    – Asaf Karagila
    Jan 14, 2018 at 2:46

1 Answer 1


As for your first question, you are correct: there is no need to assert uniqueness of $B$ in the statement of replacement, and in fact your version without uniqueness is the more usual way to state it. However, you do need some set theory, not just "logic": you need the axiom of extensionality. Without extensionality, you could have two different sets which have the same elements.

As for the two different proofs of separation, they are a result of using two different definitions of "functional predicate", and thus two different (though equivalent) statements of replacement. It appears that you are defining $F(u,v)$ to be a functional predicate if for every $u$, there is at most one $v$ such that $F(u,v)$. However, it is also common to define $F(u,v)$ to be a functional predicate if for every $u$, there is exactly one $v$ such that $F(u,v)$. In that case, your predicate $\phi(u)\wedge u=v$ is not functional (unless $\phi(u)$ is always true), and so you need to modify it before using replacement.

  • $\begingroup$ Thank you, Eric, you really have the gift of clarity. I think you are saying that my version of the axiom of replacement covers more cases than it is strictly needed. Anyway, rather than complicating the proof of the schema of separation, I think it might be easier to prove the schema of replacement starting from my loose definition of functional predicate starting from the axiom of replacement containing the more strict version of the definition of functional predicate. $\endgroup$ Jan 14, 2018 at 10:23

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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