First time asking a question here. I'm working my way through Goldblatt's Topoi, and I'm struggling with the internal/external distinction when it comes to 'topos logic'.

My understanding is that, in a topos $E$:

  1. In the semantics using a valuation function assigning atoms to arrows in HomSet$(1, \Omega)$ ($\S$6.7), a statement $p$ is valid in $E$ when all such valuations result in $V(p) = \textbf{true}$.
  2. A statement is valid in $E$ iff it is valid in $\text{Sub}(1)$ (using some valuation on the subobject algebra).
  3. In general, Sub($d$) for any object $d$ in a topos will be a Heyting algebra.
  4. Since, (a) Heyting algebras model intuitionistic logics, (b) Sub(1) and $E$ have the same tautologies/entailment relation, and (c) Sub(1) is a Heyting algebra, we have that $E$, in general, models an intuitionistic logic.

It is mentioned ($\S$7.4) that these semantics define an 'external' logic, since the valuation is an externally defined function. My question is then what is the 'internal' logic? It looks like the internal logic is simply the previously defined external logic but with all references to HomSet($1, \Omega$) arrows removed and replaced by identity arrows on $\Omega$. Is this description correct? Also, how would we describe valuation/validity/entailment in this internal logic?

Furthermore, Goldblatt says that while it's the internal logic that's used for axiomatising set theory, the external logic is useful for understanding the connection to intuitionistic logic. However, considering that they can disagree (for example, the topos $M_2$ with its non-classical internal logic and classical external logic), I don't understand how examining the external gives any insight into the internal (whatever that may be).

I'm trying to understand the connection between toposes and intuitionistic logic (at least in the zeroth order) for a research project, however my department has neither any category theorists nor any formal logicians! Hence me turning to this site. So thanks anyone that considers these questions!

  • 6
    $\begingroup$ I think the distinction between internal/external in Goldblatt's sense is not in common use. For one thing, I don't think external logic is supposed to depend on the topos under consideration – hence the name external! But there are concepts which admit both an internal interpretation and an external interpretation and sometimes these differ. For example, given a morphism $f : X \to Y$ in a topos, "there is a morphism $g : Y \to X$ such that $\forall x : X . g (f (x)) = x$" externally means $f : X \to Y$ is a split epimorphism, but internally only means that $f : X \to Y$ is an epimorphism. $\endgroup$
    – Zhen Lin
    Oct 6, 2020 at 9:50
  • 2
    $\begingroup$ @ZhenLin You can have a epimorphism $f : X \to Y$ in a topos for which the (internal) interpretation of $\exists g : X^Y, \forall x : X, g(f(x)) = x$ is not true. My favorite counterexample: in the topos $\mathbb{C}$, consider the sheaf $\mathfrak{S}$ of analytic functions, and the differentiation morphism $D : \mathfrak{S} \to \mathfrak{S}$. This is an epimorphism; but there does not exist an inverse to $D$ on any nonempty open subset of $\mathbb{C}$ because such a subset would have to contain some punctured disc. $\endgroup$ Oct 7, 2020 at 23:47
  • 1
    $\begingroup$ Sorry, I meant right inverse of $D$ - and so we would be talking about interpretations of $\exists g : X^Y, \forall y : Y, f(g(y)) = y$. $\endgroup$ Oct 8, 2020 at 0:23
  • 1
    $\begingroup$ Yes, it's a bit tricky. Not every epimorphism will "internally split", unless you have the internal axiom of choice, which is different from the external axiom of choice. $\endgroup$
    – Zhen Lin
    Oct 8, 2020 at 1:59

1 Answer 1


External and internal logics of topoi serve to build models of formal theories. External logic directly uses the subobject classifier $\Omega$, so it only makes sense in topoi. Internal logic is more general, it can be defined in categories with less structure than topoi, as explained here. Roughly speaking, to define the truth in a topos $\mathcal{T}$ of a proposition $P$ with free variables $x_1,\dots,x_n$, you need to first choose objects of $\mathcal{T}$ to interpret the types of the $x_i$'s. Let $\tau(x_i)$ denote this interpretation as objects of $\mathcal{T}$. Theories like Peano arithmetic or ZFC set theory only have one type, natural number and set respectively, so their $\tau$ will be constant (only one object of $\mathcal{T}$). But more complex theories can have a varying $\tau$. Then the external truth of proposition $P$ is a set-function $$ P_{ext} : Hom(1,\tau(x_1))\times\dots\times Hom(1,\tau(x_n)) \to Hom(1,\Omega) $$ So given the values of the $x_i$'s as generalized elements of the $\tau(x_i)$'s, we get an external truth value for $P$ as a generalized element of $\Omega$. We say that topos $\mathcal{T}$ externally satisfies $P$ when $P_{ext}$ is constantly $\top$. The function $P_{ext}$ is defined by structural recursion on the logical connectives in formula $P$. Now the internal truth of $P$ forgets about elements, replaces $Hom(1,X)$ by $X$, replaces cartesian product by $\mathcal{T}$'s product and requests that the set-function becomes a morphism of $\mathcal{T}$, $$ P_{int} : \tau(x_1)\times\dots\times \tau(x_n) \to \Omega $$ By definition of the subobject classifier $\Omega$, $P_{int}$ is a subobject of $\tau(x_1)\times\dots\times \tau(x_n)$, and that is the generalization of internal logic to categories other than topoi. We say that topos $\mathcal{T}$ internally satisfies $P$ when $P_{int}$ is the largest suboject, i.e. an isomorphism to $\tau(x_1)\times\dots\times\tau(x_n)$. Likewise, $P_{int}$ is defined by structural recursion on the logical connectives of $P$. Because the structural recursions defining $P_{ext}$ and $P_{int}$ are different, the external satisfaction of $P$ in $\mathcal{T}$ is not equivalent to its internal satisfaction.

Concerning the connection between topoi and intuitionistic logic, you probably need to first decide whether you are doing intuitionistic or classical mathematics (your meta-theory). If you choose an intuitionistic meta, then you immediately have a problem proving that Set is a topos. Because for each set inclusion $A\subset B$, you need to define a characteristic function $\chi : B \to 2$. The classical argument that $\chi(x)=1$ when $x\in A$ and 0 otherwise uses excluded middle, and so does not apply in intuitionistic mathematics. Likewise you have an intuitionistic headache for the semantics of quantifiers $\forall$ and $\exists$. The classical argument that $\forall x,P$ evaluates to 1 when $P$ constantly evaluates to 1 also uses excluded middle.

Now you can also be interested in intuitionistic mathematics other than topoi, for example basic algebra or analysis. And because you refuse excluded middle, you sometimes face a proposition $P$ that you can prove classically, but fail to prove intuitionistically. Then you wonder: is it because you haven't tried hard enough intuitionistically, or is it because the proof fundamentally depends on excluded middle? If you think the latter, then topoi can come in and help. Topoi give models of mathematics where the excluded middle is not always valid, and it is their main advantage here! If you find a topos $\mathcal{T}$ where $P$ is false, then you cannot prove $P$ intuitionistically. Because if you could, then your intuitionistic proof would not use excluded middle, and so make $P$ true in $\mathcal{T}$. That technique works either when $P$ is externally false or internally false in $\mathcal{T}$.


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .