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



Slawomir Kolodynski pisze:
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).

You suggest me reading about Isabelle/ZF rather that /HOL, but if so, then why HOL is the main system in Isabelle. Isn't there a problem with ZF that it doesn't solve the Russel's Paradox? I know I can probably learn about it from the documentation your are suggesting, but I just want to find out quickly what would be the best starting point for me.


And if you really want "every tiny bit", check out the Metamath project at http://us.metamath.org/mpegif/mmset.html
"every tiny bit" is a bit exaggeration. What I really wanted to say was that creating or following mathematical proofs many times I had a feeling that I am not really sure if some step of a proof was correct. As a programmer I strongly feel that it would be much better if proofs were written similarily like computer programs - i.e. in accordance to mechanically strict rules. Having such a system I would be able to develop mathematical theories and I would be sure that I make no mistakes.

--
Michał Czardybon






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