Re: [isabelle] Transitioning between ZF and HOL



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

Tjark,

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
requirements.

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.