Re: [isabelle] Transitioning between ZF and HOL


On Sunday 23 April 2006 06:35, Robert Lamar wrote:
> | 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.
> [...]
> 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.

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.



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