Re: [isabelle] Transitioning between ZF and HOL



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





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