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