1/0 = 0, really!

Let be a field. We can define division as a function in in the obvious way. Now, what is the value of that function on the pair ? In general, what is if and ? Is it undefined? How do we define “undefined” ? Surprisingly, in ZF 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 because the pair is not in the domain of division. Why then we can write ? 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 , but the zeros on both sides denote different things.

Math Wiki news

In a recent post to the vdash mailing list by Herman Geuvers there is an information that the application by the team at Radboud University Nijmegen, NL with participation from six other universities for funding of development of formalized math wiki was turned down. That is rather unfortunate. I didn’t like some of the specifics of the plan, but I think software created by the project, if released under free license could be reused to create something better. I am not too surprised that they didn’t get the money. Getting it was about as likely as EU funding the development of Wikipedia before it existed (I can image what a typical EU official would think about the idea of “online encyclopedia that everybody can edit”).

The Great Bailout

I have not seen such disconnect between the information provided by the media and what can be found out from other sources since I was watching TV news in communist Poland more than twenty years ago.

First of all, failures of financial systems happen often enough that by now there are empirical data that allow to evaluate different ways of resolving them. Government buying of bad assets consistently proves to be the one that is the least effective and the most costly to the taxpayers. There is no dichotomy “either bailout of economic disaster”. There are other alternatives that work better and don’t cost that much money from people who didn’t benefit from the profits of investment banks.

As an angry renter (yes, I know who finances that site) I suggest another data point to consider: inflation adjusted house prices since 1890. And for entertainment the roller-coaster version of that.