I haven’t updated this blog for a while, so I decided to try to break the writer’s block by posting a couple of quotes from the formalized mathematics stuff I read recently.

There was a discussion initiated by James Frank in November last year on the Isabelle mailing list about problems with making mathematics formalized in HOL similar in notation and terminology to the standard (informal) mathematics. The main difficulty here is that standard mathematics uses set theory notation, so obviously something based on type theory has to look different. This lead to a discussion what might be the reasons of doing formalized mathematics in simply typed HOL rather than set theory. Josef Urban expressed the following opinion:

I do not think that there are good pragmatic automation-related reasons for persuading mathematicians to work in HOL instead of ZF. Given the very low penetration that formal mathematics has so far among mathematicians, I think it would not hurt the formal systems to go where the mathematicians are.

with which I fully agree.

In the same thread Steven Obua announced the ProofPeer project – a cloud-based social network interactive theorem proving system. (That is probably the the highest concentration of buzzwords in one sentence that I ever wrote.) The alpha launch is planned for summer 2012. He recently published a paper with more details about ProofPeer.

On the subject of types vs. sets as a foundation I recall a funny cartoon that I found on a LtU thread related to this.

Back in 2008 Freek Wiedijk wrote a nice article on “Formal Proof—Getting Started”. Here is my favorite part of it:

In mathematics there have been three main revolutions:

• The introduction of proof by the Greeks in the fourth century BC, culminating in Euclid’s Elements.
• The introduction of rigor in mathematics in the nineteenth century. During this time the nonrigorous calculus was made rigorous by Cauchy and others. This time also saw the development of mathematical logic by Frege and the development of set theory by Cantor.
• The introduction of formal mathematics in the late twentieth and early twenty-first centuries.

Frank Quinne’s article “A Revolution in Mathematics? What Really Happened a Century Ago and Why It Matters Today” in  the January issue of Notices of the AMS is devoted to the second revolution. Here is a quote:

As the transition progressed, the arguments became more heated but more confined. At the beginning traditionalists were deeply offended but not threatened. But because modern methods lack external checks, they depend heavily on fully reliable inputs. Older material was filtered to support this, and as the transition gained momentum some old theorems were reclassified as “unproved”, some methods became unacceptable for publication, and quite a few ways of looking at things were rejected as dangerously imprecise. Understandably, many eminent late nineteenth-century mathematicians were outraged by these reassessments.
Meanwhile, very high reliability has been achieved in mathematics without drawing attention or having significance attached to it. The axiomatic-definition approach also made mathematics more accessible. A century ago original research was possible only for the elite. Today it is accessible enough that publication is required for promotion at even modest institutions, and an original contribution can be required for a Ph.D.

It is striking for me how well this describes the situation with the third revolution. The analogy extends also to the sort of democratization of mathematics that machine verification makes possible.

### 13 Responses to “Recently read”

1. JF Says:

Slawomir, I’ve sat on this post of yours because it’s always easy for me to give an opinion, and I’m trying to keep my opinions on blogs to a minimum.

More importantly for me, in this comment, is to get to the part about Isabelle/ZF and proper classes.

First, though, to a certain extent, the Isabelle people, in particular Larry Paulson, Steven Obua, and you, have gone where the mathematicians are. There are Isabelle/ZF and Isabelle/HOLZF.

I got bent out of shape because HOL math is inseparable from HOL functions, but nobody said I had to use HOL. If a person doesn’t start at the bottom, the HOL code can be deceptive, because Isar does a good job of allowing a person to use mathematical notation, but now I know it’s a different model, so I don’t care now.

Again, there’s the more traditional modeling of sets available with Isabelle/ZF and HOLZF, but if mathematicians don’t jump on the bandwagon, what can you do?

