<p>Hi Mario,</p>
<p>I do not know the Z fragment, but the main issues in ZFC vs HOL seem to be: (1) the HOL type discipline prevents you to mix sets of different types, and (2) the HOL axioms are too weak to allow transfinite constructions.</p>
<p>Off the top of my head, I am aware of the following:</p>
<p>- the HOLZF work in Isabelle by Obua, just axiomatizing ZF(C?) as a type (practically adding an inaccessible cardinal axiom instead of just omega)</p>
<p>- a bridge between Isabelle/ZF and Isabelle/Hol by Krauss (I do not know the details)</p>
<p>- Kuncar's MS work on importing the Mizar soft typing mechanisms into HOL (Light), again embedding the whole ZFC there as a separate type</p>
<p>- Mike Gordon's older paper discussing various options how to link ZF and HOL</p>
<p>Josef<br>
</p>
<div class="gmail_quote">On Jan 8, 2015 1:32 AM, "Mario Carneiro" <<a href="mailto:di.gama@gmail.com">di.gama@gmail.com</a>> wrote:<br type="attribution"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div><div>Hello all,<br><br></div>I'm trying to locate any research done on what kinds of subsystems of ZFC can be embedded into higher order logic. My initial approach on the subject leads me to believe that HOL can embed any proof in Z, using the following method:<br><br>HOL contains types of cardinality om (omega), ~P om, ~P ~P om, etc for any 
finite number of ~P's (the powerset operation). 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>Does anyone know of any papers or work done in the direction of embedding fragments of ZFC in HOL like this?<br><br></div>Mario Carneiro<br></div>
<br>_______________________________________________<br>
FOM mailing list<br>
<a href="mailto:FOM@cs.nyu.edu">FOM@cs.nyu.edu</a><br>
<a href="http://www.cs.nyu.edu/mailman/listinfo/fom" target="_blank">http://www.cs.nyu.edu/mailman/listinfo/fom</a><br>
<br></blockquote></div>