Re: [isabelle] Transitioning between ZF and HOL
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
> 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and