As far as your IsarMathLib bandwagon, I would jump on it, but I don’t know what dead ends there are going to be. If I spend three or more years working to get good at using Isabelle, I want to end up in a no-lose situation, which I’ve decided, as a worst case scenario, would be proficiency in Isabelle and ML for the purpose of functional programming, which is where all this started anyway: Mathematica led to Haskell which led to Isabelle. I figure that HOL is good for implementing discrete math algorithms, at the very least. If I get more, that’s great.

This leads to the subject of a possible dead end with Isabelle/ZF: the need for proper classes.

It was a combination of your post here, and the announcement of The Zermelo Proof Checker, by Jeremy Bem on the HOL4 mailing list, that got me thinking again. For a short period, I entertained the idea of working on Isabelle/ZF and Isabelle/HOL together, but no, that’s not workable.

From http://zermelo.org/manual.html, Bem explains that he uses Von Neumann–Bernays–Gödel set theory, and he writes:

Mathematicians know that the informal view is not quite that all mathematical objects can be viewed as sets. Occasionally one encounters objects, such as the collection of all vector spaces, which are regarded as too large to be sets in the usual sense. It is routine, for example, to consider such collections when working in the area of mathematics called category theory. Despite their size, it is possible to treat these collections as objects and there exists standard language for doing so: one speaks of the class of all vector spaces.

Larry Paulson explains in logic-ZF.pdf, page 19 why he chose Zermelo-Frankel over Bernays-Godel set theory, which is to prevent having to do certain tiresome proofs, and he writes:

In BG, both classes and sets are
individuals; x \in V expresses that x is a set. In ZF, all variables denote sets; classes are identifed with unary predicates.

From the wiki article on proper classes:

ZF set theory does not formalize the notion of classes. They can instead be described in the metalanguage, as equivalence classes of logical formulas… Because classes do not have any formal status in the theory of ZF, the axioms of ZF do not immediately apply to classes.

Based on my limited knowledge and the wiki article, I gather that though Paulson says that you can use classes in ZF, you get them in a very limited manner; you get classes, but no ability to operate on them. That’s what it sounds like to me.

Additionally, from Steven Obua’s Partizan Games in Isabelle/HOLZF, page 3, he writes:

Therefore,
Partizan Games do not form a set but rather a proper class.

The implication is that Isabelle/ZF is not suitable for his needs.

Finally, from An Introduction to Mathematical Logic and Type Theory, by Andrews, page xii, he writes:

Axiomatic set theory achieves consistency by restricting the Comprehension Axiom and introducing the distinction between sets and classes. Mathematicians often find this distinction unnatural, ignore the technicalities about existence axioms, and leave it to the specialists to show that their reasoning can be justified.

This last quote supports my claim that most mathematicians haven’t ever studied axiomatic set theory. You can get practical and go high, or you can get compulsive and go low, but only the best with long careers end up doing both.

The consequence of all this is the possibility of dead ends because of the lack of proper classes.

With pencil and paper proof, if your basic logic is good, and your idea is valid, then someone else can get compulsive, if they want to, and formally add more rigor to it, or fix it.

But with a theorem prover, the theorem prover is going to enforce the axioms. If you hit a dead end because of the limitations of the logical framework you’re working under, you’ll either figure out why, or you won’t. Even if you figure out why, it could be a bad situation.

I’d ask you to port IsarMathLib to HOLZF, along with the applicable parts of Isabelle/ZF, but I don’t know enough to know what kind of “more perfect solution” that would be. That’s a joke, of course, the porting part, though not the part about me not knowing enough. However, you can take the porting part serious if you want to.

I’ll got back to trying to stay low profile. These long comments take a lot of time to write.

2. JF Says:

On the other hand, your IsarMathLib may be the best place for me to find a consistent set of examples to show me how to do structured proofs, to show me how to use the methods.

This comment here is a result of having, hours after I wrote the last comment, tried one more time to find a theorem assistant to give me a better learning path.

I failed once again, so I keep coming back to Isabelle.

I go back and forth between hating theorem provers, and thinking that they’re wonderful. The documentation to teach me about them is non-existent, or it’s spread out all over the place.

