*To*: unlisted-recipients:; (no To-header on input)*Subject*: Re: [isabelle] I can't understand types in set-membership expressions*From*: Michal Czardybon <mczard at poczta.onet.pl>*Date*: Sun, 14 Sep 2008 19:42:31 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <266897.69518.qm@web30808.mail.mud.yahoo.com>*References*: <266897.69518.qm@web30808.mail.mud.yahoo.com>*User-agent*: Thunderbird 2.0.0.16 (Windows/20080708)

Slawomir Kolodynski pisze:

I always wanted to learn mathematics in the way, that Iclearlyunderstand 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 inhttp://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

-- Michał Czardybon

**Follow-Ups**:**Re: [isabelle] I can't understand types in set-membership expressions***From:*Tjark Weber

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

**References**:**Re: [isabelle] I can't understand types in set-membership expressions***From:*Slawomir Kolodynski

- Previous by Date: Re: [isabelle] I can't understand types in set-membership expressions
- Next by Date: Re: [isabelle] relating 2 theories
- Previous by Thread: Re: [isabelle] I can't understand types in set-membership expressions
- Next by Thread: Re: [isabelle] I can't understand types in set-membership expressions
- Cl-isabelle-users September 2008 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list