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 🙂
Best Answer
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..