An Induction Principle and Pigeonhole Principles for K-Finite Sets

Blass, Andreas

Blass, Andreas

J. Symbolic Logic, Tome 60 (1995) no. 1, p. 1186-1193 / Harvested from Project Euclid

Résumé

We establish a course-of-values induction principle for K-finite sets in intuitionistic type theory. Using this principle, we prove a pigeonhole principle conjectured by Benabou and Loiseau. We also comment on some variants of this pigeonhole principle.

Publié le : 1995-12-14
Classification:

@article{1183744870,
     author = {Blass, Andreas},
     title = {An Induction Principle and Pigeonhole Principles for K-Finite Sets},
     journal = {J. Symbolic Logic},
     volume = {60},
     number = {1},
     year = {1995},
     pages = { 1186-1193},
     language = {en},
     url = {http://dml.mathdoc.fr/item/1183744870}
}

Blass, Andreas. An Induction Principle and Pigeonhole Principles for K-Finite Sets. J. Symbolic Logic, Tome 60 (1995) no. 1, pp.  1186-1193. http://gdmltest.u-ga.fr/item/1183744870/