This page was started by raph in response to some discussion about Mizar in comparison to metamath. I'm writing my impressions based on my (admittedly incomplete) knowledge of some of these other systems and (equally incomplete) impressions about the needs of the HDM project. Feel free to clarify either or both.
Also, a good place for more information is Freek Wiedijk's comparison of some of the major theorem provers out there.
Metamath, and its offshoot Ghilbert, are already rightfully in the running as a basis for the formal system of hdm. There's already a lot of discussion on the metamath page, which maybe should get refactored to here, but I won't do that right now.
Mizar, of all the provers, has by a large margin the widest userbase and largest library. It's also particularly strong in the sort of mathematics that mathematicians do in their daily work.
Of particular interest to the hdm project is the Journal of Formal Mathematics, which is an extensive repository of theorems presented as a traditional, refereed mathematics journal.
Mizar was designed with a particular eye toward making theorems readable. The syntax is based on natural language, with stereotyped patterns of justification and steps. This approach depends on fairly sophisticated theorem-proving logic in the verifier.
Originally, Mizar used an 8-bit character set closely patterned after the IBM PC's. The formal Mizar articles now appear to be in essentially ASCII. There is an automated conversion to TeX, but from what I can tell it is only available as a server-based application, and the code is not public.
Perhaps the single biggest drawback of Mizar is the difficulty of implementing an independent verifier. The official Mizar version is not free software, although it is available as "free beer". In addition, it appears very difficult to adapt Mizar to being "logic agnostic". The verifier seems to implicitly encode classical logic, and the standard axiom set includes a very strong superset of ZFC. As such, there are likely to be significant technical barriers to translating Mizar theorems into other formalizations.
HOL is another formal system with a long tradition, significant userbase, and rich library. The central idea of HOL is that a proof is a program. HOL is written in a language so strongly typed (ML) that it is possible to define a type that contains only valid theorems. The only way to construct values of this type is to use axioms and inference rules that exist in the "kernel" of the system.
The ideas of HOL are fairly simple, and, given an appropriate programming language, doing an independent implementation is not particularly difficult. Of course, implementing an entire ML language, library, and runtime environment is far from a trivial task, so a completely "from scratch" implementation is daunting to say the least. There are several good implementations of HOL and variants, of which Isabelle and NuPRL are particularly notable.
While HOL has a built-in axiom system (considerably weaker than ZFC set theory), it is much better at logic agnosticism than you might think. For example, NuPRL? is based on constructive logic, while the original HOL is based on classical. Pavel Naumov has done groundbreaking work in porting proofs between HOL variants, in particular the Isabelle to NuPRL? direction.
An important technical problem in translating HOL proofs to other, weaker, logics is its reliance on the Hilbert epsilon operator. Many instances of its use can actually be replaced by the much weaker iota (or definite description) operator, but even just identifying which instances can be so converted is tricky in a large library. Metamath contains the axiom of choice but not (directly) the epsilon operator. Again, it is possible to mechanically convert proofs to eliminate the epsilon operator, but this conversion is likely to be quite tedious. There's some discussion of this linked off the [Ghilbert main page, and Norm Megill has also done followup work on Emulating Hilbert's epsilon in ZFC (pdf link).
Internally, HOL proofs and terms are represented as S-expressions, but these are considered unfriendly enough that all real work is done through an infix parser and prettyprinter. I am unaware of any good automated conversion to TeX?, but would not be surprised if such a thing exists; there should be no serious technical barriers.
Not surprisingly, the biggest weaknesses of HOL proofs are inherited from the underlying progamming environment. The text of a proof is somewhat brittle and unportable, as it depends on compatibility with the underlying ML implementation. I personally find HOL proofs to be close to unreadable, although there has been interesting work on supporting a Mizar mode for HOL, which allows for proofs much closer to the "mathematical vernacular" than traditional HOL. Isar is another similar hybrid, this time of Isabelle and Mizar. A relatively recent development is the IsarMathLib, a project to create a readable library of theorems in the Isar system, based on first-order logic and ZF set theory.
Equally unsurprisingly, the biggest strengths of HOL derive from the power of the underlying programming environment. Tedious and repetitive aspects of proofs are easily automated, and the standard library contains a number of tools (BOSS and Meson are two names you'll come across often) for automatically searching or theorem-proving within logic fragments such as propositional calculus. HOL is also a pretty decent four-function desk calculator out of the box, and it is straightforward to write one's own extensions to HOL's calculational ability.
In a profound sense, HOL is capable of short proofs. More formally, if a proof exists, then it is possible to encode it into an HOL proof of size equal to its Kolmogorov complexity. That property is not true of Metamath / Ghilbert, and for example the correctness proof of the product of two arbitrary n-digit numbers will O(n^2) using the straightforward approach. (Or O(n^lg 3) using Knuth's recursive application of Karatsuba multiplication, but that's for complexity nerds - the point is that it's still asymptotically larger than HOL's O(n) size proof, or even O(1) if the numbers themselves are procedurally generated).
HOL has a tradition of being very free software. The mainline HOL branch is released under a BSD-style license.
On the page Ghilbert and HDM, I said it would be useful to do a "comparative linguistics" for various provers. The additional detail is that this probably boils down by in large to building a system for translation – such as is possible – between the various systems. This requires a "hub" language, as it were, and a bunch of translation "spokes". (So, if I am to be accused of trying to reinvent the wheel, at least it can't be said that I didn't see it coming.)
The additional details come down to something like "user preference", which could also be interesting to study from a linguistics standpoint, but which is presumably incidental to the translation problem.
So, I'm filing a request here for more information about the state of the art computer/math platform inter-operability through translation.
--jcorneli Aug 16, 2006
Good question. I think it's deserving of its own page, so I'm making one for Translation Systems and adding what I know of the answer there. --raph
There is a discusson on Usenet about exporting Isabelle proofs into "the most elementary possible inferences," which the thread originator specifically compares to Metamath. This kind of export would, of course, greatly facilitate proof translations.
As an aside, another poster offers the following opinion: "I would consider the Metamath format slightly low-level, with adhoc handling of bound variable scopes; lambda calculus provides a more abstract and clean notion of variable binding and substitution." I think this is an interesting point of discussion. The language of set.mm was chosen to match standard logic notation as much as practical. Its development essentially formalizes, more or less directly, the proofs in standard logic and set theory books. None of these proofs use or make any reference to lambda calculus. In general it is atypical for a math textbook (such as for analysis, topology, abstract algebra, etc.) to make any mention of lambda calculus, unless the book is about lambda calculus itself. So, how does lambda calculus fit in with ordinary mathematics, outside of the computer science and formalized math world? Is it an advantage or disadvantage in terms of attracting mainstream mathematicians to formalized math?
– norm 17-Jan-2006
I'm a lambda fan, and I think that lambda (or things like it) are the only way I know of to be clear about scope. hcode is certainly going to be informed by the lambda calculus, and also be designed to capture math as it is done by your everyday mathematician. I don't think this is a contradiction; but it will require some care to pull it off in a way that everyone can enjoy. --jcorneli
I think the remark about lambda calculus in Isabelle was related to internals rather than the proof language that is exposed to the user. I have been using Isabelle for about a year and I still don't know what lambda calculus is (although I am not proud of that). Requiring a user to know about lambda calculus would not attract mainstream mathematicians. --slawekk
I'm not a mathematician but when I try to speak of metamath with one of my friend who is much more learned in mathematics ( can I say that in english ??? [yes, but emphasis is on second syllable of "learned", so learn\`ed --jcorneli]) than me I'm always very amazed he hardly knows anything in propositional calculus and absolutely nothing in predicate calculus. When you are bad at mathematics like me but accustomed to metamath it seems strange since it is absolutely impossible to make a proof in metamath without knowing a large number of tautologies.
But the reasons of that seems clear : propositional and predicate calculus are hardly used by `working' mathemathicians. And I think that we can say exactly the same for lambda calculus: mathematicians don't care about lambda calculus exactly like they don't care about predicate calculus. The logic chapter of Bourbaki's treatise for example is clear about what a mathematician thinks about logic (either standard or lambda calculus) and what they think about this is simple: who cares ?
By the way, once I tried to implement lambda calculus into metamath. It is perfectly possible. But people who thinks that standard logic in metamath is very low-level will suffer.
– frl 18-Jan-2006
My point above about lambda or things like it is that Lisp is based on lambda calculus in a fairly obvious way, and is also entirely easy to learn, understand, and use. So, hcode will be based on Lisp, and hence, fundamentally, on lambda calculus. --jcorneli
(Responding to frl) Yes, I believe the Metamath language should be able to implement lambda calculus if the axioms are set up for it, although I haven't done it myself. This would allow a direct emulation and translation of the low-level lambda calculus that happens internally in Isabelle. But even compared to that low level, the Metamath version would be very low level - one lambda-calculus "step" in Isabelle might involve a dozen Metamath steps to prove, say, a variable renaming operation by building up a wff with the various substitutions incorporated into its subwffs.
I have been trying to puzzle out what the poster meant by Metamath's "adhoc handling of bound variable scopes". Most likely he is referring to set.mm, which many people (including myself) often interchange with "Metamath". I think some people find its predicate calculus axioms somewhat odd, confusing, and seemingly arbitrary. I wouldn't argue the first two, :) but there is nothing arbitrary about the axioms, except the exact formalization I chose. (Like any logic, many equivalent formalizations are possible, and I am open to a more "intuitive" version.) I set out to find axioms that have exactly the strength needed to achieve the goal of "metalogical completeness" in a sense I defined, no more and no less, and these are what I ended up with. They provably achieve that goal, and most importantly are exactly logically equivalent to standard predicate calculus with equality.
Metalogical completeness lets set.mm naturally and directly work with wff metavariables, not just individual variables. Some proof languages can work only with individual variables and fixed predicate symbols, partly because that is a requirement of Robinson's resolution principle on which they are often based. For example, Otter can't work with ZF set theory because of ZF's wff metavariable. Since Isabelle can do ZF, it must have some method of working with metavariables. I don't know whether this ability is handled natively by its lambda calculus engine or whether it is something added on; perhaps an Isabelle expert can clarify. My feeling is that metavariables are a somewhat awkward add-on for some proof languages that make their verification/proving engines more complex, but experts in particular languages would have to clarify this.
It is possible that set.mm's metalogical completeness, i.e. the ability to work with metavariables natively, may be part of the answer to WhyAreMetamathProofsSoShort. The ability to prove general schemes may offset to a certain extent the very low-level nature of the proofs. One could set up a logic.mm module that would mimic the textbook schemes of predicate calculus, with recursively defined attributes of "free for" and "not free in", but I think many proofs would be much longer.
I wonder if any other proof language has set.mm's metalogical power of expression. Other than Ghilbert and friends of course. :) It would be interesting to know if another language can prove or even express set.mm's axiom (schemes) as theorem schemes, in particular those where free and bound variables don't have to be distinct.
--norm 18-Jan-2005
Another way of treating metavariables in ZF could be an embedding into some theory with sets and classes, like NBG or MK. The underlying theory may remain hidden from the user, who thinks he's in living in ZF with schemes. But the program understands his ZF statements as NBG statements about sets; metavariables in schemes become class variables. So the user is happy because he sees ZF, and automated provers are happy because they see a first-order NBG theory. Lambda calculus would be also helpful to invoke schemes easily. I am currently considering all this as an option for ufomath, where I've found myself drowning due to the lack of schemes. --alih