How does ZFC define functions?

Question

I found the following definition on Wikipedia.

Is it the most common definition? How is the definition usually notated?

A function f from X to Y is a subset of the Cartesian product X × Y subject to the following condition: every element of X is the first component of one and only one ordered pair in the subset. In other words, for every x in X there is exactly one element y such that the ordered pair (x, y) is contained in the subset defining the function f. This formal definition is a precise rendition of the idea that to each x is associated an element y of Y, namely the uniquely specified element y with the property just mentioned.

Answer 1

$\sf ZFC$ doesn't define anything. It's just a mathematical theory, whose language includes only one extralogical binary relation symbol denoted by $\in$.

Mathematicians, in particular set theorists, define things in the language of $\sf ZFC$ which are interpreted as functions.

Set theorists see functions as sets of ordered pairs. We say that $f$ is a function if:

1. $f$ is a set of ordered pairs.
2. If $(x,y)$ and $(x,z)$ are both in $f$, then $y=z$.

Then we write $f\colon X\to Y$ if:

1. $f$ is a subset of the cartesian product $X\times Y$, which is the same as saying that $(x,y)\in f$, then $x\in X$ and $y\in Y$.
2. $f$ is a function.
3. For every $x\in X$ there is some $y$ such that $(x,y)\in f$. We also denote this $y$ as $f(x)$.

---

So how do we define ordered pairs? Well, there are several ways, the best known is the definition given by Kuratowski:

$$(x,y) = \biggl\{\{x\},\{x,y\}\biggr\}$$

We can check to see that this definition satisfies all the properties of an ordered pair, and therefore it is a good definition. Now the definition of a function is complete. We have the properties that we want, and we have the implementation of these properties.

However! Note that the definition of an ordered pair, or even a function, is just an abstract definition. There are just some properties that we want a function to satisfy, and any interpretation which adheres to these "axioms" or "definition" is worthy of the name function (or ordered pair).

So whenever we write a proof in set theory, we really write a schema for a proof, where one later on plugs in the definition of an ordered pair, and the definition of a function, and so on and so forth. Occasionally we will require a particular interpretation, but as long that we know that such interpretation exists it's fine.

Answer 2

A relation $R$ on $A,B$ is just an subset of $A\times B$, or we can say a relation is just a set with a bunch of ordered pairs.

A function $F$ is a relation with the following additional requirement:

$\forall x\forall y\forall z(\langle x,y\rangle\in F\wedge\langle x,z\rangle\in F\rightarrow y=z)$.

That is, the "value" of $F$ to each $x$ must be unique. Then we may use the notation $F(x)$ to denote that unique object.

Answer 3

ZFC doesn't define anything; it's just a theory of sets. In particular, every object in a model of the theory of sets is (by definition) a set.

The idea is: there is a notion of 'function' inherent to mathematics: a function $f$ is an entity which associates two sets, say $X$ and $Y$, by assigning to each element $x \in X$ an element $f(x) \in Y$. Simple as that.

The problem is that 'entity' isn't good enough, we need it to be a set. How do we formalise this notion? Well associated with every function $f : X \to Y$ is its graph. In the case of $f : \mathbb{R} \to \mathbb{R}$ this really is its graph: you draw a pair of axes, which give you the plane $\mathbb{R}^2$, and then the graph of $f$ is a certain subset of $\mathbb{R}^2$. Every function has a graph, and given the graph of a function we can recover the function from the graph, so identifying a function with its graph seems like a sensible thing to do.

So, when we formalise the notion of a 'function' in the language of set theory, we can define it to be a subset $f \subseteq X \times Y$ satisfying precisely the conditions needed for this subset to be the graph of a function. We can then think of $\langle x,y \rangle \in f$ as meaning $y=f(x)$, because the graph is precisely the set of pairs $\langle x, f(x) \rangle$ for $x \in X$.

What this means is that: $f$ is a function $X \to Y$ if and only if $f \subseteq X \times Y$ such that, for each $x \in X$, there is a unique $y \in Y$ such that $\langle x,y \rangle \in f$.

This is probably the most common formalisation of a function in ZFC. But theoretically, any formalisation that allows you to (reversibly) encode the essence of being a function (i.e. assigning to each element of the domain an element of the codomain) would be just as good a formlisation as this one.

---

Another possible definition would use the cograph, which a partition of $X \sqcup Y$ (the disjoint union of $X$ and $Y$), all of whose components contain exactly one element of $Y$. Then $f(x)=y$ if and only if $x$ and $y$ lie in the same subset of the partition. (This is dual in a very precise sense to the graph.)