Checking for new stuff on Freek Wiedijk’s home page I stumbled upon slides of his recent talk given at the Workshop on Logical and Semantic Frameworks in Natal, Brasil. He poses there ten questions about how the next generation of proof assistants should look like. In this post I want to give my answers to those questions.
Should the next generation of proof assistants be based on ZFC set theory?
Short answer: yes, of course. Long answer: no, why would we want to limit the proof assistant to one foundation? The next generation of proof assistants should be generic enough to be able to support many logics. Isabelle is like that now and so is Metamath. As the standard foundation for modern mathematics ZFC should be well supported, but alternatives may be interesting for purposes other than pure mathematics or just for experimentation.
Should the next generation of proof assistants have an advanced type system?
One possibility mentioned in the slides where types are a layer on top of an untyped foundation is probably the best idea. Having some type system would simplify proofs of facts about how set membership changes when functions are applied. In IsarMathLib proofs of such facts have to be done explicitly (using standard Isabelle’s apply_funtype lemma). It is not difficult but repetitive and boring.
Should the next generation of proof assistants take partiality seriously?
To be honest, I don’t understand the question. One remark however: I don’t think the statement is disprovable in Metamath as Wiedijk claims. In ZF set theory the situation is that to define the value of a function at some point of its domain we first define what is the image of a set by a function. Having that we define the value of the function at as the union of the image of . If is a function and is in its domain then the image is a singleton and the union extracts its only element (recall that in ZF). When is not in the domain of however, (like zero is not in the domain of division), the image of is empty and so is its union. Thus is the empty set, which is zero of natural numbers. So in a way, you can prove that (except that zeros on the right and left hand side are typically different things). I write some more about that in another post.
Should the next generation of proof assistants take category theory seriously?
Category theory can be done based on ZFC (with some additional axioms) and there is some work on formalization in Isabelle/HOL. However, the question is, can we treat category theory as foundation which we use to formalize mathematics? I would really like someone to make a serious attempt at implementing category theory in some proof assistant starting from its axioms and proving some typical theorems. Both failure and success of doing so would be very instructive. Until that happens, my answer is no.
(Btw, there is an interesting discussion on Math Overflow about the role of the Replacement Axiom in category theory. Some people think it’s necessary, others find its consequences unacceptable. It seems that there is some overlap between those two sets (categories?) of people. This is similar to the situation with the Axiom of Choice in set theory some hundred years ago. )
Should the next generation of proof assistants be based on a logical framework?
Yes. The reasons are well explained on the slides.
Should the next generation of proof assistants have a self-verified kernel?
I don’t think it is essential. It would be good if the core system was short enough to be convincing to humans (like Metamath is) and possible to verify by hand. That is the important part. The self verification is not worth much – as Wiedijk notes “if it is incorrect it can falsely claim to be correct”. In addition, there is some design tension between building a system for doing formalized mathematics and software verification. These tasks are similar in theory, but quite different in practice from the user perspective. If we want a better proof assistant for formalized math (and I do), we don’t want the designers to focus on software verification.
Should the next generation of proof assistants be programmed in itself?
It would be better if it was not. The reasons are explained in the previous answer.
Should the next generation of proof assistants be competitive with commercial computer algebra?
Probably not. Maybe next after that.
Should the next generation of proof assistants use a declarative proof style?
Yes. But the most important is not how the proofs are written but how they look like after being processed by the presentation layer. I think this is the killer app for formalized mathematics: having a faithful semantic representation of mathematical knowledge in a machine that can be studied by humans. “No mystery” hyperlinked proofs that can be searched, viewed at desired level of detail and refactored. Imagine the possibilities.
How should the next generation of proof assistants be arrived at?
Better question is how can they be arrived at. I don’t know the answer. Such things typically come from academia. The problem is that the products of Computing Science departments (where the knowledge necessary to create the NGoPA is) are biased towards software verification, thus can not improve in the “better match with existing mathematical culture” area. Mathematics departments are simply not interested in formalized mathematics.
I have a fantasy sometimes that a very rich person just throws a large amount of money at the problem for pure love of mathematics. Something like that did happen for poetry, so why not for formalized mathematics?
Tags: formalized mathematics