I have released version 1.7.1 of IsarMathLib. There are two small topics I added, both in the “weird math” 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 define the notion of division in fields as a function on , then notation for it. I don’t think I cheated here but the truth is I did make an effort to make the theorem *look* like the one I wanted to prove. This brings up the question: what if I made a little more effort and manipulate notation so that a theorem appears to mean something different that it really does? For example it is quite easy in Isabelle to change the notation to print “True” as “False” and prove a theorem that appears to show inconsistency in ZF.

Freek Wiedijk’s paper formalizes this question. Back in January there was also a long thread on the Isabelle mailing list where people expressed varying opinions on how serious the problem is.

Another small piece of formal math that I added in this release is a chapter in the *Topology_ZF_2* theory on the pasting lemma. The classical pasting lemma states that if we have two topological spaces, say and and we partition into two sets , both open (or both closed), and a function is continuous on both and , then is continuous. The version in IsarMathLib is bit different, stating that the collection of open sets forms a topology.

Surprisingly from this we can conclude that the empty set (which in ZF is the same as zero of natural numbers) is continuous. Here is how it happens: since the collection forms a topology, belongs to it, i.e. is continuous. But is in fact and we get that zero is continuous. Ha Ha.

I would like to emphasize that I do *not* consider facts like this as demonstrating that ZF set theory is not a suitable foundation for formalizing mathematics (as some people interpret). It is just fun and games that formal math allows and I am sure other foundations also have their unintuitive corner cases.

### Like this:

Like Loading...

*Related*

Tags: weirdmath

This entry was posted on May 13, 2011 at 9:32 am and is filed under announcements, IsarMathLib releases. You can follow any responses to this entry through the RSS 2.0 feed.
You can leave a response, or trackback from your own site.

## Leave a Reply