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
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 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and