# How functions definided by cases, can be written in formal ZFC set theory?

Function definition by cases.

It is usual define for example the absolute value of Real number as

$$\left|x\right| = \begin{cases} x & if & x> 0 \\ -x & if &x < 0 \\ 0 & if & x = 0\end{cases}$$

However ZFC does not has anything like cases nor ifs

How this kind of function definition by cases can be written in the formal ZFC set theory?

Only for give you a context:

A function $f\colon X\to Y$ is a subset of $X\times Y$ such that $(x,y_1)\in f$ and $(x,y_2)\in f$ implies $y_1=y_2$.

so to define a specific function $F$ for given sets $A$ and $B$ one can write:

$$F = \{(x,y)\in A\times B : y = U(x)\}$$ in this case $B\subseteq P(U(A))$

or if $A$ is the Real numbers

$F = \{(x,y)\in \Bbb{R\times R}: y = \sqrt{x^2}\}$ and this is the obvious answer to my example but my question is the general handle of cases in defining functions formally in ZFC, the Direchlet function is another example with a a less obvious solution (but it do has too).

-

## migrated from mathoverflow.netMay 26 at 14:50

This question came from our site for professional mathematicians.

Wrong forum for this question. As you note: in ZF we realize a function as a set of ordered pairs, and there are operations we can do on sets. –  GEdgar May 26 at 14:25

Let us consider the absolute value, to begin with. In $\sf ZFC$ there are formulas which define the real numbers, their order, the number $0$ in the real numbers, and the addition of the real numbers.

(Note that indeed there are many different ways to interpret and represent the real numbers as sets, but they all have the same properties, so it doesn't matter. So we just fix one way of doing that.)

Then we can define what is $-x$, given a real number $x$. It is the unique real number $y$ such that $x+y=0$.

Now we can define using the formulas which define $0_\Bbb R$ and $<_\Bbb R$ (and I will omit the subscript $\Bbb R$ from here on end) the sets $\Bbb R^-=\{x\in\Bbb R\mid x<0\}$ and $\Bbb R^+=\{x\in\Bbb R\mid 0<x\}$.

Finally we can define the function $|x|$ as the union of three functions, $F_1=\{(x,x)\mid x\in\Bbb R^+\}$, $F_2=\{(x,y)\mid x\in\Bbb R^-\land y=-x\}$ and $\{(0,0)\}$. We can now verify that the three are functions, and that their domains are disjoint. Therefore their union is a function as well, and we can now prove that this union is a function whose domain is $\Bbb R$.

More generally, if we want to divide into cases, we use the complicated formulas which define the real numbers, and the things we want to use, and then we define the various cases. If we ensured that no $x$ satisfies two incompatible cases (i.e. two cases which result in a different value), then the union of these is the function we wanted.

You can try and sit down to write such formulas, or start with the formulas defining $\Bbb R$ and its basics (order, addition, etc.), then write explicit formulas for the absolute value:

$$\{(x,y)\mid \exists z(\varphi_0(z)\land ((x=z\land y=z)\lor(\varphi_{<_\Bbb R}(x,z)\land\varphi_{+}(x,y,z)=0)\lor(\varphi_{<_\Bbb R}(z,x)\land x=y)))\}$$

Doing so for more complicated functions is, well, more complicated. The point is that we know how to do that mechanically.

-
Thank you very much for your answer. However you focus too much in R and that is important but I would like the general case. For example: Let two sets A and B and a1,a2 subsets of A and b1,b2 elements of B. I want to define formally in ZF the following function F from A to B: $$F(x) = \begin{cases} b1 & if & x ∈ a1 \\ b2 & if & x ∈ b2 \end{cases}$$ How can this be done formally in ZF? I thing the choice axiom is too powerful for this, so suppose we stay in ZF only. –  Carlos Freites May 26 at 15:57
Choice has nothing to do with that. Partition $A$ into several parts, on each part you have a function, take the union of the functions. –  Asaf Karagila May 26 at 16:03
I mean formally for example in the way you did for R $\{(x,y)\mid \exists z(\varphi_0(z)\land ((x=z\land y=z)\lor(\varphi_{<_\Bbb R}(x,z)\land\varphi_{+}(x,y,z)=0)\lor(\varphi_{<_\Bbb R}(z,x)\land x=y)))\}$ I thing the my informal F is more formal than your sugestion –  Carlos Freites May 26 at 16:07
Carlos, you have some $\varphi_1(x)$ and $\varphi_2(x)$ (say two cases) and you have some $\varphi_f(x,y)$ and $\varphi_g(x,y)$ which both define function somehow (I'm omitting parameters from all these formulas; but we may use parameters which may be whatever sets we want). Then we have $$F(x)=\{(x,y)\mid(\varphi_1(x)\land\varphi_f(x,y))\lor(\varphi_2(x)\land\varphi‌​_g(x,y))\}.$$ Note that this is just the union of two sets which can be defined separately. One should note that we need to show that $\varphi_1(x)\leftrightarrow \lnot\varphi_2(x)$ for every $x\in A$, or else we may have troubles. –  Asaf Karagila May 26 at 16:13
GREAT! Thank you. That is what I need. –  Carlos Freites May 26 at 16:19