Using expressions like $ \langle x,y \rangle$ in predicate logic formulas

Question

I don't like how books on set theory write logic formulas when describing complex sets. For example that is how a regular book can show that some set $s$ is not a pair:

$$\forall x \forall y (\langle x,y \rangle \neq s)$$

Or by this way a book can show that some set $s$ is a relation: $$\forall p (p \in s \implies \exists x \exists y (\langle x,y \rangle = p))$$

The expression $\langle x,y \rangle$ when used in formulas confuses me. It is like you create an object on the fly. If the object $\langle x,y \rangle$ were constant, it would be fine, but it depends on the quantifiers $x$ and $y$, and outside of the formula doesn't make sense. And the books do it all the time.

I haven't learned logic deeply but it seems to me that the given formulas are not formulas of predicate logic. In predicate logic you have simple quantifiers like $\forall x$ that range over objects and you have predicates that evaluate either to true or false, not to other objects. But in these formulas it is like you can use a complex quantifier: $\forall \langle x,y \rangle$ that ranges over all pairs.

The authors of the books on set theory start using this way of writing without any explanation what they are doing. It is like they were saying: "you will understand it when you take a course on logic, and now watch what we do and do the same." But, alas, they don't even make this clear.

I see only two possibilities: 1) these are legitimate formulas in predicate logic, and my confusion is due to not knowing logic well, or 2) this is just an informal way to express complex ideas, and we can always translate any formula written in this informal way to a legitimate predicate logic formula.

---

That's how I would express that some set $s$ is not a pair. Let's create a property $P(x,y,z)$ which is true iff $\langle x,y \rangle = z$:

$$P(x,y,z) \iff \exists a ( x \in a \land \forall v (v \in a \implies v =x) \land \exists b(x \in b \land y \in b \land \forall v (v \in b \implies v = x \lor v = y)) \land a \in z \land b \in z \land \forall v (v \in z \implies v = a \lor v = b))) $$

Given that property we can express that some set $s$ is not a pair: $\forall x \forall y (\lnot P(x,y,s))$. Here if we substitute $P(x,y,s)$ with the big formula given above, we would get a legitimate predicate logic formula.

We can also express that some set $f$ is a function:

$$\forall p (p \in f \implies (\exists x \exists y P(x,y,p) \land \lnot \exists y' \exists p'(y \neq y' \land P(x,y',p') \land p' \in f)))$$

Answer 1

Not all authors of books on set theory.

See Patrick Suppes, Axiomatic set theory (1960 - Dover reprint), page 31.

The pair set is defined in :

Definition 8. $\{ x,y \} = w \leftrightarrow (\forall z) (z \in w \leftrightarrow z = x \lor z = y)$ & $w$ is a set.

Then we have :

Definition 9. $\{ x \} = \{ x,x \}$.

and finally :

Definition 10. $\langle x,y \rangle = \{ \{ x \}, \{ x,y \} \}$.

Technically, $\langle ..., --- \rangle$ is a term-forming operator, i.e. a (binary) function symbol (like $+$ in arithmetic) which receives as inputs two terms and gives as output a term.