Re: [isabelle] Transitioning between ZF and HOL



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





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