25 Aug 2002 raph   » (Master)


I've been chewing over Metamath in my head some more. It's very appealing in lots of ways, especially its simplicity, but a few things need to be done differently, I think, to make it work as a distributed, web-based proof repository.

The biggest problem is namespaces. On the web, everybody has to be able to define their own local namespace, while also being able to refer to other things in the world. Metamath, by contrast, uses short, cryptic, and impermanent names for its theorems. On that last point, set.mm includes this note: "While this file is complete and correct, it may undergo revisions from time to time (including theorem name changes, which means any new theorems you add may not always remain compatible)." That won't do.

Actually, I'm pretty convinced by now that the best name for a theorem is the theorem itself. If the size of the name is a concern, a hash can be substituted. However, an advantage of using the whole theorem is that, if a correct proof cannot be found on the web, someone can probably prove it by hand.

The namespace of newly defined keywords is also problematic. In fact, Metamath does not automatically check whether definitions are ambiguous. Having a definition collision could lead to contradiction, which would be bad. For definitions that simply expand as macros, I suppose you could use the expansion (or a hash thereof) as the permanent name. However, not all definitions in Metamath have this form.

The second big problem, as I've mentioned earlier, is whether to keep theorems abstract, or pin them down to a single model. Metamath does the latter, which helps keeps theorems simple, but it also makes them nonportable to other models. I think it's possible to do abstract theorems in Metamath (you quantify over all possible models that satisfy the axioms), but probably notationally very cumbersome. Even so, it's similar to the way a lot of mathematics is done: you see a lot of theorems over, say, fields, without them pinning down which field is meant.

I'm still not sure whether formulae should be represented as strings of symbols (subject to implicit parsing through wff rules), or as trees. My gut feeling is the latter, because it sidesteps the issue of whether the parsing grammar is ambiguous. The former is a slightly simpler representation, though, and also closer to human-readable mathematics.

There are a few stylistic choices which are unusual, but probably reasonable. For one, the only primitive inference rules are the Modus Ponens and generalization. Equality and substitution are handled through theorems just like everything else. For another, instead of classifying variables as "free" or "bound", Metamath just places distinctness constraints on variables. A lot of the primitive operations such as substitution are cleverly defined to place no more distinctness constraints than necessary.

By the way, does anyone have a formal spec for lambda? Here's what I have, but I don't know if it's right:

( lambda x A ) = { y | y = E. z <. z , [ x / z ] A >. }
y,z,A distinct

Latest blog entries     Older blog entries

New Advogato Features

New HTML Parser: The long-awaited libxml2 based HTML parser code is live. It needs further work but already handles most markup better than the original parser.

Keep up with the latest Advogato features by reading the Advogato status blog.

If you're a C programmer with some spare time, take a look at the mod_virgule project page and help us with one of the tasks on the ToDo list!