# What can be expressed in and proved with the internal logic of a topos?

The title of this post expresses what I really want, which is to learn how to wield the internal logic of a topos more effectively. However, to bring it down to earth, I'll ask a few basic questions about the topos $\mathcal{Grph}$ of directed graphs, whose underlying category is $$\mathcal{Grph}:={\bf Set}^{\mathcal{G}}.$$ Here $\mathcal{G}$ is the indexing category for graphs, with two objects $A$ and $V$ and with two morphisms $src,tgt\colon A\to V\$.

What can I express in the internal logic of the topos $\mathcal{Grph}$, say using the Mitchell-Benabou language or the Joyal-Kripke semantics, or what have you? How can I use this logic to prove things? What kinds of things can't be said or proven in this way?

Below are some concrete questions. In each case when I ask "Can I...", I mean "To what degree can I use the internal language and logic of $\mathcal{Grph}$ to...".

1. Can I express that a graph $X$ is finite, (respectively complete, discrete)?
2. Can I take a graph $X$ and produce the paths-graph $Paths(X)\$, whose vertices are those of $X$ but whose arrows are all finite-length paths in $X$?
3. Can I express that $Paths$ is a monad, i.e. produce some morphism $X\to Paths(X)\$ and another $Paths(Paths(X))\to Paths(X)\$ with some properties?
4. Can I take a graph $X$ and produce the subgraph $L\subseteq X$ consisting of all vertices and arrows that are involved in a loop? (That is, an arrow $a\in X(A)$ is in $L$ iff there exists a path $P$ of length $n$ in $X$ such that $a\in P$ and $P$ is a loop: $P(0)=P(n)\$. A vertex $v\in X(V)$ is in $L$ if it is the source of an arrow in $L$.)
5. Can I prove that if a graph has no loops and finitely many vertices then it has finitely many paths?
6. Can I do something else in $\mathcal{Grph}$ that might be fun and informative?

Maybe this post reflects a basic misunderstanding of how to think about the internal logic of a topos. If so, please set me straight. Also, a quiz question might be nice -- something of the form "see if you can express/prove this in $\mathcal{Grph}$: __."

-
I suspect the answer to all your questions, other than the one about finiteness, is no. In the internal logic of a topos, objects are "sets" and have no further internal structure. That is not to say we can't tack on extra gadgets to make that internal structure visible – for example, we could introduce some local operators to extract the edge set and the vertex set – but then you may as well work from the external point of view. – Zhen Lin Mar 19 '13 at 19:10
The idea of using an internal logic is not to reason in a particular category, but to perform a uniform reasoning for all categories satisfying some properties --- in exactly the same way as there is no sense to use the logic of a particular Heyting algebra to reason about that Heyting algebra. – Michal R. Przybylek Mar 19 '13 at 22:05
Actually, Kuratowski-finiteness can be formulated within geometric logic, and a Kuratowski-finite object in $\textbf{Grph}$ is precisely a graph $G$ with finitely many edges and finitely many vertices, such that the two maps $G(A) \to G(V)$ are surjective. In fact, the finite graphs are precisely the Kuratowski-subfinite objects. – Zhen Lin Mar 20 '13 at 0:01
@Zhen Lin: true, the internal logic talks about all objects as though they were just unstructured sets. But one can still often re-express external local notions in these terms — see e.g. the internal construction of a sheafification. Talking about local operators, for instance, isn’t tacking on anything extra: they can be described entirely using the internal logic itself, as constructions based on certain elements of $\mathcal{P}(\Omega)$. (From the internal point of view, they’re just Grothendieck topologies on the terminal category.) – Peter LeFanu Lumsdaine Mar 21 '13 at 6:34
@Michal: one idea is to use the internal language of a class of categories to prove their general properties. Another idea is to use the internal language of a particular category to prove its properties. @Zhen Lin: you suspect wrong, the game here is precisely to figure out what extras should be added to the general internal language of toposes. The question never said anything about using just "pure" internal language of toposes. – Andrej Bauer Apr 4 '13 at 8:57

In general the internal language of a topos can only express those statements that make sense in every topos. In essence, this limits you to something like bounded Zermelo set theory, without global membership.

The right way to use the internal language of a particular topos, such as your topos of directed graphs, is to enrich the general internal language of toposes with new primitive types and new axioms. If you are lucky you may be able to add just axiom and define the new types (i.e., the new types can be characterized in the internal language). Let us see what these may be in the case of the topos of directed graphs.

Because we are dealing with a presheaf topos we can tell in advance that the (covariant) Yoneda embedding $y : \mathcal{G} \to \mathbf{Set}^\mathcal{G}$ will give us something important. Indeed, $y(V)$ is the graph with one vertex and no arrows, while $y(A)$ is the graph with two vertices and one arrow in between. Let me write $V$ and $A$ instead of $y(V)$ and $y(A)$, respectively. We might call $V$ "the vertex" and $A$ "the arrow". We call the objects of our topos "graphs", obviously.

Simple calculations reveal that, for a given graph $G$:

