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

`I always wanted to learn mathematics in the way, that I clearly
``understand every tiny bit. I started learning Isabelle recently to find
``out how maths can be precisely formalized, not to work with it to do
``real theorem proving. I am aware of two main problems with
``formalization: (1) russel's paradox and (2) meaning of the function
``application to an argument outside of its domain. I am very interested
``with how Isabelle copes with these problems. Can anybody tell me or
``point the related sections of the documentation?
`
I have tried "Set, Functions and Relations", which states:
"Our sets are typed. In a given set, all elements
have the same type, say T, and the set itself has type T set."
but I can still see a problem with expressions like this:
a : { {a, b}, c }
As I understand the types are:
set-membership operator (:) is of type "[alpha, alpha set] => bool"
"a", "b", "c" are of type "alpha"
"{a, b}" is of type "alpha set"
What it the type of "{ {a, b}, c }"??
Isn't it a union of types "alpha set" and "alpha set set", which
seems like an incorrect typing?
Even if it were:
a : { { a, b } }
the types do not match, because the type of this expression is
"[alpha, alpha set set]" and not "[alpha, alpha set]".
Can anyone explain me where I am wrong?
--
Michał Czardybon

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