Return to Revisions

This is perhaps a rather strange example. There is a paper of Andreas Blass An induction principle and pigeonhole principle for K-finite sets (J. Symbolic Logic 59, 1995, 1186-1193) where the goal is to give an intuitionistic proof of that there is no surjection from $X$ onto $X+1$ when $X$ is finite (Theorem 2). Before proving this result, Blass proves a strong induction principle for finite sets (Theorem 1). The proof of Theorem 1 uses ordinary induction with a base case, but the proof of Theorem 2 uses the strong induction principle of Theorem 1 instead. Blass' proof of Theorem 2 very straightforward, but I think that a direct proof of Theorem 2 (along the same lines) would be unbearably long.