Ghilbert/Metamath proof repository ideas
Marnix Klooster
Last year I did a write-up of Ghilbert/Metamath-related ideas at a
website of mine:
* http://designthis.wikispaces.com/Formal+math+repository+specification
* http://designthis.wikispaces.com/TAMO
* http://designthis.wikispaces.com/TAMO+Specification
Not maintained at the moment, not actively developed, but perhaps
interesting for some of you. :-)
Groetjes,
<><
Marnix
Raph Levien
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
> 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
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
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.
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
--
Subscription settings: http://groups.google.com/group/ghilbert/subscribe?hl=en
Raph Levien
<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?
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.
Raph
