Re: [isabelle] Transitioning between ZF and HOL

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


On Mon 4/24/2006 9:30 AM, Tjark Weber wrote:
| > 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.

That comes close the the tack that I was thinking of taking.  My thought was originally to look at the category of HOL sets (objects of type "'a set"), although it may not be the best tactic.  The idea would be to prove that those were equivalent by finding the appropriate functor F, then show that the ring axioms had the same consequences when passing from one space to the other under F. 

I believe that the proper comparison depends on the implementation of rings in Isabelle/HOL.  In HOL/Algebra and [2], rings are defined in locales with records, so the underlying set of the ring is something of the type "'a set".  In HOL/Algebra/abstract, HOL/Ring_and_Field.thy, and in my implementation (a more recent paper may be seen at [3,section 2.7,2.8]), the ring is defined through an axiomatic class, so the underlying set is taken to specifically be "UNIV::'a set".  In the first case, the equivalence would be (ZF sets ~ typed sets), for the second, I think it would be necessary to prove (ZF sets ~ types).

Does this seem to be a good aproach?

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

Are these "usual set-theoretic semantics" similar to what is found in the Gordon paper [4] you cited in a previous email?  If so, are there other descriptions you would recommend as well?  If not, could you direct me towards a sound description of these?


[4] "Higher Order Logic, Set Theory or Both?",

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