[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.