What is the standard first-order language to formalize ZFC?

Question

I was hoping to find an easy, viusally intuitive first-order formalization of ZFC.

I have tried to look in several books, but it's often something that is understimated.

I think a schematic presentation of the language would be straightforward and helpful.

Variables:
Non-logical Symbols:
Logical Symbols:

Signature, Structure, Vocabulary.....

Just an overview that might remain in your head.

Moreover, sometimes I find the equality symbol included, other times it's not.

What is the conventional choice?

Answer 1

See e.g. Enderton, page 70.

FOL Logical symbols

0) Parentheses: $( , )$.

1) Sentential connective symbols: $→, ¬$

2) Variables: $v_1, v_2,\ldots$

3) Equality symbol (optional): $=$

4) Quantifiers: $\forall, \exists$.

Non-logical symbols

Predicate symbols: $\in$ (binary)

Function symbols: none (or occasionally the constant symbol $\emptyset$).

If equality is not part of the underlyig logic, we have to add it to the list of non-logical symbols.

As you can see from the literature, both options are used:

Formally, $\mathsf {ZFC}$ is a one-sorted theory in first-order logic. The signature has equality and a single primitive binary relation, set membership, which is usually denoted $\in$.

See e.g. Takeuti, page 7 for the set theoretic definition of equality:

$a=b \leftrightarrow_{def} (\forall x) [x \in a \leftrightarrow x \in b]$.

Answer 2

There is a not a single theory 'ZFC'; there is a family of closely related, equivalent theories, which vary slightly from one author to the next. There's not a single standard.

In every case I can think of, the language of ZFC has a non-logical binary relation '$\in$', and possibly an equality relation '$=$', which can be a logical or nonlogical symbol depending on taste. Apart from that, there are no more non-logical symbols, and everything is the same as the underlying first-order logic.

Fraenkel, Bar-Hillel, and Levy [1, p. 25ff.] talk at some length about the equality relation. As they point out, there are essentially three options:

(a). Equality is treated as a logical symbol, which is always interpreted by the actual equality relation. The axioms of equality are then viewed as logical axioms.

(b). Equality is treated as a second, undefined binary relation, and appropriate axioms are added to the theory.

(c). Equality is taken as a defined relation within the theory. In this case, the axiom of extensionality is tweaked.

In older texts, (c) was somewhat common, because it allowed set theory to have only one undefined symbol ($\in$). In modern texts, (a) is almost universal, because people are not worried anymore about including the equality axiom as part of the logic.

1: A.A. Fraenkel, Y. Bar-Hillel, and A. Levy (1973), Foundations of Set Theory, 2nd ed., Studies in Logic v. 67, North Holland, 978-0-0808-8705-0