HomePage RecentChanges

Ghilbert

ghilbertlogo

Ghilbert is an extension of metamath designed for collaborative theorem-proving on the Internet. It tries to preserve the simplicity, beauty, and power of the original, but fix several shortcomings. Over and above metamath, Ghilbert has:

There are a number of minor fixups and changes as well, such as getting rid of the "extended frame", reducing the number of "mandatory hypotheses" that are necessary in proofs (and thus taking away much of the need to store proofs in an ASCII compressed format).

One important part of the greater Ghilbert project is Ghilbert Pax, a web of axiomatizations designed to help make proofs easily portable from one system to another.

I strongly believe that Ghilbert is a good formal basis for a large Web-based repository of mathematical proofs. I would be happy to cooperate with The Hyperreal Dictionary of Mathematics project if they choose Ghilbert for this role, perhaps adopting it instead of hcode, or perhaps developing hcode as a competing project to Ghilbert level 1 (as mentioned in Ghilbert syntax plans), but with a seamless bridge to Ghilbert level 0 so that it can interoperate with the Ghilbert world. That said, there are some philosophical differences between my vision of Ghilbert and that of the HDM. In particular, Ghilbert is not AI-complete.

I'm currently in the process of putting together a real release. For a darcs repository of the development, as well as a snapshot and other related files, see the Ghilbert home page.

--raph

Tasks

Ghilbert is still in pre-release form. Here are some of the tasks that remain:

Specification

Ghilbert really needs a clear, up-to-date spec. The "design document" on ghilbert.org, in particular, doesn't reflect the more recent thinking on definitions. The Ghilbert specification is currently being updated collaboratively here on AsteroidMeta.

Verifier

The current verifier prototype, written in Python, is fairly complete (especially now that it includes verification of exports to interfaces from proof files). It is, however, lacking polish in a number of other areas, including error checking and reporting.

