Caghni update

12 views

Skip to first unread message

Adam Bliss

unread,

Dec 15, 2013, 5:19:06 AM12/15/13

to ghil...@googlegroups.com

On Nov 1, 2013 4:07 PM, "Adam Bliss" <abl...@gmail.com> wrote:
> My hope is to eventually have a script that can parse set.mm into theorem-objects, and parse ProofWiki and our own peano_thms.gh as well. All propositional-logic theorems will collide, even if the names are different. The peano theorems will be able to be automatically kind-bound to metamath's cardinals, since the theorems proved in metamath about cardinals will collide with the peano axioms required by our proofs. This will make practical a "global theorem search engine" which can search many different corpuses and convert between them. It will also be able to spit out verifiable Ghilbert versions of all objects; however the names will be opaque and one will need a kind of naming-layer (something like a stylesheet -- each camp can choose its own) in order to read the proofs.
>
> So far I've gotten just far enough to give this harebrained scheme a name: "caghni" for "Content-Addressable GHilbert Namespace and Index". I'll be trying to develop it at http://github.com/abliss/caghni if my motivation stays high enough.

I've been hacking slowly on caghni and I'm prepared to call this scheme slightly more than harebrained. Not quite foxbrained yet, but perhaps horsebrained.

The code is far from pretty, but it can now do one little trick that I haven't seen elsewhere. In the caghni repo I have four ghilbert interfaces: prop_min.ghi, prop_mer.ghi, prop_nic.ghi, and prop_luk.ghi, representing four different axiomatic bases for propositional calculus (one in -/\ and three in -> plus -.). After sucking in all the theorems in prop.gh (plus a few slight variations in nic.gh), the tool can then dynamically regurgitate a minimal .gh file which imports any one of the interfaces and exports any one of the others.

Soon, it should also be able to mix and match theorems from peano/ and from general/, but this is not yet implemented. Also, comments and whitespace do not yet survive the process.

Comments welcome. I have described the schema in the Readme.md on github, and I'd be keen to hear whether it actually works for anyone else but me.