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

[Joe Leslie-Hurd]

Hi Mario,

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

That's a nice write-up of your work. I particularly enjoyed your
discussion comparing the different forms of the Axiom of Choice in HOL
and ZFC:

"HOL is based on a version of the Axiom of Choice that is stronger
than the usual one in ZFC. Instead of asserting that for any set there
exists a choice function on that set, it asserts that a specific
function is a choice function on the universe. If the HOL universe
were a proper class, this would be problematic, but luckily it can be
entirely contained within Vω2, which is a set in ZFC, and thus the ZFC
axiom of choice gives us a single choice function on all of Vω2."

It's nice to know that HOL is "small" enough to fit cleanly into ZFC
in that way.

> 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?

How to divide your theories is mainly a question of taste. I recommend
aiming to base your theories on top of the standard theory library:

http://opentheory.gilith.com/?pkg=base

which contains many basic definitions, plus whatever other theories on
the public OpenTheory repo

http://opentheory.gilith.com/

that you find useful. Looking at the theories on the public repo may
also provide some good examples of how to export Metamath theories
into OpenTheory format.

> 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?

Your "large ind" proposal sounds similar to the "HOL + V" model in
Mike Gordon's classic paper on merging HOL and Set Theory:

https://www.cl.cam.ac.uk/~mjcg/papers/holst/index.html

Though it would be even better if Metamath theories could be converted
into "pure HOL".

Cheers,

Joe