The legitimacy of topos theory and intuitionism.

Question

This is an exercise in critical thinking. I am not looking, therefore, for opinions on the matter; rather: I would like to know the evidence (whatever that might mean).

Background:

I have a longstanding interest in different types of logic:

• The Adjunction $\_\times A\dashv (\_ )^A$ for Preorders: The Deduction Theorem.
• Understanding an example of a subobject classifier.
• Defining "Penon Infinitesimals".
• Verifying a Construction Satisfies the $\Omega$-axiom.
• What makes "the topos $\mathbf{M}_2$" such a good counterexample?
• Equivalence of categories preserves subobject classifiers.
• Priest's nonstandard $N$: showing $\not\vdash_N \square p\supset p$.
• In $\mathbf{Sets}^\mathbf{Q}$, prove the subobject classifier $\Omega$ is given by $\Omega(q)=\{r\mid r\in\mathbf{R^+},r\ge q\}.$
• What are the prerequisites for topos theory?

I have read (most of) Goldblatt's, "Topoi: A Categorial Analysis of Logic." I stopped doing the exercises entirely in its fourteenth chapter.

I'm aware of "The Uses and Abuses of the History of Topos Theory," but it's behind a paywall I can't afford.

I have read most of Priest's, "An Introduction to Nonclassical Logic, Second Edition: From If to Is," although I don't recall much on intuitionism, from what I have read.

A recent, private conversation I had online called into question the legitimacy – the efficacy, the applicability, the rigour – of topos theory and its implications about constructive mathematics.

The Question:

Are the different logics given by topoi legitimate?

Thoughts:

What do I mean by, "legitimate"?

Well, not to be glib, I mean the second sense as given by this Google search:

able to be defended with logic or justification; valid.

I find it difficult to improve upon that definition.

What kind of answer am I looking for?

I'm not sure. Perhaps a list of reputable academics – like Prof. Peter Johnstone – working in the area, alongside a brief summary of their position on intuitionism and/or constructivist logic; I don't know. Some applications wouldn't go amiss. Suggestions on further reading are welcome.

Please help 🙂

Answer 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.