Is there a characterization of the topos of finite sets in the internal language?

Question

The topos ${\mathcal{Set}}$, at least as axiomatized in ETCS, is a well-pointed topos that satisfies the axiom of choice and has a natural numbers object.

Is there a characterization of the topos ${\mathcal{FinSet}}$ in the internal language?

Answer 1

Characterization is too strong; there are many models of $\operatorname{ETCS}$, so its axioms don't characterize $\operatorname{Set}$ either. But I'll interpret your question as asking how the axioms of $\operatorname{ETCS}$ might be changed if the intended model is $\operatorname{Fin}\operatorname{Set}$ instead of $\operatorname{Set}$.

Of course, you must remove the existence of the natural numbers object, and that might be sufficient; I mean, if you just want to have a topos whose internal mathematics is finitist in the weak sense that it doesn't assume the existence of any completed infinity, then this is sufficient. Both $\operatorname{Fin}\operatorname{Set}$ and $\operatorname{Set}$ are models of this theory.

If you want to more assertively claim that the objects should be finite sets, then a strong way to do this is to add the following axiom scheme, where $\Phi$ is any property (in the language of $\operatorname{ETCS}$) of sets (objects): $$ \Phi(0) \;\Rightarrow\; (\forall\,S\colon \operatorname{Ob},\; \Phi(S) \;\Rightarrow\; \Phi(S + 1)) \;\Rightarrow\; \forall\,S\colon \operatorname{Ob},\; \Phi(S) \text.$$ (Here I've chosen a particular way of phrasing the language of $\operatorname{ETCS}$ that hopefully makes sense to you.)

We can make this a finite axiomatization by requiring finiteness set by set: $$ \forall\,X\colon \operatorname{Ob},\; \forall\,\mathcal{C}\colon \mathcal{P}\mathcal{P}X,\; \emptyset_X \in_{\mathcal{P}X} \mathcal{C} \;\Rightarrow\; (\forall\,S\colon \mathcal{P}S,\; \forall\,a\colon X,\; \neg\,(a \in_X S) \;\Rightarrow\; S \in_{\mathcal{P}X} \mathcal{C}\;\Rightarrow\; S \cup_X \{a\}_X \in_{\mathcal{P}X} \mathcal{C}) \;\Rightarrow\; \forall\,S\colon \mathcal{P}X,\; S \in_{\mathcal{P}X} \mathcal{C} \text{.}$$ This does induction over subsets of an arbitrary set $X$ rather than over sets themselves. (Thanks to Ingo Blechschmidt for reminding me that this can be done!) Actually, the clause $\neg\, (a \in_X S)$ can be omitted, giving an a priori weaker axiom (Kuratowski finiteness), which is equivalent in a boolean topos.

The axiom scheme proves the above axiom, but I haven't gone through all of the sentences of $\operatorname{ETCS}$ to see if the axiom proves each instance of the axiom scheme. (Offhand, I'd guess not.)