Re: [isabelle] I can't understand types in set-membership expressions



Michal,

> I always wanted to learn mathematics in the way, that I
> clearly 
> understand every tiny bit. 

The set theory you might be familiar with is the Zermelo - Fraenkel set theory. This is different than the typed set theory implemented in Isabelle/HOL. 
A Tjark Weber mentions in a separate post, Isabelle implements the ZF set theory as well. For what you want to do I believe Isabelle's ZF logic is a better place to look at. There is some documentation on the logic in  

http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle/doc/logics-ZF.pdf

For Isabelle/ZF based formalizations farther away from the foundations you can look at http://formalmath.tiddlyspot.com/ . (dislaimer: I am the author of that site).

And if you really want "every tiny bit", check out the Metamath project at http://us.metamath.org/mpegif/mmset.html 

Slawomir

http://savannah.nongnu.org/projects/isarmathlib
Library of Formalized Mathematics for Isabelle/Isar (ZF Logic)




      





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