Re: [isabelle] Transitioning between ZF and HOL

My paper below includes an (implicit) recipe for interpreting set theory in a model of type theory.

Michael P. Fourman. Sheaf models for set theory. Journal of Pure and Applied Alegebra, 19:91-101, 1980.
  AUTHOR = {Michael P. Fourman},
  TITLE = {Sheaf Models for Set Theory},
  PAGES = {91-101},
  JOURNAL = {Journal of Pure and Applied Alegebra},
  VOLUME = {19},
  YEAR = {1980}

On 24 Apr 2006, at 14:30, Tjark Weber wrote:


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.