By my count, there are now no less than five independent implementations of metamath verifiers, and it would be very heartening to see something similar for Ghilbert. There are a number of good reasons to write a Ghilbert verifier, so I commend it to people wanting to get involved (of course, having a real spec would help.

Repository and website

The idea is for ghilbert.org to be a central website and repository of proofs, with an easy interface for both browsing the existing database and uploading new proofs to it. I need to figure out what software is best for hosting the site, or whether it's best to roll my own.

Connections to other systems

One of the central goals of Ghilbert is to make it feasible to translate proofs from other systems into Ghilbert, and also to import Ghilbert proofs into other systems.

Of these connections, I think HOL has the most immediate potential. The hol.ghi interface is written especially to support proofs translated from HOL.

In the other direction, a prototype bridge to import Ghilbert proofs into HOL is now posted on the Ghilbert website. Currently, it is capable of importing the entire propositional calculus theory, but needs more work to handle bound variables and definitions.

This section is still very sketchy. If there's any interest in taking up one or more of the tasks, put feedback here and I'll try to fill it in.

GUI Application

There is now an interactive Ghilbert application for creating proofs. It's still in early form, but usable enough to create proofs such as cnsscnp.

Discussions

AsteroidMeta has become a cozy home for discussions of Ghilbert, metamath, and related proof topics. By all means, feel free to ask questions here, and I'll do my best to answer. This is a Wiki, after all!

Here are some of the other wiki pages that may be of interest:

Still active?

Hi, is this the correct place to start a new thread?

Is the GHilbert project still active? There haven't been many changes to this page lately, and http://www.ghilbert.org is down.--GrafZahl

Questions and (maybe) answers

{ A few questions/failures in understanding the obvious:

1. The export/import features are declarative? But what is the mechanism for creating the export files? Does that happen via a utility – every time a utility is run (and how are things kept in sync if so).

I do have a utility for converting thm's to stmt's (it's very simple, basically just removing the proof and names of the hypotheses), but a lot of the time I create the .ghi file more manually. In fact, I often write the stmt in the .ghi file first, then try to write the proof.
Keep in mind that not all thm's should be exported as stmt's. The lemmata and so on never go past the .gh file. It's kind of like declaring a function in C static and not putting its prototype into the .h file :)

2. Utilization of namespaces, and syntax of the param/import statements are unclear to me.

Yes, this is probably one of the biggest areas that needs improvement in the spec. It is a fairly complex and subtle area, and took me months to puzzle out.

3. I am increasingly dissatisfied with the Metamath style treatment of (grammatical) type conversions. And yet sub-classing is common in programming languages, not to mention the new Bourbaki language. Should something like the set/class relationship be treated as a definition or theorem, and removed from the sphere of "syntax" per se – meaning that an explicit conversion should be required, either by the user or a a built-in coercion "theorem"?

Ghilbert doesn't do any automatic conversions between "kinds". Rather, in my translation of set.mm, I have an explicit (cv x) term. In my axiomatization of HOL, the corresponding term to convert a "var" to a "val" kind is (var x T), where T is a type.
The distinction between "set" and "class" in set.mm has a lot more to do with the fact that the former is a bindable variable, and less to do with the fact that the latter may not necessarily be a member of V. If you had one kind for both, how would you prevent constructions like E. 3 pi = 3 ?
It's not obvious how the type/kind distinction should go in other axiomatic frameworks. For a long time, in my axiomatization of Z2, I had separate kinds for nats and sets of nats (actually a total of four, because variables and values for both). Right now, I have one kind for both, and always state the type explicitly in quantifiers. I'm not sure which is better, frankly.
Another area in which I can imagine using the kind mechanism more fully is to implement the restrictions on formulae in the various subsets of second order arithmetic in Simpson's book. I haven't created files for any of that yet, though.

4. Will the user be able to apply the notation of his/her choice to the gh/ghi modules? So Norm could use set.mm's notation and another person could use, say, Polish notation?

There are definitely going to be translations between different syntax notations. The details are not entirely clear to me yet. The idea of .ghi files with really simple s-exp notation is important, because that's much easier for tools to deal with than requiring powerful parsing.
So how do we deal with both? The simplest way is just to have tools for translating in both directions (this already exists to a significant degree with Metamath). A fancier way is to do the translations "on the fly," for example in the UI of an interactive app.

4.B I suggest separating notation specifications from the other files, perhaps with a ".ghn" file providing notation.

5. Are Bourbaki and Ghilbert going to be unified conceptually? (I would like to view Bourbaki and Ghilbert as format and interface specifications rather than looking at, say, Bourbaki as a Lisp program…but they are already very closely related…)

I think your question gets to the heart of the reason why these are two different projects. Ghilbert is intended to be a simple, self-contained spec. Bourbaki, because it allows programming, includes by reference all of Common Lisp, which is pretty heavyweight. Thus, it's quite infeasible (though possible in principle; Turing completeness and all) to embed a Bourbaki verifier (and thus importer) into, say, HOL.
Do proofs need a programming language? That's a difficult question. The biggest issue is proof size - you certainly wouldn't want to do heavy arithmetic directly in Ghilbert (or Metamath). But, on the other hand, the entire set.mm is a testament to the fact that you don't need programming features to do a good job over a wide range of real mathematics.
My favorite approach for getting some of the best of both worlds is to use a "proof compiler" to go from higher levels (with programming) to lower (without). The result is basically a proof in "machine code". The big advantage is that you can verify this compiled proof using only very simple tools. Also, as long as the technical details are worked out, you should be able to mix and match proofs translated from several different source languages, and have everything verify in a clean, formal sense.
A quick way to get there would be for Bourbaki to output a "trace" of its proof as a Ghilbert .gh file. At heart, this should be pretty easy, but the devil is always in the details. I haven't studied how Bourbaki deals with definitions, in particular.

5.B I was, of course, disappointed with incorporation of Lisp by reference ("lisp-form") in the specification. I see how it might be useful though. Still, one not take advantage of this "feature", and that wasn't exactly what I was thinking about. One thing Bourbaki provides is the ability to specify a "bound" variable. It does that in addition to distinct variable specifications. Bourbaki also glumps the hierarchy of namespaces into "contexts", with a "root-context". I'm not clear on how all of this works in practice. And perhaps Ghilbert doesn't need to have the free/bound concept.

a comment about the Bourbaki context system
comment from raph: I haven't dug deeply into Bourbaki yet, but I'm going to take a wild guess that the concept of "bound variables" exists primarily to make definitions work; a dummy appearing in a definition is safe (and can be alpha-converted without loss of meaning) if it is bound, but potentially dangerous otherwise. In Ghilbert, I've carefully worked out rules entirely in terms of distinct variables, so that (unless I've made a mistake), definitions not using bound variables, or using a hybrid of bound and free variables as in the definition of substitution, are also safe. I do plan to study Bourbaki's approach to definitions in more detail, but in the meantime if somebody has more to say about which approach is better, I'd love to hear it. --raph

} --ocat p.s. I look forward to one day working on Ghilbert related topics. At this moment I really want to develop a proof assistant GUI, and am working hard to learn Python and Tkinter. Anyone wants to send me an IQ upgrade, post a note…I don't like thrashing any more than the next person, though I suspect that discomfort and suffering are prerequisites for (my) education :)

Not to throw cold water, but a GUI app is a pretty ambitious goal. The kind of tool I have in mind for Ghilbert even more so, because I want it to do real 2D math typesetting, which is of course an ambitious goal even without making it do formal proofs. I'm taking it in stages - certainly I want to get a batch parser working before even attempting to do it interactively. The important thing is to enjoy each step along the way, without getting too caught up in the final results.
Of course, all contributions to the Ghilbert universe are greatly appreciated, and, who knows, you might come up with a usable tool before I do - my perfectionism and the fact that I have a life guarantee that my tool won't be ready any time soon.

{If I cannot create a proof assistant GUI for Metamath then I'm going to have to hang up my keyboard :) I feel that it is essential to have a GUI for working with this stuff. Not necessarily for "experts", but for the novices who cannot bear the Mt. Everest learning curve. People today expect a GUI interface. They don't want to read-read-read and then do, they want to do-do-do and then reboot and try again. A lot of the learning process in logic is, like math, linguistic. That means transference of knowledge to the frontal lobes and wiring it in. (Notice how Norm's set.mm propositional logic theorems are basically just about moving symbols into different patterns – a sub-verbal activity.) Wiring in the skills requires lots of practice, and doing that in batch mode is ugly. Pencil and paper work too, of course…}--ocat

You might be interested in my description of Ghilbert's Core Proof Language. --marnix 15 June 2006

Possible design changes

I'm considering a few small changes to the design. This is a good place to leave feedback. Note: as of the latest development version (2005-11-21), both of these proposals are implemented. However, the dv conditions in the database mostly have not yet been trimmed.

RPN vs terms in proofs

Currently, terms occurring in proofs are in RPN format. So, to prove (→ (\/ ph ps) (\/ ph ps)), you'd write:

  ph ps \/ id

A consequence is that terms and theorems share a namespace. This causes a few collisions when the set.mm database is translated to Ghilbert, including 1o, 2o, and exp. To fix this, and possibly to improve readability, I'm considering changing it to writing the terms inline:

  (\/ ph ps) id

Variables and theorems would still share namespace, but that seems like a minor issue, especially as there are no such collisions in set.mm.

RPN is fine, and Lisp syntax is fine. But they sort of go in opposite directions, don't they? It seems like it would be confusing. You could, instead, format the whole proof in Lisp syntax:

  (id (\/ ph ps))

I like how applying a theorem here looks exactly like applying a procedure in a Scheme program. I can't tell if this solves your namespace problem or not, though. --jorend

…Surely if you ask Norm really nicely he'll rename the exp theorem and the handful of others that cause problems. No? --jorend 11 Oct 2006

On June 24, 2006, the Metamath spec was officially changed to prohibit label and math symbol namespace collisions, and set.mm was changed to conform to the new spec. E.g. the 'exp' theorem was renamed to 'ex'. So any Ghilbert translation since then shouldn't have this problem. --norm 12 Oct 2006

Presumably it is easy enough to create a new namespace for theorems? At least in lisp… --jcorneli


I have made the change to s-expressions rather than RPN for terms in proofs, and am very happy with the decision. Ironically, that means that Metamath and Ghilbert have now completely switched places with respect to the question of whether a term and theorem sharing the same name is allowed. I personally would have no problem with the requirement being removed from the Metamath spec, but this might be problematic for other Metamath implementation work.

Switching to s-expressions for the proofs, as jorend proposes, would reintroduce the namespace separation problem, because currently a proof step which is an atom is known to be either a variable, hypothesis, or stmt name, and all other steps are known to be terms. If a proof becomes a tree represented in s-expression form, rather than a sequence of proof steps, then this distinction is no longer available.

I have a few other stylistic reasons for preferring the sequence approach. First, it is more flexible for representing incomplete or broken proofs (important in interactive settings). Second, there is less work in rearranging proofs, as simple cut-and-paste of lines usually suffices, with no additional fixup of parentheses.

And third, I like not having to explicitly show deep nesting with calculational proofs involving long chains of equality, biconditionals, and indentations. I've chosen a preferred indentation policy based on this principle as well: the indentation level is equal to the stack depth after the last step on the line.

   proof that A = B
     proof that B = C
   eqtr
     proof that C = D
   eqtr
     proof that D = E
   eqtr

To me, this style of proof of A = E captures at least some of the flavor of Dijkstra and Scholten's calculational proofs. You can see some examples amongst the new proofs in hol-zfc.gh, such as df-$\/-half and df-$\/.

raph 17 Oct 2006

Distinct variable conditions on dummies

Right now, Ghilbert enforces the same distinct variable conditions as Metamath (where they are written as $d statements). I'm considering requiring only dv constraints on variables listed in the hypotheses and result; dummies that occur only inside the proof would automatically be considered distinct.

marnix has implemented this more liberal policy in Hmm, and suggests that I do the same in Ghilbert.

?