Email Gateway (Aug 18 2022 at 12:22): Email Gateway (Aug 18 2022 at 12:22):From: Michal Czardybon <mczard@poczta.onet.pl>
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?
Last updated: May 03 2024 at 08:18 UTC