Topos theory and higher-order logic

Question

[Updated in light of some of the comments and answers below]

This is a question about the relationship between higher-order logic and topoi. It's well-known that every topos gives a model of higher-order logic, in which the type in which sentences inhabit is taken to be the subobject classifier $\Omega$.

As far as I can see $\Omega$, qua interpretation of higher-order logic, is playing two distinct roles and I can't see why they're being identitified:

1. $\Omega$ plays a special role in turning subobjects into elements of a power object in the topos. $Sub(-)\cong Hom(-,\Omega)$
2. $\Omega$ plays the role of being the truth values of sentences.

There is, for example, another natural choice for the second role, namely: $2$ (the coproduct of the terminal object with itself). Given a choice of arrow $true: 1\to 2$ we can interpret higher-order logic within a topos in an analogous way.

I'd like to know if there's any reason not to split these two roles. Is there a principle of higher-order logic that forces these two roles to coincide? A natural candidate would be the schema:

• $\forall f(\forall xy(fx=fy \to x=y) \to \exists G \forall z(Gz \leftrightarrow \exists xfx=z))$

where $f:A\to B$, $x,y: A$, $z:B$ and $G:B\to \Omega$. This schema is schematic in the types $A$ and $B$. Does this sentence fail if I use $2$ in a topos instead of $\Omega$? Or does $\forall xy(fx=fy \to x=y)$ fail to express the fact that $f$ is mono? Or does $\forall z(Gz \leftrightarrow \exists xfx=z)$ fail to express the fact that $G$ is a characteristic function of $f$. Or what?

Lastly, just to clarify where I'm coming from: I'm mainly interested in topos theory as an interpretation of higher-order logic. I realise there are lots of interesting differences between topoi that lead to the same sentences of higher-order logic being true, but these aren't the sorts of differences I'm interested in (at least for these purposes).

Answer 1

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.

Answer 2

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.