Re: [isabelle] Lattices with explicit carrier set vs. lattices with implicit carrier set



So it is a "challange". My question is whether having such a theory
makes it easy to tailor Isabelle to do such lifting between the two
kinds of theory development? How much programming work would this be
to have a usable framework?

- Gergely

2009/10/28 Lawrence Paulson <lp15 at cam.ac.uk>:
> Yes, this would be an excellent research project for somebody who is
> familiar with a variety of type theories and also has an intuitive
> understanding of set theory. But finding such a person is probably more
> difficult than finding somebody who is conversant in both Latin and Klingon.
> Larry
>
> On 27 Oct 2009, at 20:32, Jeremy Avigad wrote:
>
>> Tobias Nipkow, Brian Huffman, Amine Chaieb, and I once discussed ways that
>> one could embed Isabelle's type theory in a larger set-theoretic framework,
>> e.g. adding a type of sets and axioms that guarantee that "small" types
>> correspond to sets. If done right, that could yield a consistent system
>> (e.g. having the same logical strength as set theory) where one could go
>> back and forth between typed and set-theoretic versions of theorems, and so,
>> indirectly, from axiomatic-type class versions to set-based locale versions.
>> I still think that's an idea worth exploring, if anyone is willing and able.





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