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.


next up previous contents index
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 up previous contents index
Next: Algebra Up: Set Theory Previous: The Subset Constructor



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