Next: Intervals Up: Set Theory Previous: Set Theory

## The Subset Constructor

The expression of concepts from set theory in Nuprl is facilitated by the availability of the set   type constructor as one of the primitive constructors of the underlying Nuprl logic. The notation for this constructor is { x:A|B}. Intuitively the set type constructor first forms a dependent sum of the two component types and then discards the second member of each pair in the dependent sum. The members of this type are those members a of the type A such that is inhabited. Recalling the propositions--as--types principle,  we may think of B as a propositional function and as a proposition. The proposition is true when the corresponding type is inhabited; thus the notation { x:A|B} defines the type whose members are members a of A that make the proposition true. This is essentially what the classical set formation construct means.

The simplest statements about sets that one can make involve subsets  of a specific type such as int. In Nuprl we may represent such sets as set types over int in the following fashion. Given a predicate P on the integers, the set corresponding to P is,

```        {x:int | P(x)}.
```
This set  type denotes those elements of int which satisfy P. Two important aspects of this type are that its members are elements of int and that the proof of for an element a of int is not available in computations. For example, to prove that 9 belongs to
```        {x:int | some y:int. ~(y=x in int) & x mod y=0 in int}
```
we must prove that some number, such as 3, satisfies the defining predicate, but we do not keep this factor as part of the membership condition. This means that from an assumption such as y in {x:int | P(x)} we do not have access to the proof of . This aspect of the subset constructor comes out as a restriction on the way hypotheses can be used in the set--elimination rule.

Next: Intervals Up: Set Theory Previous: Set Theory

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995