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

[Mario Carneiro]

On Mon, Jan 5, 2015 at 6:10 PM, Joe Leslie-Hurd <joe at gilith.com> wrote:

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

Great, a paper like that is exactly what I was hoping for. Of course I
would like to map as much as possible of Metamath into pure HOL, and since
Metamath tracks axioms in a proof and theorems are generally proven in the
weakest possible subsystems, this may well be possible for those theorems
that are in fact embeddable in HOL. But what subsystem would that be? My
gut tells me that Z should fit in HOL, but it seems a bit tricky to do
properly. My thoughts:

HOL contains types of cardinality om, ~P om, ~P ~P om, etc for any finite
number of ~P's (that's the powerset operation, btw). Since any particular
proof in Z will use the theorems "om e. V" (omega exists) and "x e. V -> ~P
x e. V" (a powerset exists) finitely many times, you could define a
function on types (does such a thing exist?) saying that a type A is
"n-large" meaning there is an injection from ~P ~P ... ~P om to A (where
there are n ~P symbols), and then a proof in Z would get V mapped to an
arbitrary type A, and if there are n ~P's used in the proof you would
preface the entire proof with "A is n-large". When you are done and ready
to map the model back to the regular HOL notions, you replace A with
ind->bool->...->bool (n times), and then prove that this type is n-large to
discharge the extra assumption.

Do you know of any papers or work done in the direction of embedding
fragments of ZFC in HOL like this?

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