Last year I did a write-up of Ghilbert/Metamath-related ideas at a
website of mine:
Not maintained at the moment, not actively developed, but perhaps
interesting for some of you. :-)
These design decisions are tough to make, and aren't fully independent
of each other. For example, in isolation I think distinct variables
make just as much sense as bound ones (although not having to have
separate foo and foov theorem variants is nice). But in the context of
a definition mechanism, bound variables allow a _much_ simpler
treatment of def dummies.
Now that we have several variants, I'm looking forward to reconciling
them as much as possible, or at least writing translation scripts that
let people move smoothly between them.
Thanks again, Marnix.
> Awesome, thanks for those links. Mind if I add them to the wiki?
You're welcome, feel free to use as you wish.
> These design decisions are tough to make, and aren't fully independent
> of each other. For example, in isolation I think distinct variables
> make just as much sense as bound ones (although not having to have
> separate foo and foov theorem variants is nice). But in the context of
> a definition mechanism, bound variables allow a _much_ simpler
> treatment of def dummies.
Yes, I agree about the dependency, and I'm meaning to read up on all
definition (I really prefer "abbreviation") mechanism ideas. Perhaps
I also wanted to touch on one of the other design decisions you
brought up in those pages: whether to have namespace prefixing or just
treat import as textual inclusion of the interface files. The main
motivation for the namespaces is to allow "adapters" that import one
axiomatization and export another. As a crisp example, see
http://levien.com/garden/ghilbert/peano/zfc-peano.gh , which is a
construction of Peano arithmetic in ZFC set theor (as axiomatized by a
translation of Metamath's set.mm). The definition of Peano's = is
slightly different from the original in set theory. What's done in
zfc-peano.gh is creating all the terms and theorems in the Peano space
with a "$" prefix, and exporting the peano interface with "$" as a
Similarly, if you look at http://levien.com/garden/ghilbert/hol/
you'll see a fairly complete construction of the axioms of HOL based
on ZFC set theory. That includes both the construction of new types
and iota (I was also going to work on a construction of epsilon based
on the axiom of choice, but ran out of steam around then). A complete
version would probably be publishable work. In that particular case, I
chose to name the HOL primitives $= and so on, but that would force
all users of the HOL axioms to use those names. It would almost
certainly be nicer to use the prefix as in the peano case.
Another use of the namespace prefixes would be in a Z2 world. In that
world, you can quantify over two types of variables: nats and sets of
nat. What would make tons of sense is to have _one_ interface
representing first-order propositional calculus, and import it twice
with two different prefixes. (In the typesetting and UI layer, all
this would be hidden, and you'd say \forall x and \forall s, which
would be converted into, say A. x and *A. s, respectively, based on
type sensitivity in the disambiguation rules).
So I'd be reluctant to give up that additional richness, especially
since a major goal of my work in Ghilbert is to bridge between various
axiomatizations. If you were going to do all your work in a single
axiomatization (as is pretty much the case in the Metamath world, with
set.mm, even though there are others), then you probably wouldn't need
it and the simplification would be worthwhile.