The legitimacy of topos theory and intuitionism.

Solution 1:

I think I would answer by a combination of the following, though I'm not absolutely positive that this answers your question. Please feel free to engage in a discussion :-)

1. What the internal logic of a given topos turns out to be is just a fact of life, hence to a certain degree any philosophical concerns about the logic go beside the point: Sure, I would love the axiom of choice to be true internally to any topos, but that is just plain false, irrespective of my metatheory.
2. The internal logic of some specific toposes is particularly interesting and one can well argue for their merit on general philosophical (non-topos-theoretic) grounds. For instance, the internal logic of $\mathrm{Set}$ is ordinary classical logic (assuming classical logic on the meta level -- else consider the "smallest dense subtopos of $\mathrm{Set}$", this topos always validates classical logic even if your metatheory does not), the internal language of the effective topos is "Russian constructivism" and so on.
3. Yes, one perspective on the internal logic of toposes is that it is just a rhetorical tool for simplifying working with the toposes. However, I would take issue with the word "just". For instance:

• The external translation of the internal statement "$f$ is injective" made about some morphism $f : F \to G$ of sheaves on a topological space $X$ is just that all the components $f_U : F(U) \to G(U)$ are injective. Hence the internal statement and the external one are more or less of the same complexity. Judging merely from this example, it's easy to get the impression that the internal language is not very interesting.
• However, the external translations of the internal statements "any nonunit of $\mathcal{O}_{\mathrm{Spec}(A)}$ is zero" and "any ideal of $\mathcal{O}_{\mathrm{Spec}(A)}$ is not not finitely generated" (valid if $A$ is an arbitrary reduced ring, not necessarily a field or Noetherian) are quite unwieldy. (See for instance page 22 of these notes for the translation of one of these.) You could not easily use them in ordinary proofs. They are accessible to us only thanks to the internal language machinery. And it turns out that they are quite useful in some situations. For instance, the proof of Grothendieck's generic freeness lemma in algebraic geometry can be shortened to just a short conceptual paragraph of text if those statements are employed. In a couple of days you will find the details of this example spelled out in this early draft.

Solution 2:

I just see topoi as a generalization of the concept of powerset.

A topos can be viewed as a subcategory of a category of presheafs preserving a bunch of the nice properties of a category of presheafs.

A category of presheafs $[C^{\text{op}}, \text{Set}]$ is not really so different from a set of subsets $[X, 2]$ but just a higher version of the concept. You can think of prestacks $[C^{\text{op}}, \text{Grpd}]$ or displayed categories $\text{Lax}[C, \text{Span}]$ (lax double functors into Span) or any number of other variations on the concept.

My take is it is only a coincidence that presheafs in $\text{Cat}$ happen to be "nice places to do math in" and really the core concepts of subobjects and indexing are very unrelated.

Now it seems to me that of course subobjects in $\text{Set}$ are going to reflect the nature of $\text{Set}$ and be "nice" in certain ways mathematicians might like. The same goes for fields of sets in $\text{Set}$. I think the same probably goes for sheaves in $\text{Cat}$. I think the "logical validity" of categories of sheaves ought to be valid so much as you believe $\text{Cat}$ is logically valid.

Unfortunately $\text{Cat}$ isn't really a nice place to work. But figuring out how to "fix" category theory is really hard. The problems get really bad in higher category theory. For example, in many respects simplicial sets are nicer than infinity categories but I severely doubt some sort of concept of "field of simplicial sets" is really what you want.

But anyway here is my argument. Sheaves in $\text{Cat}$ are bad because $\text{Cat}$ is bad. It's perfectly reasonable to find some alternative formalization (the category of comonads with respect to composition in the category of polynomial endofunctors for example) and figuring out an alternative perhaps nicer behaved notion of sheaf. There's lots of research to make category theory "nicer." It's just it's far easier to say "topoi are nice places to do math in" than to say "topoi are a kind of a bodge but they mostly work except for a few perverse examples."

Now personally I don't believe in "logical validity" at all. I consider myself a formalist and the dual $\text{Set}^{\text{op}}$ is just as logically valid as $\text{Set}$ as far as pushing symbols around goes anyhow. Personally I think the concept of topos is bad because topoi are way too strong for my own purposes of substructural logic and programming languages. The Kappa calculus doesn't even have exponentials much less subobject classifiers.