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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and