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
Ghilbert is still in pre-release form. Here are some of the tasks that remain:
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.
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.
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.
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.
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.
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:
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
{ 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).
2. Utilization of namespaces, and syntax of the param/import statements are unclear to me.
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"?
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?
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…)
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.
} --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 :)
{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
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.
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
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
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.
—
?