Functions are defined as particular kinds of relations and relations themselves relie on the concept of Cartesian Product. It can be proved from ZF the Cartesian Product of two sets exists but this requires using either the Axiom of Separation or the Axiom of Replacement. In both of them we make use of the concept of predicate, so it should be a difference to avoid falling in circularity.
Am I right? Am I missing something?
Thanks in advance :)
On
You're missing that "predicate" in logic refers to a formula in the language with some free variables that denote parameters. For example "$x < 1+1+1$" is a predicate in the language of arithmetic. In any given model we say that a predicate is satisfied by an object tuple iff it is true when that tuple is substituted in place of the free variables (in some specific order of variables). In the natural numbers "$x < 1+1+1$" is satisfied by $0,1,2$.
Defining ZFC as a formal system is no problem in any meta-system that is capable of standard string manipulation, because the axioms of ZFC are defined syntactically (since "predicate" there refers to a formula in the language of ZFC).
Now in the meta-system we can also talk about the collection of objects in a model that satisfy a predicate. For predicates with more than one parameter, this collection is often also thought of as a relation. Note that there may be collections in the meta-system that do not correspond to any predicate.
In particular, any uncountable model of ZFC will have an object $S$ such that the collection of all objects $x$ such that "$x \in S$" is satisfied does not correspond to any predicate over ZFC, namely there is no predicate that is satisfied by exactly the same objects. Same goes for relations and functions in a model of ZFC, which may not correspond to any predicate over ZFC.
Furthermore, there are predicates that do not correspond to any object in any model, such as the Russell predicate "$x \notin x$". Those that do do so precisely because of the axioms of separation and replacement, which are there to reify some predicates (meaning to make them objects). Russell's paradox shows that not all predicates can be reified in classical set theory, which is the same as saying that unrestricted comprehension is invalid.
In first-order logic theories, like $\mathsf {ZFC}$, a predicate symbol is part of the language used to develop the theory.
In set theory, there is only one basic predicate symbol : $\in$.
With it (and the logical symbols of first-order logic with equality) we can build formulae expressing properties of sets, like $\exists x \ \forall y \ \lnot (y \in x)$, that means : there is an emptys set.
Some of them are assumed as axioms, like e.g. the $\text {Axiom (schema) of Separation}$.
With the rules of logic, starting form the said axioms, we can prove theorems about sets.
A particular kind of set is that of relations : as you say, a binary relation is a subsets of the cartesian product of two sets.
A function is a particular kind of relation, and thus a set.
Conclusion : in set theory a function is a set defined by a "condition" expressed in the language of the theory with a formula that uses the predicate $\in$.