Additionally, the fact that almost exclusively, coders, for any of these theorem assistants, write the proof code with no comments to explain the logical reasons for the steps; that’s utterly ridiculous to me. Who do they think is going to be interested in reading 1000 pages of nothing but line after line of code?

Mathematical proofs are supposed to teach, and be a work of literature. Trying to get pleasure out of reading Coq or Isabelle or HOL4 or any of these theorem assistant proofs would be like trying to get pleasure out of reading the Windows 7 OS code.

I’m gonna keep calling mathematicians Luddites for not working to automate the proof process, but at times like this, I understand why theorem assistants haven’t gained widespread acceptance. At this point, they’re not used to teach a person anything when it comes to math.

The process of writing proofs and teaching is highly integrated in the math world, but in the computer science world, their thrill only comes from that final step in which the message flashes on the screen and tells them, “Compiled successfully.”

For me, there’s a carrot on a stick, so I guess I’ll eventually hunker down and painfully and slowly learn this stuff.

This site shows that you might have a mailing list:

http://savannah.nongnu.org/projects/isarmathlib

I said I didn’t like mailing lists, but that’s because I wasn’t using a filter for my email client in the past.

I don’t know what I’ll do, and working through the Isabelle tutorials is going slow for me.

I don’t think asking questions on math.stackexchange.com would be good in general. On those sites, I don’t think they appreciate short, cryptic questions and answers between two people, and everything is going to get voted on.

On the other hand, if you want to advertise what you’re doing, using that site could be a way to pique interest in people.

3. slawekk Says:

I wouldn’t worry about “hitting a dead end” just because Isabelle/ZF implements the version of ZF that does not have classes. For a long time I didn’t even know there are other versions (until I attempted a translation from Metamath that uses classes). There is no dead end, at worst there may be some inconvenience in expressing some concepts. Having all objects of the same kind (set) simplifies things.
I think you also overestimate the effort needed to learn writing proofs using Isabelle. Indeed years are needed to learn mathematics, but then learning Isabelle is more like three months of additional effort rather than three years. Learning math by reading and writing formal proofs is an interesting way, but I don’t think anybody has attempted it yet. I am curious myself how it would go. I agree with you that formal proofs written without any informal commentary are useless for this purpose.
One big disadvantage of a mailing list is that math notation is not available. It is very inconvenient to discuss math without having math notation. Some public forum with LaTeX support would be good. I like your idea of using StackExchange. If they complain, another possibility is to set up a wiki on wikidot.com .

4. JF Says:

FIRST PART THAT YOU CAN SKIP

So I’ll quote you on “there is no dead end”, and hold you to it. But that’s a joke, because no one can know what the dead ends are or aren’t, unless they’ve formally proved what the dead ends are or aren’t for a particular theorem prover.

As far as being able to learn math from a proof, In my mind, I was relating that to the idea that in mathematical writing, people have an expectation that they’re going to be able to learn something that they don’t know from studying a proof. On mathoverflow.net, they emphasize that even when you ask a question, the way that you ask it should be informative:

So when you ask for the help of those who know more than you, please also extend a hand to those who know less than you by explaining why you are asking the question.

A person throwing out cryptic, mathematical statements that only serve his or her purpose is obnoxious to people.

A decently explained proof is the completion of something like a three or four step process: an informal discussion, an example, the formal statement of the theorem, and the proof. It’s the understanding of the proof that takes you to a different level of understanding. The scope of mathematical writing runs the gamut, but the more unfriendly an author gets, such as going to a pure theorem, proof, theorem, proof, theorem, proof format, the less their book is going to be read.

Additionally, if an author gets to a point where they’re not filling in huge logical steps in their proofs, it becomes totally unacceptable to the mathematical masses. The use of “by auto” and other automatic proof methods is the equivalent of a textbook author not providing a proof, or providing a cryptic proof. The level of mathematics in a book will determine what steps can be left out, but still, you don’t get to say, “Proof: It’s true. Figure it out yourself.”.

