Re: [isabelle] Transitioning between ZF and HOL

Title: RE: [isabelle] Transitioning between ZF and HOL


On Sat 4/22/2006 5:37 PM, Tjark Weber wrote:
| 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.

I have actually been working on this a while, and that didn't occur to me when
I started.  I am considering porting my work to be based on one of these while
deleting repetitive results.  But that is a decision that I am not going to make
right now.  At the moment I am more focused on the equivalence question, which
is below.

| > 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?

My goal is a mathematical paper-proof that shows that the ring theory in
Isabelle is equivalent to what has been developed in Abstract Algebra.  I should
probably mention that I am an undergraduate:  this is a project for my
bachelor's degree, and while I have learned much about rigorous Zermelo-Fraenkel
set theory and category theory, I am still not very confident.

The proof that I seek, upto my understanding of the discipline, is to declare
the category of rings based on ZF sets and the category of rings based on Isabelle
sets, and then to find a functor from one to the other which satisfies certain

Does this make my goal clearer?  I have seen some information about both HOLZF
and HOL-ST, but it is unclear whether they would serve my purpose.

Thanks for your thoughts,
Robert Lamar

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