*To*: "Robert Lamar" <rlamar at stetson.edu>*Subject*: Re: [isabelle] Transitioning between ZF and HOL*From*: Tjark Weber <tjark.weber at gmx.de>*Date*: Wed, 26 Apr 2006 18:28:01 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <16530916C2FEF64EBE4C333390E3BEFC04FB5E79@beta.ad.stetson.edu>*References*: <16530916C2FEF64EBE4C333390E3BEFC04FB5E79@beta.ad.stetson.edu>*User-agent*: KMail/1.8

Robert, 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 http://www.cs.uu.nl/docs/vakken/pv/resources/kananaskis-2-description.pdf. There is also a formalization of the HOL semantics (in HOL however, rather than in ZFC) by R. Arthan, available at [5]. Best, Tjark [2] http://afp.sourceforge.net/entries/Group-Ring-Module.shtml [3] http://www.stetson.edu/~rlamar/rings.pdf [4] "Higher Order Logic, Set Theory or Both?", http://www.cl.cam.ac.uk/~mjcg/papers/holst/ [5] http://www.lemma-one.com/ProofPower/specs/spc002.pdf

**Follow-Ups**:**Re: [isabelle] Transitioning between ZF and HOL***From:*Michael Norrish

**References**:**Re: [isabelle] Transitioning between ZF and HOL***From:*Robert Lamar

- Previous by Date: [isabelle] CFP: Workshop on Verified Software: Theories, Tools, and Experiments (VSTTE 2006)
- Next by Date: Re: [isabelle] Transitioning between ZF and HOL
- Previous by Thread: Re: [isabelle] Transitioning between ZF and HOL
- Next by Thread: Re: [isabelle] Transitioning between ZF and HOL
- Cl-isabelle-users April 2006 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list