How do you formalize, in ZFC set theory, the process of forming a function from an expression?

Intuitively, I want to say something like this (I am guessing some vocabulary):

There is an expression $E$ with the only free variable $x$. When $x$ is substituted in $E$ with an element of a set $X$, the expression evaluates to an element $y_x$ of a set $Y$. Therefore, there exists a function $f_E : X \to Y$ such that $f_E(x) = y_x$.

The motivation is that I want to formalize the derivative of an expression, as in $D(x^2) = 2x$, where $x \in \mathbb{R}$. Here $E = x^2$, and the problem is to extract the implicitly-defined function $f_E : \mathbb{R} \to \mathbb{R}$ such that $f_E(x) = x^2$; the definition can then be reduced to that of the derivative of a function.


First note that the language of set theory has no constant symbols, or function symbols. So what $E$ really is, is a formula with free variables $x, y$ and possibly some parameters which are fixed, and for every $x\in X$ there is exactly one $y\in Y$ such that $E(x,y)$ is true in the universe.

So the set $f_E$ is really however you choose to represent functions on set theory, using $E$ to define it. For example if a function is a set of ordered pairs, then $f_E=\{\langle x, y\rangle\in X\times Y\mid E(x,y)\}$.

The parameters could be additional structure on $X$ or $Y$. Like addition, multiplication, topologies, etc.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.