SPEAKER: Klaus Thiel
         LMU Muenchen
         thiel@math.lmu.de
 TITLE: Constructive Finiteness

Dirichlet's Schubfachprinzip, aka Pigeonhole Principle,  states
that if k pigeons are put into l pigeonholes, and if k > l, then
at least one pigeonhole must contain more than one pigeon. In a
set-theoretic framework this principle reads as "Every injection
on a finite set into itself is surjective." and can easily be
shown in a classical setting.

In Constructive Set Theory some more care is needed also because
there are at least 4 different notions of finitenessto
distinguish, which are classically equivalent, e.g. finite and
finitely enumerable. I will present the different notions of
finiteness and, if time permits, a proof of the Pigeonhole
Principle for finitely enumerable sets.


REFERENCES

[1] Peter Aczel and Michael Rathjen
    "Notes on Constructive Set Theory"
    http://www.ml.kva.se/preprints/meta/AczelMon_Sep_24_09_16_56.rdf.html