*To*: Michal Czardybon <mczard at poczta.onet.pl>*Subject*: Re: [isabelle] I can't understand types in set-membership expressions*From*: Tjark Weber <tjark.weber at gmx.de>*Date*: Mon, 15 Sep 2008 23:26:18 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <48CD4D07.3070407@poczta.onet.pl>*References*: <266897.69518.qm@web30808.mail.mud.yahoo.com> <48CD4D07.3070407@poczta.onet.pl>

Michal, On Sun, 2008-09-14 at 19:42 +0200, Michal Czardybon wrote: > 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? both Zermelo-Fraenkel set theory (ZF) and higher-order logic (HOL) dispose of Russel's paradox (albeit in different ways: in ZF, "{x|x \notin x}" is not a set; in HOL, "x \in x" is not well-typed). This is not specific to their formalization in Isabelle. For a quick introduction, see, e.g., the Wikipedia entries on Russell's paradox, ZF set theory, and type theory. Best, Tjark

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

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

- Previous by Date: Re: [isabelle] relating 2 theories
- 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