Set-builder notation function definition

I know that a function is a subset $f \subseteq X \times Y$ such that

\begin{eqnarray} \forall x \in X, \exists ! y \in Y | (x,y) \in f \end{eqnarray}

First, is it possible to express what a function is using the set-builder notation? I'm thinking about

\begin{eqnarray} f = \{(x,y) | (x \in X) \wedge (\exists ! y \in Y) \wedge ((x,y) \in f)\} \end{eqnarray}

Is this correct? Does the recursion (I mean the fact that $f$ is both in the left-hand side of the equality and the right-hand side) give any problem?

Another thing I came up with is the following:

"A function $f$ is a member of the set

\begin{eqnarray} F = \{f | f \in (X \times Y) \wedge (\forall x \in X) \wedge (\exists ! y \in Y) \wedge ((x,y) \in f)\} \end{eqnarray}"

Can this be taken as a definition of what is a function?

Can you give me any reference to a book, site etc. where a set-builder definition of what is a function is given?

Another curiosity I have is if those definitions I gave (if correct) have something to do with higher-order logic rather than first-order logic.

Thank you, Luca

PS. This is my first post so please be kind :)

Yes, functions can be defined using set-builder notation. But this is not the most common approach.

However, what you have written down is not really well-formed. Let me address this first; then we can end on a positive note.

Compare your expressions with their correct counterparts, so that you may avoid these mistakes in the future (some things are common abuses of notation, but I strongly suggest you get down to writing the tedious full form until you can recognise a well-formed expression within a second):

$$\begin{array}{c|c} \forall x \in X, \exists! y \in Y|(x,y)\in f &\forall x \in X:\exists! y\in Y: (x,y) \in f\\ f= \{(x,y)|(x\in X)\land(\exists!y \in Y) \land ((x,y)\in f\} & f = \{(x,y) \mid \forall x \in X: \exists! y \in Y: (x,y)\in f\} \end{array}$$

and a similar problem arises with the expression for $F$.

So, what is usually done is the following. Let $\rm fn$ be the unary predicate given by:

$$\mathrm{fn}(f) = \forall z \in f: (\exists x,y: z = (x,y)) \land (\forall z' \in f: x_z = x_{z'} \to z = z')$$

That is: "$f$ is a collection of ordered pairs $z = (x_z, y_z)$, and each first coordinate $x_z$ is unique in $f$."

Note that we haven't specified the domain or codomain of $f$ yet. We can use the following binary predicates:

\begin{align} \mathrm{dom}(f,X) &= \mathrm{fn}(f) \land \forall x: (x \in X\leftrightarrow \exists y: (x,y) \in f)\\ \mathrm{cod}(f,Y) &= \mathrm{fn}(f) \land \forall y: ((\exists x: (x,y) \in f) \to y \in Y) \end{align}

Then we can define the set of functions from $X$ to $Y$, $Y^X$, by:

$$Y^X = \{f \subseteq X \times Y\mid \mathrm{fn}(f) \land \mathrm{dom}(f,X) \land \mathrm{cod}(f,Y)\}$$

where it is not hard to show that $f \subseteq X \times Y$ makes the $\rm cod$ condition a consequence of the other two.

All being formulated in the first-order language of set theory, this is a first-order definition. The tell-tale sign is that we have no need for quantifying over predicates, etc..

• It's even common to go farther, once you get the hang of it, and define the range and domain of arbitrary relations. Then, one realizes there's no reason to limit it to relations, so one defines the "domain" function as taking an arbitrary set and returning the domain of the largest relation that is a subset of the set, and similarly for range. Basically, we just ignore any elements of the set that are not ordered pairs. This convention makes it possible to drop the "fn(f)" clause from the definitions. Commented Oct 16, 2013 at 10:34
• Also, although I voted up, there is an important caveat with the "Cod" function. Usually, when people say "codomain", they mean a set that is determined by the function (so Cod(f,Z) and Cod(f,Y) imply Z = Y). Thus, they can talk about the codomain of a function. The Cod(f,Y) function defined here basically just says that the image of f is a subset of Y, which is a weaker substitute for the usual meaning of codomain. In the definition of a function typically used by set theorists, a function does not have a uniquely determined codomain. Commented Oct 16, 2013 at 10:38
• @CarlMummert Interesting; I haven't seen anyone go beyond arbitrary relations -- it's then just some generality that may yield some very strange results AFAI see. As to $\rm cod$, there are indeed two conventions. (Apparently it's easy to forget that the other convention exists... we both did it.) I have come to distinguish "codomain" from "range" as a matter of habit. Moreover, I explicitly called $\rm cod$ a binary predicate, and by no means a function. Commented Oct 16, 2013 at 10:43
• In practice, compared to the usual set theoretic definition of a relation as simply a set of ordered pairs, it doesn't cause any trouble to say, for a set $X$, the domain of $X$ is the set $\{ a : (\exists w)(\exists a)(\exists b)[w \in X \land w = (a,b)]\}$. Similarly for the image of a set $X$. It doesn't have any great benefit, either, but some authors to use this other convention where every set is also a relation. Commented Oct 16, 2013 at 10:47
• @Lord_Farin Regarding the notation, I've always met in a math book the quantifier $\forall$ followed by a comma and the quantifier $\exists$ by a colon or a vertical line (both meaning "such that"), but I guess there are many different variations (link). I read here link that the comma is used in place of $\wedge$... I probably misinterpreted that and mixed it up with the fact that $\exists x \in X : P(x) \equiv (x \in X) \wedge P(x)$ and $\forall x \in X, P(x) \equiv (x \in X) \rightarrow P(x)$ Commented Oct 18, 2013 at 14:36