2 Sep 2002 raph   » (Master)


jeremyw is correct, of course. Simply saying "permission to quote is granted" or something similar is almost as concise, and far clearer to most people.


The second big problem with Metamath is the fact that it nails down specific constructions. It's important to note, however, that this is a characteristic of the set.mm database, not the Metamath framework itself.

The solution to this problem, I think, is to use "theory interpretation." Instead of saying, for example, "0 is the empty set, and x + 1 is x U {x}", you say, "for all sets N and functions +, -, *, /, whatever satisfying the usual axioms for arithmetic." Then, if you ever need to show the existence of such a thing, for example to use arithmetic as a temporary while proving something else, you can use the standard construction, or any construction for that matter.

The question is how much more awkward this will make proofs. Metamath's choice of a definite construction is good for overall simplicity. I guess there's really only one way to find out.

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!