## 1/0 = 0, really!

Let $(K, +, \cdot )$ be a field. We can define division as a function in $K\times K\setminus \{ 0\} \rightarrow K$ in the obvious way. Now, what is the value of that function on the pair $\langle 1, 0\rangle$? In general, what is $f(x)$ if $f : X \rightarrow Y$ and $x\notin X$? Is it undefined? How do we define “undefined” ? Surprisingly, in ZF $f(x) = \emptyset$ in such case. In Isabelle/ZF this is lemma apply_0 in func.thy theory. Metamath also proves this as Theorem ndmfv. To see why this is true, look at the Metamath’s definition of the value of function at a point and think what happens when F“{A} there is empty.

So $1/0 = \emptyset$ because the pair $\langle 1,0 \rangle$ is not in the domain of division. Why then we can write $1/0 = 0$? We are cheating a bit here. In ZF set theory the empty set and the zero of natural numbers are the same thing. So really $1/0 = 0$, but the zeros on both sides denote different things.

Tags:

### 5 Responses to “1/0 = 0, really!”

1. pdf23ds Says:

I knew I was right! Take that, 6th grade teacher!

2. pdf23ds Says:

I think it’s worth noting that a different construction of the naturals would yield a different result for 1/0. For instance, if {{}} were 0, and {{{}}} were 1 and so on, then 1/0 wouldn’t correspond to any natural number.

3. slawekk Says:

different construction of the naturals would yield a different result for 1/0

I would say that the result for 1/0 would be the same: the empty set (only it would not be equal to any natural number if we start natural numbers from $0 := \{\emptyset \}$). To change the result of 1/0 one would have to fiddle with the definition of function application.

4. The next generation of proof assistants: ten questions « Formalized Mathematics Says:

[…] To be honest, I don’t understand the question. One remark however: I don’t think the statement is disprovable in Metamath as Wiedijk claims. In ZF set theory the situation is  that to define the value of a function at some point of its domain we first define what is the image of a set by a function. Having that we define the value of the function at  as the union of the image of . If is a function and is in its domain then the image is a singleton and the union extracts its only element (recall that in ZF). When is not in the domain of however, (like zero is not in the domain of division), the image of is empty and so is its union. Thus is the empty set, which is zero of natural numbers. So in a way, you can prove that (except that zeros on the right and left hand side are typically different things). I write some more about that in another post. […]

5. IsarMathLib 1.7.1 « Formalized Mathematics Says:

[…] category. The first is related to the “1/0=0″ story that I talk about in another post. Proving the theorem that states that was a little bit more involved that I had thought. I had to […]