Next: Algebra Up: Set Theory Previous: The Subset Constructor

## Intervals

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 array  a of type A as
```        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 n is the cardinality of A.

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 int
```
The proof of such a proposition in Nuprl will include a procedure which, given a function f from the interval to the interval with m > n, produces the values i and j for which . The constructive proof is considerably harder than the (trivial) proof of the classically interpreted pigeon--hole principle, but the information contained in the constructive proof is correspondingly much greater.

Next: Algebra Up: Set Theory Previous: The Subset Constructor

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