Hostname: page-component-cd9895bd7-jkksz Total loading time: 0 Render date: 2024-12-19T04:52:25.887Z Has data issue: false hasContentIssue false
  • English
  • Français

An induction principle and pigeonhole principles for K-finite sets

Published online by Cambridge University Press:  12 March 2014

Andreas Blass
Andreas Blass*
Affiliation:
Mathematics Department, University of Michigan, Ann Arbor, Michigan 48109, E-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

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 Bénabou and Loiseau. We also comment on some variants of this pigeonhole principle.

Keywords

Primary 03F55
Type
Research Article
Information
The Journal of Symbolic Logic , Volume 60 , Issue 4 , December 1995 , pp. 1186 - 1193
Copyright
Copyright © Association for Symbolic Logic 1995

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

[1]Acuña-Ortega, O. and Linton, F. E. J., Finiteness and decidability. I, Applications of sheaves (Fourman, M. P., Mulvey, C. J., and Scott, D. S., editors), Lecture Notes in Mathematics, vol. 753, Springer-Verlag, Berlin, 1979, pp. 80–100.CrossRefGoogle Scholar
[2]Barr, M., Toposes without points, Journal of Pure and Applied Algebra, vol. 5 (1974), pp. 265–280.CrossRefGoogle Scholar
[3]Bell, J. L., Toposes and local set theories, Oxford Logic Guides, vol. 14, Oxford University Press, Oxford, 1988.Google Scholar
[4]Bénabou, J. and Loiseau, B., Orbits and monoids in a topos, Journal of Pure and Applied Algebra, vol. 93 (1994), pp. 29–54.CrossRefGoogle Scholar
[5]Boileau, A. and Joyal, A., La logique des topos, this Journal, vol. 46 (1981), pp. 6–16.Google Scholar
[6]Coste, M., Langage interne d'un topos, Séminaire Bénabou, Université Paris-Nord, Paris, 1973.Google Scholar
[7]Fourman, M. P., The logic of topoi, Handbook of mathematical logic (Barwise, J., editor), North-Holland, Amsterdam, 1977, pp. 1053–1090.CrossRefGoogle Scholar
[8]Fourman, M. P. and Scott, D. S., Sheaves and logic, Applications of sheaves (Fourman, M. P., Mulvey, C. J., and Scott, D. S., editors), Lecture Notes in Mathematics, vol. 753, Springer-Verlag, Berlin, 1979, pp. 302–401.CrossRefGoogle Scholar
[9]Freyd, P., Aspects of topoi, Bulletin of the Australian Mathematical Society, vol. 7 (1972), pp. 1–76, 467–480.CrossRefGoogle Scholar
[10]Johnstone, P. T., Topos theory, London Mathematical Society Monographs, vol. 10, Academic Press, London, 1977.Google Scholar
[11]Kock, A., Lecouturier, P., and Mikkelsen, C. J., Some topos-theoretic concepts of finiteness, Model theory and topoi (Lawvere, F. W., Maurer, C. and Wraith, G. C., editors), Lecture Notes in Mathematics, vol. 445, Springer-Verlag, Berlin, 1975, pp. 209–283.CrossRefGoogle Scholar
[12]Osius, G., Logical and set-theoretical tools in elementary topoi, Model theory and topoi (Lawvere, F. W., Maurer, C. and Wraith, G. C., editors), Lecture Notes in Mathematics, vol. 445, Springer-Verlag, Berlin, 1975, pp. 297–346.CrossRefGoogle Scholar