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


> 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

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

And if you really want "every tiny bit", check out the Metamath project at 

Library of Formalized Mathematics for Isabelle/Isar (ZF Logic)


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