As it is, to learn an Isabelle statement applied to math, I have to understand the math to figure out the logical reason underlying why the person used that statement. If I already knew how to use Isabelle, I would just start proving the standard, textbook theorems I want to prove.

For me, learning Isabelle can’t be a three-month process. Part of my complaint is people’s use of commands like “by auto”. For me to be able to fill in the gaps of “by auto” and “simp”, I’ll have to know where the theorems are that those methods use. That will require me going through a certain amount of foundational code.

Additionally, I need to learn how to use natural deduction and the Isabelle methods that go along with that, which all starts down in Isabelle/FOL. The fact that Isabelle/ZF and Isabelle/HOL are based on natural deduction is part of what keeps me coming back.

The idea of matching conclusions of theorems with hypothesis is something I like. Backward proof is not considered good form when writing up a formal proof, but it’s an important part of proving math. You figure a proof out by going backwards, many times, and then you write it up forwards style. Not knowing a lot, it still appears to me that natural deduction tactics are simple, but yet potentially very powerful.

SECOND PART

I don’t really like all that social-networking style voting, especially because of what I see on mathoverflow.net. Math.stackexchange.com is more tolerant of questions, but even on that forum, I suspect you end up with math supercops wanting to police everyone. I haven’t been watching math.stackeschange to know how bad it is.

I can get pedantic with the best of the pedantics, but if someone gets snippy with me, then I want to go inflammatory on them, and that’s not good on a site like that. These days, I don’t like to see my name out on the web much, so you might see me ask questions under a pseudonym, not that JF is a pseudonym, though it’s not my full name. I don’t even like the idea of opening up an account on stackexchange.com, but a man has to do what he has to do to get ahead in life.

THIRD PART

You have to understand that I have no interest in making any contribution to IsarMathLib. I only care to learn from what you’ve written, both in how to use Isabelle, in reviewing math I’ll be familiar with in IsarMathLib, and learning math I don’t know as a result of trying to figure out a proof.

All I’m interested in right now is proving theorems in textbooks that I’ll be studying. Eventually that’s supposed to lead into something original, but that’s not of ultimate importance to me. If something can be extracted out of what I do, or if I want something I don’t know how to get, and it causes you to add definitions and theorems to IsarMathLib, then that’ll be good, but having that happen is not my primary goal.

I’ll be marking up what you’ve done to suit my purposes. Renaming definitions and theorems, maybe. Expanding steps in proofs to make the logic more clear, hopefully. Anything to help me out and put what I study into a more verbose format.

Creating a fork based on your IsarMathLib wouldn’t be desirable for a number of reasons, but forks are a fact of life, because people want what they want, the way they want it. ProofPeer is a fork off of both Isabelle and HOL-Light (I guess I’m using “fork” in the right way). I wouldn’t want to create a fork off of IsarMathLib, but I want what I want. I just tell you these things.

This is all lofty talk, but after I get laid off from my current job, I expect to make faster progress. I should start making some progress even now. This all assumes I won’t look again in the Isabelle/ZF files and again say, “Forget this. I’m not going this route.”

I hope to get out of “opinion mode” here and go purely technical. Expressing my opinions and talking about the future suck up my time in a bad way.

5. JF Says:

My first statement in the last comment suggests that I know for sure that we can’t know that there’s not a dead end in Isabelle/ZF, because ZF doesn’t formally have proper classes. I don’t know that at all.

I’ve only barely scraped the surface of axiomatic set theory, but as I understand it, the axioms absolutely prevent you from building certain types of sets, otherwise, you would get a paradox, such as Russel’s paradox. I barely went through a certain exercise which showed that one of the axioms, call it Axiom X, prevents you from creating a set of sets which don’t contain themselves, or whatever it did, it prevented Russel’s Paradox. I’m too lazy to look that up again…

