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

Mathematics is most easily formalised using types, with the exception of the sort of thing done in set theory: foundational definitions of functions, relations, ordinal and cardinal numbers, etc. Set theory is therefore rather like assembly language: it is perfect for low level developments but otherwise a poor choice if you want to get anything done.

On 15 Sep 2008, at 23:08, Slawomir Kolodynski wrote:

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.

Larry Paulson

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