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.



Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s

This site uses Akismet to reduce spam. Learn how your comment data is processed.

%d bloggers like this: