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

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.

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.