what is the relationship between ZFC and first-order logic?

Solution 1:

First-order logic is a framework in which one can only quantify over elements of the universe. In second-order logic one is allowed to quantify over subsets of the universe.

For example, the axiom schema of induction in Peano axioms is a schema in which for every formula we add a first-order axiom talk about this formula. However if one allows second-order axioms the schema shrinks into one axiom, namely "If $A$ is an inductive set, then $A=\mathbb N$".

In the first formulation for every formula which can be used to define a set we say that if the set it defines has inductive properties then it is indeed everything; on the second-order axiom we are allowed to quantify over subsets of the universe so we say that every subset which has this property has got to be equal to $\mathbb N$.

Many-sorted logic is a logic in which we distinct between several types of elements in our universe. For example set theory with atoms, which allows non-set objects in the universe. In this language there are predicates to indicate whether an object is a set or an atom. It cannot be both.

Second-order theories can be made into first-order theory by expanding the universe to include sets, and adding a distinction between the elements of the original universe and sets. Now quantification over "every set such that ..." is again first-order since those sets are elements of the universe.

ZFC is a first-order logic theory, it allows only to quantify over elements of the universe. It is also one-sorted since there is only one type of elements in a universe of ZFC, namely sets.

Solution 2:

ZFC is a first-order theory over a language with two binary predicates, $=$ and $\in$. It is given by a bunch of axioms, which are sentences in first-order logic.

Second-order logic is many-sorted: it has two different types of variables, basic variables and predicates. Contrastingly, the axioms of ZFC only talk about one kind of object, sets.