[opentheory-users] Embedding Z (or other ZFC fragments) in HOL

[Roger Jones]

On 8 Jan 2015 06:17, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk> wrote:
>
> 
>
> 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 https://cakeml.org/jarhol.pdf (under review).

That is the paper I had intended to mention in my second post.  My apologies for incorrectly attributing it to Rob Arthan rather than to the team of which you and he were members.

Roger Jones