Actually, I’m not, and it’s the Axiom Schema of Specification, referred to as the Axiom of Comprehension by Andrews, who I quote in my first comment. Not allowing unrestricted comprehension prevents the paradoxes. Here’s the wiki link:

http://en.wikipedia.org/wiki/Axiom_schema_of_specification#Unrestricted_comprehension

I’m not worried about axiomatic set theory at this time, but I would like to make a particular request of someone familiar with Isabelle, where my request is in the context of the quotes above about proper.

The request would be this:

Can someone please give me an example of a theorem involving a proper class that’s implemented in Isabelle/ZF?

I don’t make that request, because I don’t want to be a pest anymore than what I am, and who says anyone will answer it? But if you or Larry Paulson created a little example involving a proper class, then that would make me feel better about the future. I assume everyone has higher priorities than making me feel better about the future.

If everything is required to be a set, then certain sets can’t exist, which puts limitations on what kind of objects you can have that contain sets. That sounds to me like a dead end. The other possibility is that it ends up being such a hassle to have these kind of objects, that it’s not worth using them in ZF set theory.

6. JF Says:

Well, I think I’ve wasted your time some. I have to make an attempt to go the HOL route. It’s a lonely, painful route, but that’s the nature of math anyway. If you were to be inclined to delete all these comments, that wouldn’t particularly bother me.

7. JF Says:

I am like a wave, driven by the wind and tossed. It’s true I may be wasting your time, but I’ve come full circle in my searches about proper classes, this time due to searching for books on NBG set theory. So, we can ignore, for the moment, my last comment, and delay the deleting of all of this.

Not wanting to talk unintelligently about what I don’t understand, I had set aside part of what I originally wanted to ask about as a possible way to get proper classes with ZF.

In the wiki article I linked to in my first comment, it says this:

Because classes do not have any formal status in the theory of ZF, the axioms of ZF do not immediately apply to classes. However, if an inaccessible cardinal κ is assumed, then the sets of smaller rank form a model of ZF (a Grothendieck universe), and its subsets can be thought of as “classes”.

It seems to indicate that by simply adding an axiom, we get to mess around with classes like we get to mess around with sets, all in ZF or a model of ZF.

I thought, can it be that simple? But then I also asked, “What’s a model of ZF?”

Grothendieck unverses, models of ZF, that’s too many things to ask about, so I decided.

But, there is this link:

http://mathoverflow.net/questions/6423/set-theory-for-category-theory-beginners

And an arXiv article linked to in one of the answers, the pertinent sections being 6, 7, and 8:

http://arxiv.org/pdf/0810.1279v2.pdf

Those indicate that maybe I was on the right track. I think I’m going to write up a question for math.stackexchange.com to ask about these things. Maybe it’s so simple as adding an axiom assuming an inaccessible cardinal, whatever that means.

I don’t really like putting all these lengthy comments on your blog, but these type of activities can help me work through things sometimes. That regrettable thread I started on the mailing list helped me think some things through faster than I would have without it.

8. slawekk Says:

The truth is, I don’t know much about classes. As I said, I never used them. I know an additional axiom about inaccessible cardinal allows to do some limited sort of category theory inside ZF.
There is no way to formulate a theorem that uses classes in Isabelle/ZF as Isabelle/ZF implements the version of ZF without classes.
I can tell you how I understand the statement that classes can be modeled by predicates. This is very simple: suppose you want to prove a theorem that applies to all groups. In a foundation where classes are allowed you define the class $\mathbb{G}$ (consisting of pairs $\langle G,P \rangle$ where $P:G\times G\rightarrow G$ is a binary operation on $G$) of all groups and when you want to formulate a theorem about groups you put $\langle G,P\rangle \in \mathbb{G}$ in the assumptions.
When you are not allowed to use classes, you define a predicate “is a group” that says what it means that a pair of sets is a group (something like “$\langle G,P \rangle$ is a monoid and all elements in $G$ have an inverse with respect to the operation $P$, or some alternative definition) and then instead of writing “$\langle G,P\rangle \in \mathbb{G}$” you write “$\langle G,P\rangle$ is a group”.

