show/hide this revision's text 2 addendum

I guess it's hard to understand this one without seeing the proofs. So I'll give a similar proof (without the intuitionistic fuss, for clarity). The strong induction on finite sets I will use is the following.

(SI) If $\mathcal{K}$ is a family of sets such that if all proper subsets of $A$ are in $\mathcal{K}$ then $A$ is in $\mathcal{K}$ too, then $\mathcal{K}$ contains all finite sets.

Let $\mathcal{K}$ be the family of all sets $A$ such that if $A$ is a proper subset of $B$ and $f:A \to B$ then the image $f[A]$ is not all of $B$. I claim that $\mathcal{K}$ satisfies the hypothesis of (SI).

Suppose all proper subsets of $A$ are in $\mathcal{K}$. Let $B$ be a proper superset of $A$. Given $f:A \to B$, we consider two cases.

If $f^{-1}[A] = A$, then $f[A] \subseteq A$ and so $f[A]$ is certainly not all of $B$.

If $A' = f^{-1}[A]$ is a proper subset of $A$. Then $A' \in \mathcal{K}$ and hence $f[A']$ is not all of $A$. But then $A \setminus f[A'] = A \setminus f[A] \subseteq B \setminus f[A]$, which shows that $f[A]$ is not all of $B$.
show/hide this revision's text 1 [made Community Wiki]

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.