Also see Decremented Interval and Interval for examples of Nuprl4 theorems mentioning intervals. It turns out that decremented specification of intervals has seen greater use than direct indication of both endpoints. For more discussion (and formalization) of finiteness and the pigeon hole principle see Intro to Counting.

Subsets of the integers of the form are especially useful.
We call them * intervals,* and they are defined as follows.
First we define the symbol ` <=` to mean ``less than or equal to'' with
the following definition:

<x:int>\<=<y:int>==((<y><<x>)->void)}.Now the concept of interval can be defined by

{<n:int>,...,<m:int>}=={x:int| <n><=x # x<=<m>}.Using intervals we can define the concept of an

a:{1,...,n}->A.

A very important concept in set theory is the concept of
* equal cardinality*. We shall use the
term * equipollent* to signify the type--theoretic
analogue of equal cardinality. As in classical set theory,
two types are equipollent if there are a pair of invertible
functions between them. This is captured by the following definition.

<A:type> is equipollent with <B:type>== (some ab:<A>-><B>.some ba:<B>-><A>.all x:<A>.all y:<B>. ba(ab(x))=x in <A> & ab(ba(y))=y in <B>)In the constructive account, however, we must exhibit the two functions that establish equipollence, so it is not permissible to use the Schroeder--Bernstein theorem, for example, to establish equipollence. Thus equipollence is not identical to the classical notion of equal cardinality.

The following three Nuprl theorems express basic facts about equipollence.

>>all A:U1. A is equipollent with A >>all A:U1.all B:U1. A is equipollent with B => B is equipollent with A >>all A:U1.all B:U1.all C:U1. A is equipollent with B & B is equipollent with C => A is equipollent with C

Using the notions of intervals and equipollence we can define the concept of a
* finite type*.
We say that a type **A** is finite if and only if
it is equipollent
with some interval.

<A:type> is finite== some n:int.{1,...,n} is equipollent with <A>We say that

A nontrivial statement that can be made with the definitions introduced in this section is the pigeonhole principle. The following Nuprl theorem expresses the principle.

>>all n:int.all m:int. all f:{1,...,m}->{1,...,n}. 0<n<m => some i,j:int.i<j & f(i)=f(j) in intThe proof of such a proposition in Nuprl will include a procedure which, given a function

Thu Sep 14 08:45:18 EDT 1995