9. JF Says:

Thanks for the explanation. It sounded more difficult than only needing a definition and adding words such as “Let ___ be a ___” to your hypothesis. Maybe there are some subtleties, but it appears that you lose all the set operations when it’s neither a set or a class, but a predicate.

My quote above by Andrews is what makes me paranoid. Naive sets rule, and he indicates that people occasionally define something as a set and violate the Axiom Scheme of Specification. If I’m trying to duplicate math where that has happened, then maybe there’s an easy way to fix the problem with the right framework.

I have to check out of here permanently. I can only use what people like you produce. I forget that because I’ve been in a dormant state, having had to work.

I’ll be working soon to try and produce some social-moral-political commentary-music-entertainment. That doesn’t mix well with the professional scene.

However, out of this series of comments, I think I’ve gotten one answer and one future possibility.

It appears that NBG set theory is not a practical solution to the “more than a set” problem. If you get too far from imitating naive set theory, it’s probably a clumsy solution.

I put the idea about inaccessible cardinals in the back of my mind, as a future possibility.

Happy proving grounds.

10. Joe Rusky Says:

You don’t have a massive number of posts, but there are enough that it would be good if you had an archives widget in the sidebar.

Also, you can list the post titles to every post by using a WordPress shortcode. The instructions are on this page:

http://en.support.wordpress.com/archives-shortcode/

You would put the command “[archives]” in a new page, then drag a text widget into the sidebar, and then put a link to the page in the text widget. That’s one way to do it.

Or, you would use a template that provides links to your pages (pages rather than posts).

It’s just a suggestion.

11. slawekk Says:

Good ideas, thanks.

12. Jim Kingdon Says:

One of the comments asks whether anyone has taught themselves math by writing and reading formal proofs. While I had an undergraduate math education before getting into formal proofs, I have learned significant areas from reading metamath ( http://metamath.org/ ), writing proofs at http://www.wikiproofs.org/ , reading coq geometry proofs of Julien Narboux at http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.158.8614 and perhaps a few other more minor sources.

Things I have learned include: (1) doing propositional logic via axioms and proofs, rather than truth tables (e.g. translating the propositional logic chapter of Principia Mathematica to a formal proof system which is metamath-like in the sense of not having it built in), (2) intuitionistic propositional logic (if there is a good textbook on this, I haven’t yet found it, but as long as I start from a correct set of axioms, I feel like I won’t go too far astray), (3) the difference between a class and a set (hinted at in my undergraduate days, but which actually has subtleties that come out, at least for me, much more in a formal proof system than in any amount of trying to explain it in terms of concepts), (4) predicate logic: I knew very little of this, beyond what the average non-logician uses in an intuitive way without trying to explain it in detail. Now I have proved enough predicate logic to use in, say, arithmetic or set theory, from two different axiomizations. (5) Formalizing geometry (in the point/line style of Euclid’s elements or Tarski’s geometry axioms). When I started I had no idea how the diagrams of high school geometry could be translated to a formal language with predicates like “x is between y and z” and “x y is congruent to z w”. (6) Logical concepts like the deduction theorem (although I haven’t tried to express these in a formal proof system, or even read the work of people who have, it is hard to work in a system like metamath without gaining some insight into what kinds of informal reasoning translate into what kinds of formal proofs).

I’m happy to use a relevant (non-computer-formalized) textbook, so I wouldn’t say my learning has been exclusively by means of formal proofs, but the bulk of it has been focused on writing formal proofs and many of the source materials I have been reading are formal proofs.

13. ProofPeer | Formalized Mathematics Says:

[…] is a project to create a cloud-based social network interactive theorem proving system. I wrote about it a year ago. The project looked dormant since about July, but now it got funding and is […]