Topos theory and higher-order logic

Before focusing on the specific question, I'd like to provide some context. First, every (non-trivial) topos has a Boolean subtopos. This is essentially what you say, and it roughly corresponds to the double negation interpretation of classical logic into intuitionistic logic. However, one of the things that makes toposes interesting is that many things are toposes, but relatively few things are Boolean toposes. Similarly, (part of) what makes intuitionistic type theory interesting is that it's the internal language of a topos. Restricting to a classical theory discards many relevant examples. For example, as the name "topos" suggests, a significant application is to topology with a topological space giving rise to a topos. Restricting to Boolean toposes is like only considering Stone spaces which largely defeats the purpose of topology. (One could say this paragraph is an [partial] argument for why the law of excluded middle is not a "good principle", though it is certainly convenient when it holds.)

The way predicates are interpreted in categorical logic for an arbitrary category is as subobjects. A predicate $P$ on "individuals" of sort $A$ is viewed as a subobject of the object $A$ in a category, i.e. as a(n equivalence class of) monomorphism(s) $P \hookrightarrow A$. A subobject classifier allows us to reify these subobjects as terms. That is, the formula $a:A\vdash P(a)$ becomes the term $a:A \vdash \chi_P(a):\Omega$. We can then recover the formula as $a:A\vdash P(a)\Leftrightarrow \chi_P(a)=_\Omega\top$. In fact, this equivalence is the heart of what a subobject classifier is. Characteristic functions $\chi_P$ that factor through $\mathbf{2}$ correspond to decidable predicates, i.e. predicates for which the law of excluded middle holds. As a formula $a:A\vdash P(a)\lor\neg P(a)$ or via a characteristic function $a:A\vdash (\chi_P(a)\lor\neg\chi_P(a))=_\Omega\top$. The former states that $P$ is a complemented or decidable subobject of $A$. In the latter, $\lor$ and $\neg$ are operations on $\Omega$ rather than logical connectives.

A topos where $\Omega \ncong \mathbf{2}$ is one whose internal logic has some propositions that are not decidable in the above sense. If you restrict yourself to Boolean-valued characteristic functions, then you are restricting yourself to only the decidable propositions in your internal logic. This is a completely coherent thing to do, but it means there are formulas you can state which will have no Boolean-valued characteristic function. They will, however, always have an $\Omega$-valued characteristic function. If you identify predicates with Boolean-valued characteristic functions, then what you are doing is equivalent to interpreting into a Boolean subtopos of whatever topos you started with.


The main idea connecting logic to set theory is the idea that propositions are subsets.

On the one hand, if you are interpreting propositional logic in some (set-theoretic) domain $D$ of discourse, then each proposition gets interpreted as a subset of $D$, and connectives are operations on subsets.

On the other hand, given any set $D$, we can make $\mathcal{P}(D)$ into a Boolean lattice in which we can compute with propositional logic.

And this all extends fairly naturally to predicates and quantifiers and such.


When connecting logic to category theory we use basically the same idea, except instead that propositions are subobjects rather than subsets.

The posets $\operatorname{Sub}(X)$ of subobjects of $X$ are of crucial importance to doing propositional logic, and more generally we are interested in the maps back and forth between $\operatorname{Sub}(X)$ and $\operatorname{Sub}(Y)$ that may be induced by a map $X \to Y$.

So, for internal first-order logic, classifying subobjects really is the thing we want. Even better, in a topos, $\operatorname{Sub}$ is a representable functor

$$ \operatorname{Sub}(-) \cong \hom(-, \Omega) $$

So, while $\operatorname{Sub}(-)$ is a relatively complicated object, in a topos the whole thing effectively collapses down to being a single object $\Omega$, thus allowing the internal logic to be treated in a more elementary way.