[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Functions and Operators

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.