<div dir="ltr"><br><div class="gmail_extra"><br><div class="gmail_quote">On Mon, Jan 5, 2015 at 6:10 PM, Joe Leslie-Hurd <span dir="ltr"><<a href="mailto:joe@gilith.com" target="_blank">joe@gilith.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Your "large ind" proposal sounds similar to the "HOL + V" model in<br>
Mike Gordon's classic paper on merging HOL and Set Theory:<br>
<br>
<a href="https://www.cl.cam.ac.uk/~mjcg/papers/holst/index.html" target="_blank">https://www.cl.cam.ac.uk/~mjcg/papers/holst/index.html</a><br>
<br>
Though it would be even better if Metamath theories could be converted<br>
into "pure HOL".<br></blockquote><div><br></div><div>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:<br><br></div><div>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.<br><br>Do you know of any papers or work done in the direction of embedding fragments of ZFC in HOL like this?<br><br>Mario<br><br></div></div></div></div>