Does the axiom of separation work for predicates that aren't definite, ie predicates that have logical atoms besides the equality and membership relations?
This came up because a logic professor pointed out to me that when we describe events of a sample space, we can only deduce that equivalent descriptions of events give equal events because of the separation axiom, and it isn't always obvious how to reduce event descriptions to having only membership and equality atoms. So if we have arbitrary predicates A and B, and know that they're equivalent, we can't use separation to separate their corresponding events from the sample since we have no information about them with which to reduce them to equality and membership.
First, let's get a subtlety out of the way.
There are two ways to discuss a unary predicate on the set $S$. The first is as a logical formula $\phi(s)$, typically phrased in some sort of first-order logic, where the only free variable in $\phi(s)$, if there is any, is $s \in S$. I call this an "external" predicate.
The second is a function $\chi_\Phi : S \to \Omega$ where $\Omega$ is the set of truth values (classically, $\Omega = \{\top, \bot\}$ is a 2-element set). I will refer to this as an "internal" predicate.
The third is a subset $\Phi \subseteq S$. Note that every subset $\Phi$ of $S$ corresponds to a function $\chi_\Phi$, with the property that for all $s \in S$, we have $\phi(s) = \top$ if and only if $s \in \Phi$. In other words, we have $\Phi = \{s \in S \mid \chi_\Phi(s) = \top\}$. So this is essentially just an alternate way of phrasing the definition internal predicate.
One way of discussing an "indefinite" predicate is as an internal predicate $\chi_\Phi : S \to \Omega$. Here, we have no issue at all using the axiom of separation to form the set $\Phi = \{s \in S \mid \chi_S(s) = \top\}$. More formally, we can translate the $\chi_S(s) = \top$ to the statement $(s, \top) \in \chi_S$, which can then be translated further as elaborated below into a statement which involves only set membership.
The more difficult case is if we have an external predicate which does not use the two primitive symbols of set theory, $\in$ and $=$ (assuming we're working with ZFC - other set theories like ETCS and SEAR have function composition or relations as their primitive notions and not set membership).
The first argument is that there actually is no such external predicate $\phi(s)$. Set theory does not permit such a predicate to exist at all.
Certainly, we can come up with all kinds of predicates like $\phi(s) :\equiv (s^2 + 2s + 1 = 0)$, for example. But all of these predicates can be translated, often in an extremely complicated way, into a logically equivalent external predicate which does not involve any nonlogical symbols other than $\in$ and $=$.
In this view, when we introduce notation such as $s^2$ or $+$, what we're actually introducing is not a new concept but rather a systematic way of taking extremely long first-order logic formulas in the basic language of set theory and abbreviating them. So things like $+$ or squaring or even numbers like 1 don't actually have an independent existence. Instead, they are used as part of a system of definitional extensions to the ground theory which do not permit one to say new things, but do permit one to say old things in a much more concise way.
An example would be that the statement $((a, b) \in c)$ is first translated to $\{\{a\}, \{a, b\}\} \in c$. It is then translated to $\exists d (d \in c \land d = \{\{a\}, \{a, b\}\}$, which is then translated to $\exists d (d \in c \land \forall x (x \in d \iff x = \{a\} \lor x = \{a, b\}))$. This statement is then translated to $\exists d (d \in c \land \forall x (x \in d \iff (\forall y (y \in x \iff y = a)) \lor (y \in x \iff y = a \lor y = b)))$.
The idea is that the statement $(a, b) \in c$ is, formally speaking, just an abbreviation for the very complicated and lengthy formula $\exists d (d \in c \land \forall x (x \in d \iff (\forall y (y \in x \iff y = a)) \lor (y \in x \iff y = a \lor y = b)))$.
The second key point is that there is no way, within set theory, to properly quantify over external predicates. There is no single formula within set theory which expresses the statement
So in fact, separation is actually an infinite collection of axioms, one for each statement $\phi(a, x_1, x_2, ..., x_n)$.
But one can perfectly well quantify over internal predicates and prove the statement
This is perfectly permissible.
Finally, the thing you need separation for isn’t proving that equivalent conditions for an event represent the same event. This follows from extensionality. You need separation to show that a “description of an event” actually corresponds to an event at all.