This question is about how accurate is it to say that axiomatic set theory is a first-order logic (FOL) theory? The crux of the matter is the nature of the set comprehension symbol $\{\_ \mid \_ \}$.

In FOL, the collection of non-logical symbols is parametric on a triple $(X,F,P)$ where $X$ is a collection of variables, $F$ a collection of function symbols, and $P$ is a collection of predicate symbols. For example, $\emptyset \in F$ represents the empty set and ${\subseteq} \in P$ represents the subset relation. Usually, axiomatic set theory is built from $X$ ranging over all collections, $F = \{\emptyset\}$ and $P = \{{\in},{=}\}$. So far so good.

However, is the binary symbol $\{\_ \mid \_ \}$ in $F$ or in $P$? On the one hand, it is intuitively a function symbol because it identifies a collection in the domain of discourse. However, the second argument in this symbol is a formula in the syntax of the theory ... and this sadly breaks the hierarchy for how terms in FOL are built: terms at the bottom in any syntax tree. On the other hand, one might say that it is a predicate symbol that, in the end, is meta-notation for succinctly writing a formula that uniquely identifies an object in the domain of discourse. However, the expressions $x \in \{ y \mid \phi \}$ and $x \in y$ (assuming $x,y \in X$ and $\phi$ a formula) uses differently the membership predicate symbol: in the former, it refers to the membership of $x$ in a formula!?!?; in the latter, it refers to the membership of $x$ in a collection.

So, which one is it? I have checked several axiomatic set theory books (including Kunen, Jech, and a few more) and there is no clear explanation that can help to answer my question. Btw, it is also OK if you point out that such an axiomatization for set theory, to begin with, is beyond the reach of FOL.


$\{\ \mid \ \}$ can also be seen as simply an abreviation, that does not appear in the "actual" formulas of set theory, just like $\subset$.

If the formula is $\forall x, x\subset y \implies P(x)$, then the actual formula should be $\forall x, (\forall z, z\in x\implies z\in y) \implies P(x)$.

Similary, if the formula is $P(\{x \in z\mid \phi(x)\})$, then the actual formula is $\forall y, y= \{x \in z\mid \phi(x)\} \implies P(y)$ where $y= \{x \in z\mid \phi(x)\}$ is an abreviation that stands for $ (\forall t, t\in y \implies (t\in z \land\phi(t)) )\land (\forall t, (t\in z\land \phi(t)) \implies t\in y)$, so $P(\{x \in z\mid \phi(x)\})$ is an abreviation for

$\forall y, ((\forall t, t\in y \implies (t\in z \land\phi(t)) )\land (\forall t, (t\in z\land \phi(t)) \implies t\in y)) \implies P(y)$.

Now since $ZF \vdash \exists ! y, y= \{x \in z\mid \phi(x)\}$, we allow ourselves to use the latter symbol as an abbreviation for a unique element.

Similarly, $\cup$ is not in the language of set theory, but we allow ourselves to write $A\cup B$ for a set since $ZF\vdash \exists ! z, z=A\cup B$ where $z= A\cup B$ is an abbreviation for a formula that I will let you write out if you wish.

So one can also see this symbol as simply an abbreviation

  • $\begingroup$ Thanks, Max, for the detailed explanation. The answer to my general question is then that axiomatic set theory is indeed a FOL theory. As for the nature of the set-comprehension syntax, it is syntactic sugar and a shorthand for identifying a unique element from the domain of discourse. The trouble I had was that I wanted to see this symbol as part of the syntax, which is not. It is rather meta-notation to name some collections. $\endgroup$ – hquilo May 11 '17 at 18:21
  • $\begingroup$ It is a way of seeing it, yes. And so axiomatic set theory is a first order theory. Mauro Allegranza has answered another way that I'm not familiar with, but yes, it's often used as a meta-notation, but it's not mentioned. If you wanted to do a formal proof, using the abbreviations I gave would give "Let $z$ be the unique set blablabla", but to go faster we just say "Let $z:= \{x \mid \phi(x)\}$". $\endgroup$ – Max May 11 '17 at 18:36

It is FOL.

In general, $\{ \ \mid \ \}$ is a "term-forming" operator. It can be defined with the "definite description" operator $\iota$:

$\{ x \mid \varphi(x) \} :=(\iota y) [\ \forall x \ (x \in y \leftrightarrow \varphi (x))]$.

For more detials, see:

Very similar to:

  • $\begingroup$ Thanks for the answer, especially for pointing me to the notion of definite description, which is completely new to me. In conclusion, axiomatic set theory is a FOL theory. $\endgroup$ – hquilo May 11 '17 at 18:13

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.