Thanks for the book recommendations! The Handbook of Mathematical Logic is peculiarly expensive, but it looks like the University of Washington Library has a copy. I'll check out the Halmos text first.
On Saturday, March 21, 2015 at 6:24:16 AM UTC-7, Stephan Merz wrote:
> For example, \in has type "'a set => bool"
That should (of course) have been "'a => ('a set => bool)". Incidentally, you can define "'a set" simply as an abbreviation for "'a => bool" in HOL, identifying sets and their characteristic predicate (and \in is just [reverse] function application). Then, you can define the set of all values of type 'a as
UNIV :: "'a set" == \lambda x::'a. true
Note that there is a separate such set for every type, in particular
(UNIV :: "'a set") and (UNIV :: "'a set set")
are different for any type 'a, and this helps avoiding paradoxes.
Stephan