[opentheory-users] Preprint of OT->Metamath conversion paper, thoughts on MM->OT conversion

[Mario Carneiro]

Hello all,

Although the implementation is still in progress, I've completed a writeup
of the algorithm for converting OT article files into valid Metamath
proofs, to be published in the Journal of Formalized Reasoning. You can
find the preprint on arXiv, http://arxiv.org/abs/1412.8091 .

I've also been thinking about the reverse conversion process, but before I
get into the details I'd like to establish what are the usual conventions
are for producing good output, since so far I've only looked at the article
level and haven't even touched any theory files. In particular, how should
I structure the theory division process, and what OT base definitions
should I import?

For context, a Metamath file is a list of theorems, where each theorem has
a derivation that refers to textually previous theorems or axioms. The
entire metamath database is one (rather large) file, and there are section
headers, but they are just comments (although they are machine-readable for
presentation purposes). I expect that the different theorems correspond
well to "thm" exports, and perhaps the section headers correspond to theory
files (although there are quite a few, perhaps a few thousand section
headers). The sections come in three levels, from the 14 major "parts" to
the "chapters" and then "sections", each of which might have from 1 or 2 to
a couple hundred theorems each. (see:
http://us2.metamath.org:88/mpegif/mmtheorems.html)

Also, Metamath is built on ZFC foundations, although we also have the
Tarski-Grothendieck axiom defined. However, Metamath tracks axiom usage,
and there is a conscious effort to limit unnecessary axiom usage (most
other systems don't seem to do this, i.e. using the axiom of choice to
prove the law of excluded middle is rather overkill), so it is possible
that some of the weaker subsystems fit in vanilla HOL. However, it is
well-known that ZFC is stronger than HOL, and so the general approach I was
intending is to add some kind of universe axiom to say that "ind" is a
really big set, big enough for some construction of an epsilon-relation to
satisfy the axioms of ZFC. Does anyone know of research and/or existing
definitions along these lines?

Mario Carneiro
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20150102/d53dd561/attachment.html>