• $G \times V$ is the associated discrete graph on the vertices of $G$.
• $G^V$ is the associated complete graph on the vertices of $G$.
• $G \times A$ is the following graph: for each vertex $g$ in $G$ we get two vertices $(g,s)$ and $(g,y)$ in $G \times A$ (think of them as "$g$ as a source" and "$g$ as a target"), and for each arrow $a : g \to g'$ in $G$ we get an arrow $a : (g,s) \to (g',t)$ in $G \times A$. This probably means something to graph theorists, I would not be surprised if they have a name for it.
• $G^A$ is the associated "graph of arrows": the vertices of $G^A$ are pairs of vertices $(g,g')$ of $G$; and for each arrow $a : g \to h$ we get an arrow $a : (g,g') \to (h',h)$ in $G^A$. This makes more sense once you compute the global points of $G^A$: they correspond precisely to the arrows in $G$. Also, it is helpful to think of the vertices of $G^A$ as "potential arrows of $G$".

• A graph $G$ is discrete when the projection $G \times V \to G$ is onto.
• A graph $G$ is complete when the canonical map $G \to G^V$ is onto.

You would like to have the graph of paths $\mathsf{Path}(G)$ of a given graph $G$. I think you've described the wrong gadget, i.e., what you should be looking for is a graph whose global points are the paths in $G$, but there will be many other "potential" things floating around. We have so far not used the fact that there are two morphisms $s, t : A \to V$. These allow us to form "generic paths of length $n$" $P_n$ as pullbacks: $P_1 = A$, $P_2 = A \times_V A$ is the pullback of $s : A \to V$ and $t : A \to V$, and so on. With a little bit of care we should be able to form the object of "generic paths" $P$, equipped with a concatenation operation that turns it into a monoid. I am going to naively guess that the vertices of $P$ are pairs of natural numbers $(k,n)$ with $k < n$ and that arrows are of the form $(k,n) \to (k+1,n)$. But this needs to be checked, and in any case it should be possible to define the "correct" $P$ internally. The graph $\mathsf{Path}(G)$ that you are looking for ought to be the dependent sum $\sum_{p : P} G^p$ (and this looks a lot like a polynomial functor). The monoid structure on $P$ should give you a monad.

Regarding cyclic paths (you call them loops): if I am not mistaken the internally projective graphs are those graphs whose in- and out-degrees are all 1, in other words the cycles and the infinite path stretching in both directions. This should help with getting a grip on cyclic paths. That a graph $G$ is internally projective can be expressed in the internal language as "every $G$-indexed family of inhabited graphs has a choice function", i.e., these are the objects that satisfy the axiom of choice, internally.

The vertex $V$ is a subobject of the terminal object $1$, which is the graph with a single vertex and a single arrow. Thus, there is a corresponding truth value $v \in \Omega$, which is a kind of "intermediate" truth value. We can define a closure operator $j : \Omega \to \Omega$ (a modality) by $j(p) = (v \Rightarrow p)$. This modallity should be called "vertex-wise". Indeed, if $H \hookrightarrow G$ is a subgraph of $G$ then its $j$-closure $\bar{H} \hookrightarrow G$ is the subgraph of $G$ induced by the vertices of $H$. Ah, but this is then the same as the compleement of the complement of $H$, so we see that $j$ is just the double negation closure. (I hope I am doing this right, I am speaking off the top of my head.) If I am correct, then we can define $V$ in the internal language, using an axiom:

Axiom: there is a truth value $v \in \Omega$ such that $(v \Rightarrow p) = \lnot\lnot p$ for all $p \in \Omega$.

Then $V = \lbrace * \in 1 \mid v \rbrace$. We still have to do something about $A$, though.

In any case, my experience with internal languages is that they are well worth using. It takes a bit of effort, thoough, to figure out the optimal way of setting up the internal language of a particular topos. The general idea is to introduce as few new types as possible, characterize them with suitably chosen axioms, and figure out what other useful axioms are valid in your topos.

-
Why is it important for $V$ to be parameter-free definable? – François G. Dorais Apr 4 '13 at 12:23
That was too brief a question... I didn't read the parameter-free requirement in the op's question. I do find it interesting when something is parameter-free definable and I'm happy you are addressing that issue, but I wonder why you find it such a sticking point. – François G. Dorais Apr 4 '13 at 15:15
I am not sure I understand you. What would be a parameter-non-free definition of an object? – Andrej Bauer Apr 4 '13 at 15:54
"A graph $G$ is discrete when the projection $G\times V \to G$ is onto" defines discreteness using $V$ as a parameter. Later, you show that there is a parameter-free definition since $V$ is definable (up to isomorphism). Am I missing the point of the last few paragraphs where you argue that $V$ is definable? – François G. Dorais Apr 4 '13 at 16:11
I do not think of $V$ as a parameter. It is a primitive type in the internal language of the topos of graphs, i.e., it is a constant. It is no more a parameter than the type $N$ of the natural numbers. It is good that we can characterise $V$ up to isomorphism wiht an internal statement, because then its interpretation is fixed. – Andrej Bauer Apr 4 '13 at 17:04

A beautiful question; thank you!

First, you can as well take Set and see if its boolean two-valued logic helps in any way to tell a finite set (definitions vary) from an infinite (definitions vary). It does not.

In Grph the subobject classifier is pretty simple, it consists of two vertices (T and F) and five arrows (two trivial ones, one from T to F, one from F to T, and one from T to F, impersonating those arrows that originate and end in a subgraph, but do not belong to it).

What can you do with it? Hardly anything. There are exactly four Grothendick topologies in this topos, and that's it.

-
I’m not sure I follow your second paragraph. The logic of Set certainly can tell the difference between a finite and an infinite set. Of course, it doesn’t do so in a novel way, since the logic of Set is just (a large fragment of) the logic we reason in all the time. But that novelty is exactly what can get more interesting when one moves to a different topos! – Peter LeFanu Lumsdaine Mar 21 '13 at 6:29