AN INDUCTION PRINCIPLE AND PIGEONHOLE PRINCIPLES FOR K-FINITE SETS

Authors
BLASS A
Citation
A. Blass, AN INDUCTION PRINCIPLE AND PIGEONHOLE PRINCIPLES FOR K-FINITE SETS, The Journal of symbolic logic, 60(4), 1995, pp. 1186-1193
Citations number
12
Categorie Soggetti
Mathematics, Pure",Mathematics
Journal title
The Journal of symbolic logic → ACNP
ISSN journal
00224812
Volume
60
Issue
4
Year of publication
1995
Pages
1186 - 1193
Database
ISI
SICI code
0022-4812(1995)60:4<1186:AIPAPP>2.0.ZU;2-1
Abstract
We establish a course-of-values induction principle for K-finite sets in intuitionistic type theory. Using this principle, we prove a pigeon hole principle conjectured by Benabou and Loiseau. We also comment on some variants of this pigeonhole principle.