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

For Isabelle/ZF based formalizations farther away from the foundations you can look at . (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
"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.