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

*From*: Andrew Helwer <andrew...@xxxxxxxxx>*Date*: Mon, 23 Mar 2015 22:22:31 -0700 (PDT)*References*: <888ba871-f342-4159-8f60-5b055ee40813@googlegroups.com> <2556ED24-313D-4CDA-AD2C-ED3DAAD7D749@gmail.com> <BBBDEFE5-B35E-4BAE-AAB3-03C9BDC11EE0@gmail.com>

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:

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

**References**:**Functions and Operators***From:*Andrew Helwer

**Re: [tlaplus] Functions and Operators***From:*Stephan Merz

**Re: [tlaplus] Functions and Operators***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] Functions and Operators** - Next by Date:
**Re: Functions and Operators** - Previous by thread:
**Re: [tlaplus] Functions and Operators** - Next by thread:
**Re: Functions and Operators** - Index(es):