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...". 


*

*Can I express that a graph $X$ is finite, (respectively complete, discrete)? 

*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$?  

*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?

*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$.)

*Can I prove that if a graph has no loops and finitely many vertices then it has finitely many paths?

*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}$: __."
 A: 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$".


We can already answer some of your questions:


*

*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.
A: 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.
