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.
As you observe yourself, the question does not quite make sense as $\phi$ in 1. is a formula in the first order language of a category and in 2. $\phi$ is a formula in higher order logic (something like the Mitchel-Benabou language).
The only framework I can think of where this question makes perfect sense is if you interpret "internal logic" in the sense of Mike Shulman "Stack semantics" as in his paper https://arxiv.org/abs/1004.3802.
Here you interpret "the first-order language of categories" as in def. 3.1 of the paper linked above, and the stack semantics is an extention of the Kripke-Joyal semantics that is also formulated in that language (where the higher order part come from the fact that you can quantify on objects).
In this case, as pointed out by Andrej Bauer, the Kripke-Joyal semantics (or rather its extention called the stack semantics) turns a formula $\phi$ in this language to a formula $\phi'$, so that "$\phi$ hold internally in $\mathcal{E}$" if and only if $\mathcal{E}$ satisfies $\phi'$).
Of course $\phi'$ is in general different from $\phi$, though I believe $\phi'' = \phi'$.
In any case, not every formula arise as a $\phi'$ (i.e. corresponds to an "internal property"). For example, the validity of such formulas are always local properties: if $\mathcal{E}$ satisfies $\phi'$ then every slice $\mathcal{E}/X$ also satisfies $\phi'$; and conversely if $\mathcal{E}/X$ satisfies $\phi'$ for a family of objects covering the terminal, then $\mathcal{E}$ also satisfies $\phi'$.
Best Answer
Sort of. Traditional Kripke–Joyal semantics can only force the truth of predicates, not the existence of structure. So once you have multiplication, unit, and inversion maps, you could use KJ semantics to prove that the necessary diagrams commute if and only if they render each homset into a group. (At least, once you generalize KJ semantics to categories with finite products — I'm not sure I've seen it written down in more generality than categories with finite limits.)
However, Awodey, Gambino, and Hazratpour have recently generalized KJ semantics to dependent type theory (Kripke–Joyal forcing for type theory and uniform fibrations), and you might be able to use that version to deal with the algebraic structure as well.