# If set theory only contains the notions of “set” and “is a member of” as primitives, how can an axiom of set theory refer to a “formula”?

It's said that the primitive concepts of set theory are those of "set" and "membership", then all axioms of set theory must begin with "Let $$A$$ be a set" or "Let $$x\in A$$", but they don't. For example, let us consider the subset axiom:

Subset Axiom. Let $$\varphi(x)$$ be a formula and let $$A$$ be a set. Then there exists a set $$S$$ such that for all sets $$x$$ we have that $$x\in S$$ if and only if $$x\in A$$ and $$\varphi(x)$$.

This axiom begins with "Let $$\varphi(x)$$ be a formula" but "formula" is not a primitive concept, then, for having sense, it must be a defined concept, but as far as I see we can't define "formula" in terms of "set" and "membership" if I am wrong, please tell me. Now, in the case where we can't define "formula", how is the subset axiom justified from a logical point of view?

In many books, when the subset axioms is introduced, the statement "Let $$\varphi(x)$$" is used informally, I will appreciate if you recommend me a book on set theory where the concept of "formula" is used formally, where there is a formal definition of what a formula is.

• One book that elaborates in quite a bit of detail about the anatomy of formulas (and everything to do with their syntax, such as free variables, bound variables, what an "occurrence" of a variable in a formula means, etc.) is Quine's Mathematical Logic (1940). However due to its age it is quite dated and its notation is hard to read (akin to Principia Mathematica), and the axiomatic set theory it presents is somewhat different than ZFC (it presents a system based on New Foundations).
– C7X
Feb 11 at 4:54
• There are many books which define what a “formula” is, but these are usually logic books rather than set theory books. Some examples: Van Dalen, Logic and Structure (terse and concise), Propositional and predicate calculus, Goldrei (good beginner text). In order to study set theory, it helps to have an understanding of logic. Feb 11 at 14:42
• See also First-Order Logic and Set Theory Feb 12 at 9:49

In formalizations of set theory (e.g. ZFC), this subset axiom you've described in usually called the axiom schema of specification. Note the use of the word "schema" in its name: this is where your confusion stems from. Indeed, formally speaking, this is not a single axiom, but a whole collection of axioms: one for every formula $$\phi(x)$$. For every formula $$\phi(x)$$, there is an axiom of set theory which goes "$$\forall A \exists S \forall x (x \in S \Leftrightarrow (x \in A \wedge \phi(x)))$$". Taken together, all these axioms make up what you call the subset axiom.

Edit: Axiomatic set theory is based on first-order logic, which is the system of language and inferences that are used to do this sort of math. It starts with symbols (including variables, connectives like $$\neg$$ and $$\wedge$$, quantifiers $$\forall$$ and $$\exists$$, the $$=$$ symbol, and predicate symbols) which are combined according to certain rules to make formulas. First-order logic also uses rules of inference to deduce some formulas from others. Set theory uses first-order logic with the predicate symbol $$\in$$; its axioms and theorems are formulas. I suggest reading some more (on Wikipedia or in your favorite textbook) if you're interested in learning more about how first-order logic works.

• @RataMágica Formulas and first-order logic come "below" set theory, in that axiomatic set theories such as ZFC rest on top of first-order logic. In each language of first-order logic, there is a definition for what a formula is, which is a string of characters $($, $)$, $\land$, $\lnot$, $\lor$, variable symbols, relation symbols, and predicate symbols, which follows the rules for being a wff of that logic. But this is conceptually "below" set theory, and more general, as it also applies for formalizing what a formula is w.r.t. some other axiomatic systems like Peano arithmetic.
– C7X
Feb 11 at 5:10
• @RataMágica See my edit. Don't forget that you can accept an answer if you believe it resolves your question. Feb 11 at 19:24
• @RataMágica: To follow up Sambo’s general explanation with examples: A formula here means any statement in the logical language we’re using, possibly with free variables — so like “$\exists y,\ y \in x$”, “\forall z, (z \in y \leftrightarrow (z = x_1 \lor z = x_2))”, or in prose, “$x$ is inhabited”, “$y$ is the pair $\{x_1,x_2\}$”. So (1) each individual instance of the axiom schema doesn’t involve the concept of ‘formula’; and (2) once you’re setting out axioms in a formal language, you’re already talking about formulas (possibly under some other name). Feb 12 at 11:16
• Strictly speaking, the definition of "formula" doesn't matter to set theory. My understanding is that The first-order logic definition could be written $∀𝜙∀𝐴∃𝑆∀𝑥(𝑥∈𝑆⇔(𝑥∈𝐴∧𝜙(𝑥)))$, and the definition $𝜙(x)$ is no more part of set theory than the definition of $\forall$ or $\exists$. Feb 12 at 14:29
• @chepner First-order logic doesn't allow you to quantify over formulas $\phi$. For that, you'd need some kind of second-order logic. I'd say that, although the definition of a formula isn't "part of" set theory, it still matters to set theory, precisely because there is a comprehension axiom for each formula. Feb 12 at 15:28

Formulas and first-order logic come "below" set theory, in that axiomatic set theories such as ZFC rest on top of first-order logic. In each language of first-order logic, there is a definition for what a formula is, which is a string of characters $$($$, $$)$$, $$\land$$, $$\lnot$$, $$\lor$$, variable symbols, relation symbols, and predicate symbols, which follows the rules for being a wff of that logic. But this is conceptually "below" set theory, and more general, as it also applies for formalizing what a formula is w.r.t. some other axiomatic systems like Peano arithmetic, or the group axioms.