Predicate logic in set theory: what components can we write in an expression?

Question

Recently, I wanted to look more into the foundations of mathematics. I started reading Enderton's Elements of Set Theory and have become confused with what exactly we can use in predicate logic statements. This is bad news for me, because set theory is already quite fundamental, and since I'm familiar with reading and some writing of logic statements (from an undergraduate class), I don't want to go another level deeper and waste a bunch of time learning predicate logic in full rigor.

For an example of where I'm confused: Enderton shows in Corollary 3C that the cross product $A \times B$ exists as a unique set. He writes roughly (if we elaborate on his shorthand) that

$$\exists C\; \forall w\ (w \in C \iff w \in \mathcal{P} \mathcal{P}(A \cup B) \wedge [\exists x\ \exists y\ (x \in A) \wedge (y \in B) \wedge w = \langle x, y \rangle]).$$

I'm confused about several points, mostly involving the predicate logic:

1. There are no quantifiers here over $A$ or $B$. In the English preceding this expression, $A$ and $B$ are said to be sets. When do we explicitly write something like $\forall A$, rather than just saying something like "let $A$ be some set" and then launching into the predicate logic statement?
2. We also seem to be using $\langle x, y \rangle$ (which was defined previously) in the predicate logic statement. When can we write expressions of variables, like this?
3. To expand on question 2, what are exactly the elements which are allowed in valid predicate logic statements? For example, constants ($1$, $0$), variables being quantified over, quantifiers, propositional logic operators ($\wedge$, $\vee$, etc.)? I can read simple predicate logic easily and would just like to know what's valid to write.

Thank you for your help.

Answer 1

1. Yes, you can imagine this to be universally quantified over $A$ and $B.$ So it says "for all $A$ and $B$ there exists a $C$ such that $C$ has the defining properties of the cartesian product of $A$ and $B.$"
2. You may want to read about definitional extensions (perhaps it is explained in Enderton). We can write the statement here purely in the language of first order logic with equality and just the relation symbol $\in.$ In particular we can replace $\mathcal{P P}(A\cup B)$ and $\langle x,y\rangle$ with their definitions. For instance, instead of writing $w=\langle x,y\rangle$ we can write $$\forall z(z\in w\leftrightarrow z=\{x\}\lor z=\{x,y\}) $$ and then we can replace $z=\{x\}$ by $\forall u(u\in z\leftrightarrow u=x)$ and so on. Needless to say this becomes unreadable pretty quickly.
3. It depends on what your language is. As we mentioned before, the language of set theory technically has no constants or function symbols, only the relation symbol $\in,$ so everything can be expressed in terms of variables, connectives, quantifiers, $=$ and $\in.$ However this is completely unnecessary and impractical in practice. In general, if there is a formula $\phi(\vec x,y)$ such that the theory (say, ZFC or something somewhat weaker, though this idea is not particular to set theory) can prove $\forall \vec x\exists !y\varphi(\vec x,y)$ then we can add a new function symbol $f_\varphi$ to the language and the axiom $$\forall \vec x\forall y (y=f_\varphi(\vec x)\leftrightarrow \varphi(\vec x,y))$$ an the resulting theory is a conservative extension of the original theory. This is how we can formally add things like, say a constant representing $\emptyset$ or $\omega,$ or a function symbol representing the pairing function $x,y\mapsto \{x,y\}$ or the binary union $x,y\mapsto x\cup y,$ and on and on as we keep adding definitions. To get new defined relations, for any formula $\varphi(\vec x),$ you can add a new relation symbol $R_\varphi$ with the same arity as the formula and then add the axiom $\forall \vec x (R_\varphi (\vec x)\leftrightarrow \varphi(\vec x))$ to similar effect (and defining relations doesn't even require us to know the theory a certain strength like we need to prove functionality when defining functions). So you can either understand these sentences as abbreviations for formal sentences in the pure language of set theory (which may be the best course cause many other liberties will typically be taken that just using new defined symbols), or you can imagine it as a formal sentence in a definitional extension of the language over the theory, like we just described.