<div dir="ltr"><div class="gmail_extra"><div class="gmail_quote">On Thu, Jan 8, 2015 at 2:55 AM, Roger Bishop Jones <span dir="ltr"><<a href="mailto:rbj@rbjones.com" target="_blank">rbj@rbjones.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
  

    
  
  <div text="#000000" bgcolor="#FFFFFF">
    HOL has the same consistency strength as Maclane Set theory,<br>
    which is strictly weaker than Zermelo set theory.<br>
    Therefore an embedding of Zemelo into HOL will not be possible<br>
    without axiomatic extension of HOL, for which a strengthening<br>
    of the axiom of infinity would suffice.<br></div></blockquote><div><br></div><div>Somewhat related work on specifying Zermelo set theory in HOL (and using this to prove HOL's consistency in HOL, under the above-mentioned assumption) can be found at <a href="https://cakeml.org/jarhol.pdf">https://cakeml.org/jarhol.pdf</a> (under review).<br></div></div></div></div>