Well-founded induction does work in the internal logic of a topos. However, you need the proper definition in order to get this to work. Namely, you define a relation $R$ on a type $X$ to be well-founded if for each $S : P(R)$, assuming $\forall x : X, (\forall y : X, y \mathrel{R} x \rightarrow y \in S) \rightarrow x \in S$, then $S$ is the full subset, i.e. $\forall x : X, x \in S$. Note that in a non-boolean topos, the classically equivalent conditions are no longer equivalent to $R$ being well-founded. Namely, $R$ being well-founded is not necessarily equivalent to the condition that every inhabited subset of $X$ has an $R$-minimal element; nor even in a topos with natural numbers object is it necessarily equivalent to the condition that there is no $R$-decreasing sequence.
Now, it would seem at first blush that this is just a tautology: if you assume that the well-founded induction principle is valid for a relation $R$, then the well-founded induction principle is valid for $R$. However, we can still construct ways to build up proofs that certain relations are well-founded. For example:
- The empty relation is always well-founded.
- If a relation $R$ is well-founded, then so is its transitive closure (defined as the internal intersection of all transitive relations containing $R$).
- The sum of two well-founded relations is well-founded, i.e. if $R$ is well-founded on $X$ and $S$ is well-founded on $Y$, then $R \sqcup (X \times Y) \sqcup S$ is well-founded on $X \sqcup Y$.
- Iterating the previous construction, we see that for any metalogical natural number $n$, $\bigsqcup_{i=1}^n 1$ with relation $\bigsqcup_{1 \le i < j \le n} (1_i \times 1_j)$ is well-founded, and it would be natural to treat this as an analog in the topos of the set $[n] = \{ 1, 2, \ldots, n \}$.
- The lexicographic product of two well-founded relations is well-founded.
- If a topos has a natural numbers object $N$, then the graph of the successor morphism is a well-founded relation on $N$; therefore, so is its transitive closure, which is equivalent to $<_N$.
- For an arbitrary relation $R$, define the "accessible elements" of $R$ to be the intersection of all subsets satisfying the well-foundedness closure condition. Then the restriction of $R$ to the subobject of accessible elements is well-founded.
You can also extract certain properties from a well-founded relation. For example:
- A well-founded relation is irreflexive: $\forall x : X, \lnot (x \mathrel{R} x)$.
- Therefore, combining this with the fact about transitive closures, you can prove the metatheorem indexed by metalogical natural number $n$ that $\forall x_1, \ldots, x_n : X, \lnot (x_1 \mathrel{R} x_2 \land x_2 \mathrel{R} x_3 \land \cdots \land x_{n-1} \mathrel{R} x_n \land x_n \mathrel{R} x_1)$. For instance, the case $n = 2$ shows that a well-founded relation is "strictly antisymmetric".
- You can prove an "internal recursion" theorem, in much the same way that you usually prove it in set theory (where the partial functions involved can be modelled for example as certain elements of the exponential type $(\tilde X)^X$ where $\tilde X$ is the partial function classifier).
