*To*: Michal Czardybon <mczard at poczta.onet.pl>*Subject*: Re: [isabelle] I can't understand types in set-membership expressions*From*: Tjark Weber <tjark.weber at gmx.de>*Date*: Sun, 14 Sep 2008 20:49:02 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <48CB99B3.30108@poczta.onet.pl>*References*: <48CB99B3.30108@poczta.onet.pl>

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

**References**:**[isabelle] I can't understand types in set-membership expressions***From:*Michal Czardybon

- Previous by Date: [isabelle] relating 2 theories
- Next by Date: Re: [isabelle] relating 2 theories
- Previous by Thread: [isabelle] I can't understand types in set-membership expressions
- Next by Thread: Re: [isabelle] I can't understand types in set-membership expressions
- Cl-isabelle-users September 2008 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list