# Ghilbert/Metamath proof repository ideas

61 views

### Marnix Klooster

Mar 5, 2010, 2:49:58 PM3/5/10
Hi all,

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. :-)

Groetjes,
<><
Marnix

### Raph Levien

Mar 5, 2010, 11:45:03 PM3/5/10
Awesome, thanks for those links. Mind if I add them to the wiki?

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.

Raph

### Marnix Klooster

Mar 6, 2010, 3:58:59 AM3/6/10
to Ghilbert
Hi Raph,

> 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
the recent
definition (I really prefer "abbreviation") mechanism ideas. Perhaps
even
today...

Groetjes,
<><
Marnix

### Raph Levien

Mar 27, 2010, 3:22:56 PM3/27/10

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
namespace prefix.

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.

Raph

### Marnix Klooster

Apr 23, 2010, 4:12:21 PM4/23/10
to Ghilbert
Hi Raph,

On 27 mrt, 21:22, you wrote:
> 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.

I don't think I wrote explicitly on this distinction at
http://designthis.wikispaces.com/TAMO+Specification. At least I did
not intend to. What wording led you to this conclusion?

That specification document currently only has the "metalogic" part
filled in, where I talk about the concepts, not about their embodiment
in text or files or S-expressions or anything.

Anyway, in a TAMO database, no statement would inherently have a name,
instead statements and (hierarchical) names would have a many-to-many
relationship. Also, a TAMO database is a basically a collection of
proofs, where each proof describes how to construct one statement from
zero or more others. So I'm not thinking of any grouping of theorems
in 'proof files'. The only grouping is a 'theory', which is just a
set of theorems (no names, no order).

Therefore TAMO has no notion of "textual inclusion" nor of "interface
files". At least that's my current thinking.

Separate from prefixing of statement names, still prefixing of
constants ('term's) could be useful. And in TAMO that's covered by
abbreviations: using abbreviations it is possible that a set of
statements with "\$"-prefixed constants, and a set without that prefix,
are "equivalent", in the sense that introducing abbreviations lets us
prove one from the other. So that is no theoretical need to have
prefixing here-- but practically this would be an operation that would
be done often, as it is in Ghilbert, as you described well in your
mail.

Indeed, I intend TAMO to be a database that can be directly filled
from Ghilbert files through a simple conversion, and vice versa.

Groetjes,
<><
Marnix

--

### Raph Levien

Apr 24, 2010, 6:18:35 PM4/24/10
On Fri, Apr 23, 2010 at 1:12 PM, Marnix Klooster
<marnix....@gmail.com> wrote:
> Hi Raph,
>
> On 27 mrt, 21:22, you wrote:
>> 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.
>
> I don't think I wrote explicitly on this distinction at
> http://designthis.wikispaces.com/TAMO+Specification.  At least I did
> not intend to.  What wording led you to this conclusion?

I think I didn't read it very carefully. It's probably mostly because
you said you're rejecting the "param" approach, and of course the
namespace prefix in "param" is the main way in Ghilbert to allow
import of multiple interfaces with possibly conflicting names. But it
seems like you have a different approach.

> That specification document currently only has the "metalogic" part
> filled in, where I talk about the concepts, not about their embodiment
> in text or files or S-expressions or anything.
>
> Anyway, in a TAMO database, no statement would inherently have a name,
> instead statements and (hierarchical) names would have a many-to-many
> relationship.  Also, a TAMO database is a basically a collection of
> proofs, where each proof describes how to construct one statement from
> zero or more others.  So I'm not thinking of any grouping of theorems
> in 'proof files'.  The only grouping is a 'theory', which is just a
> set of theorems (no names, no order).
>
> Therefore TAMO has no notion of "textual inclusion" nor of "interface
> files".  At least that's my current thinking.
>
> Separate from prefixing of statement names, still prefixing of
> constants ('term's) could be useful.  And in TAMO that's covered by
> abbreviations: using abbreviations it is possible that a set of
> statements with "\$"-prefixed constants, and a set without that prefix,
> are "equivalent", in the sense that introducing abbreviations lets us
> prove one from the other.  So that is no theoretical need to have
> prefixing here-- but practically this would be an operation that would
> be done often, as it is in Ghilbert, as you described well in your
> mail.
>
> Indeed, I intend TAMO to be a database that can be directly filled
> from Ghilbert files through a simple conversion, and vice versa.

That sounds great!

Raph