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

{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

Thu Sep 14 08:45:18 EDT 1995