<div dir="ltr"><div><div><div>Thank you to everyone who has provided such great references; this is exactly what I was looking for.<br><br></div>I think I can see why my proposed translation would fail, since there is a possibility that unbounded quantifiers in the separation scheme, which would be translated to bounded quantifiers over a "large enough" set, could still detect that they are bounded. To take a simple example, the proposition ( om e. x /\ A. x E. y rank(y) > rank(x) ) would be true in the intended model V_2om of HOL but false in any type (assuming that types are mapped to elements of V_2om), no matter how large.<br><br></div>The claim that Z (just so we're on the same page, Z means Zermelo set theory here) proves Con(HOL) leads me to consider the reverse embedding, however, by roughly the same method. Define the types 2 = bool and om = ind as 0-large, and define an n-large set inductively as sets of the form A, A^B for any n-1-large sets A, B. This is definable in Z, and the set of all n-large sets for fixed n provably exists in Z. Then any given proof in HOL will use only n-large sets up to some fixed n, and all these can be proven to exist. Furthermore, this approach allows one to map HOL + global choice (which is the way AC is usually formulated in HOL) to ZC, because if you assume that f is a choice function on all n-large sets for some n large enough for all the types in the proof, then f can play the role of the @ choice function, and at the end of the proof you can discharge the assumption by AC.<br><br></div>Mario<br></div><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Jan 7, 2015 at 5:07 PM, roux cody <span dir="ltr"><<a href="mailto:cody.roux@gmail.com" target="_blank">cody.roux@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div><div>Hi Mario,<br><br></div> You've probably found Forster's "Weak systems of Set Theory Related to HOL"<br><br><cite><a href="https://www.dpmms.cam.ac.uk/~tf/maltapaper.ps" target="_blank">https://www.dpmms.cam.ac.uk/~tf/maltapaper.ps</a></cite><br><br></div><div>Which clarifies things a bit: HOL is *exactly* as strong as "Mac Lane set theory", which is Zermelo set theory with only *bounded* comprehension (no quantifiers over all sets)<br>and so is quite weaker than Zermelo set theory <i>per se</i>.<br><br></div><div>A nice article by Alexandre Miquel describes a variant of HOL (which allows additional quantifications) that is *exactly* as powerful as Z: they are equiconsistent (in PA).<br><br></div><div>"lambda Z: Zermelo's Set Theory as a PTS with 4 Sorts"<br><br><a href="http://dl.acm.org/citation.cfm?id=2150524" target="_blank">http://dl.acm.org/citation.cfm?id=2150524</a><br><br></div><div>This rather nicely settles the question of finding a type theory as powerful as Z set theory. I think ZF is considerably more difficult, and as far as I know the question is still open.<br><br></div><div>Best,<br><br></div><div>Cody<br></div><div><br></div><div><cite></cite><cite></cite></div></div><div class="gmail_extra"><br><div class="gmail_quote"><div><div class="h5">On Tue, Jan 6, 2015 at 4:48 AM, Mario Carneiro <span dir="ltr"><<a href="mailto:di.gama@gmail.com" target="_blank">di.gama@gmail.com</a>></span> wrote:<br></div></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div class="h5"><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?<span><font color="#888888"><br><br></font></span></div><span><font color="#888888">Mario Carneiro<br></font></span></div>
<br></div></div><span class="">_______________________________________________<br>
FOM mailing list<br>
<a href="mailto:FOM@cs.nyu.edu" target="_blank">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></span></blockquote></div><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><br></div>