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



Michal,

On Sat, 2008-09-13 at 12:45 +0200, Michal Czardybon wrote:
> 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?

your following questions seem to target (Isabelle's implementation of)
higher-order logic.  (Note that Isabelle also supports other logics --
e.g., ZF set theory.)  A formal account of the logic's syntax and
semantics can be found in

M. J. C. Gordon and T. F. Melham, editors. Introduction to HOL: A
theorem proving environment for higher order logic. Cambridge University
Press, 1993.

Regarding function application, the only rule to remember is the following:
if "f" is a term of (function) type "A => B" and "x" is a term of type "A",
then "f x" is a term of type "B".

> 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?

That would indeed be an incorrect typing.  Since in your example
"{a, b}" and "c" must have the same type, the type of "c" must be
"alpha set" (provided the type of "a" and "b" is "alpha").  The type
of "{ {a, b}, c }" will then be "alpha set set".

> 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]".

"a : { { a, b } }" is not type-correct.  If "a" has type "alpha", then
"{ { a, b } }" has type "alpha set set", whereas the membership
operator ":" expects its second argument to be of type "alpha set".

If you enter
  term "a : { {a, b} }"
in Isabelle, you will get an error message to that effect.

Hope this helps,

    Tjark






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