IsarMathLib 1.7.1

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 $K\times K\setminus \{0\}$ , 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 $(X_1,\tau_1)$ and $(X_2,\tau_2)$ and we partition $X_1$ into two sets $U,V\subseteq X_1, \ U\cup V=X_1$ , both open (or both closed), and a function $f:X_1\rightarrow X_2$ is continuous on both $U$ and $V$ , then $f$ is continuous. The version in IsarMathLib is bit different, stating that the collection of open sets $\{U \in \tau_1 : f|_U \text{is continuous}\}$ 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 $\{U \in \tau_1 : f|_U \text{is continuous}\}$ forms a topology, $\emptyset$ belongs to it, i.e. $f|_\emptyset$ is continuous. But $f|_\emptyset$ is in fact $\emptyset$ 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:

Be the first to like this post.

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.

Formalized Mathematics

IsarMathLib 1.7.1

Like this:

Leave a Reply Cancel reply

Follow “Formalized Mathematics”