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.

> Isn't
> there a problem with 
> ZF that it doesn't solve the Russel's Paradox? 

Certainly not, see .


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