I am reading Halmos’ Naive Set Theory. I attempt to translate the axioms of set theory as Halmos puts them in formal first-order logic containing equality and belonging. Please check if these are correct:
Axiom of Extension: Two sets are equal if and only if they have the same elements.
Immediate translation: $$\forall A\forall B(A=B\leftrightarrow\forall x(x\in A\leftrightarrow x\in B))$$
Axiom of specification: To every set $A$ and to every condition $S(x)$ there corresponds a set $B$ whose elements are exactly those elements $x$ of $A$ for which $S(x)$ holds.
Immediate translation: $$\forall A\exists B(x\in B\leftrightarrow x\in A\wedge S(x))$$
Ad hoc axiom (to be later replaced by axiom of infinity):
… there exists a set.
Immediate translation: $$\exists A$$
Axiom of pairing: For any two sets there exists a set that they both belong to.
Immediate translation: $$\forall A\forall B\exists C(A\in C\wedge B\in C)$$
Axiom of unions: For every collection of sets there exists a set that contains all the elements that belong to at least one set of the given collection.
Immediate translation: $$\forall A\exists B\forall x(\exists C(x\in C\wedge C\in A)\rightarrow x\in B)$$
Note: Though Halmos doesn’t explicitly assume that the theory is one-sorted (only sets are the “objects” of the theory), I bravely assume it. Otherwise I’d to use statements such as $\forall A(A \text{ is a set …})$. Is my assumption okay if I just want to translate what Halmos writes?
Comments
The usual form of Pairing is :
In this case we have : $∀A∀B∃C∀w \ (w ∈ C ↔ w=A ∨ w=B)$.
But see Halmos, page 9 : from the "more liberal" version he uses (and correctly formalized by you) the usual version is derived through Separation.
The "usal" formulation of FOL is that every interpretation has a not-empty domain. This means that the ad hoc Existence axiom is not needed.
Having said that, if we want to expess it, $∃A$ is not a well-formed formula.
We need :