Re: [isabelle] I can't understand types in set-membership expressions
> You suggest me reading about Isabelle/ZF rather that /HOL,
> but if so,
> then why HOL is the main system in Isabelle.
Isabelle is mostly used for tasks related to software verification, not formalized mathematics. HOL is much better for that.
A more interesting question is why people choose to do formalized mathematics in Isabelle/HOL rather than Isabelle/ZF. For that I don't have a good answer.
> there a problem with
> ZF that it doesn't solve the Russel's Paradox?
Certainly not, see http://en.wikipedia.org/wiki/Zermelo_Fraenkel_set_theory .
This archive was generated by a fusion of
Pipermail (Mailman edition) and