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

[Ramana Kumar]

On Thu, Jan 8, 2015 at 2:55 AM, Roger Bishop Jones <rbj at rbjones.com> wrote:

>  HOL has the same consistency strength as Maclane Set theory,
> which is strictly weaker than Zermelo set theory.
> Therefore an embedding of Zemelo into HOL will not be possible
> without axiomatic extension of HOL, for which a strengthening
> of the axiom of infinity would suffice.
>

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).
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20150108/2ceefc3b/attachment.html>