An Induction Principle and Pigeonhole Principles for K-Finite Sets

Thumbnail Image

Date

Authors

Journal Title

Journal ISSN

Volume Title

Publisher

Abstract

Description

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.

Keywords

Logic

Citation

URI

http://salesiana.dossiersoluciones.com/handle/123456789/152907

Consulte el texto completo en el siguiente enlace:

https://arxiv.org/abs/math/9405204
 http://arxiv.org/abs/math/9405204

Collections

arXiv