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 , 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  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 , 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 .
 "Higher Order Logic, Set Theory or Both?", http://www.cl.cam.ac.uk/~mjcg/papers/holst/
This archive was generated by a fusion of
Pipermail (Mailman edition) and