[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:
- $\Omega$ plays a special role in turning subobjects into elements of a power object in the topos. $Sub(-)\cong Hom(-,\Omega)$
- $\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).