Email Gateway (Aug 17 2022 at 14:16): Email Gateway (Aug 17 2022 at 14:16):From: Robert Lamar <rlamar@stetson.edu>
I am attempting to develop ring theory in HOL, and at the same time prove that these rings are categorically equivalent to rings founded in Zermelo-Fraenkel set theory. It has been singularly difficult to find resources that describe the transition between ZF and the typed set theory that one finds in Isabelle, or a more general type theory. Is there anyone here who could point me to good references?
Thanks,
Robert Lamar
Email Gateway (Aug 17 2022 at 14:16):From: Tjark Weber <tjark.weber@gmx.de>
Robert,
On Saturday 22 April 2006 04:07, Robert Lamar wrote:
I am attempting to develop ring theory in HOL,
I would suggest to take one of the existing formalizations of ring theory that
can be found in HOL/Ring_and_Field.thy or in HOL/HOL-Algebra as a starting
point.
and at the same time prove that these rings are categorically equivalent to
rings founded in Zermelo-Fraenkel set theory.
Do you want to prove this on paper, or in Isabelle? In any case, what would
be your theory for this proof?
It has been singularly difficult to find resources that describe the
transition between ZF and the typed set theory that one finds in Isabelle,
or a more general type theory. Is there anyone here who could point me to
good references?
I'm not sure if this answers your question, but HOL can be given a
set-theoretic semantics (see e.g. Mike Gordon and Tom Melham (editors), An
Introduction to HOL, a Theorem Proving Environment for Higher Order Logic),
and while ZF set theory cannot be interpreted directly in HOL (as there is no
type of sets), such a type can be added to HOL as an axiomatic extension --
see http://www.cl.cam.ac.uk/~mjcg/papers/holst/ for some papers on this, and
http://www4.in.tum.de/~obua/partizan/ for a description of a recent
implementation in Isabelle.
Best,
Tjark
Email Gateway (Aug 17 2022 at 14:16):From: Robert Lamar <rlamar@stetson.edu>
Tjark,
Email Gateway (Aug 17 2022 at 14:16):From: Tjark Weber <tjark.weber@gmx.de>
Robert,
it may be conceptually simpler to look at (the categories of) arbitrary ZF
sets and HOL types first. Do you consider them to be "equivalent" in any
sense? Rings should then form a particular subcategory.
The embedding of type theory into ZF that you discuss in Section 3.6 of
your research proposal [1] is probably going to be the usual set-theoretic
semantics of HOL.
Best,
Tjark
[1] http://www.stetson.edu/artsci/mathcs/students/research/math/ms498/2005/lamar/proposal.pdf
Email Gateway (Aug 17 2022 at 14:43):From: Robert Lamar <rlamar@stetson.edu>
Tjark,
Email Gateway (Aug 17 2022 at 14:43):From: Tjark Weber <tjark.weber@gmx.de>
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
Email Gateway (Aug 17 2022 at 14:43):From: Michael Norrish <Michael.Norrish@nicta.com.au>
Tjark Weber writes:
Just a minor point: that HOL documentation is better taken from our
website
http://hol.sf.net
What is in our Description manual should indeed be just the same as
what is in the Gordon-Melham book.
Regards,
Michael.
Last updated: May 03 2024 at 08:18 UTC