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


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.


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