Re: [isabelle] Transitioning between ZF and HOL


On Tuesday 25 April 2006 11:06, Robert Lamar wrote:
> I believe that the proper comparison depends on the implementation of rings
> in Isabelle/HOL.  In HOL/Algebra and [2], rings are defined in locales with
> records, so the underlying set of the ring is something of the type "'a
> set".  In HOL/Algebra/abstract, HOL/Ring_and_Field.thy, and in my
> implementation (a more recent paper may be seen at [3,section 2.7,2.8]),
> the ring is defined through an axiomatic class, so the underlying set is
> taken to specifically be "UNIV::'a set".  In the first case, the
> equivalence would be (ZF sets ~ typed sets), for the second, I think it
> would be necessary to prove (ZF sets ~ types).
> Does this seem to be a good aproach?

I think it is.  Both approaches are of course closely related.

> Are these "usual set-theoretic semantics" similar to what is found in the
> Gordon paper [4] you cited in a previous email?  If so, are there other
> descriptions you would recommend as well?  If not, could you direct me
> towards a sound description of these?

There is a brief description in [4], and a more complete one e.g. in
the referenced book by Gordon and Melham, "Introduction to HOL: A
Theorem-Proving Environment for Higher-Order Logic".  A similar
presentation can be found in "The HOL System Description", available at
There is also a formalization of the HOL semantics (in HOL however, rather
than in ZFC) by R. Arthan, available at [5].


[4] "Higher Order Logic, Set Theory or Both?",

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.