Heyting algebras originating from directed graphs

These can be described in a manner similar to my answer to this related MO question about simplicial sets. This case is simpler and to understand the subobject classifier in the topos of reflexive graphs, it suffices to look at the lattice of abstract simplicial complexes on $\{0,1\}$ (including the empty one):

• $1 = \{\{0,1\},\{0\},\{1\}\}$
• $s \vee t = \{\{0\},\{1\}\}$
• $s = \{\{0\}\}$
• $t = \{\{1\}\}$
• $0 = \varnothing$

Let's write $\Omega_1$ for this Heyting algebra.

In down to earth terms, this lattice represents all five possibilities of what could happen to a non-loop edge $e$ of $X$ in a reflexive subgraph $X'$:

• $e$ is an edge in $X'$
• $e$ is not an edge in $X'$ but both its source and target vertices remain in $X'$
• $e$ is not an edge in $X'$ and only its source vertex remains in $X'$
• $e$ is not an edge in $X'$ and only its target vertex remains in $X'$
• $e$ is not an edge in $X'$ and its source and target vertices are not in $X'$

We now see that $\operatorname{Sub}(X)$ is naturally a subalgebra of a power of $\Omega_1$, specifically the subalgebra of all $p \in \operatorname{Edges}(X)\to\Omega_1$ which are coherent (e.g. if $e$ is a loop then $p(e) = 0$ or $p(e) = 1$ and if two edges $e,e'$ share a vertex then $p(e)$ and $p(e')$ shouldn't disagree on the fate of that shared vertex).

The logic $L(K_1)$ is precisely that of $\Omega_1$. I'm not sure what to make of your other questions about $K_1$. The main issue is that the Heyting algebras $\operatorname{Sub}(X)$ are always complete, so it's not clear that free objects should exist in $K_1$ unless I'm missing something.

Your category of graphs is dually equivalent to an equationally defined category of algebras. The algebras don't form a variety in the technical sense that François intends, since infinitary operations are required, although there is a variety whose category of finite algebras is dually equivalent to the category of finite graphs. If we remain open about what the algebras are, that is, don't require that they appear as $Sub(G),$ then there is a simple answer to what they can be. The category of sets is dually equivalent to the category of complete atomic Boolean algebras, which are equationally definable using equations for joins and meets, and equations for complete distributivity. The action of the two element monoid, whose Karoubi envelope is $\Delta_1$, used to describe the graph category can be transferred to the Boolean algebras as an extra unary operation.

But there's another answer that is closer to your question. What if the subobject classifier Omega is used directly to induce a duality, and we try to describe the Heyting algebras that arise from the poset of subgraphs of the graphs ? If we use the axioms for Heyting algebras plus the two equations (mentioned already in my second post) $p \vee (p \Rightarrow (q \vee \neg q))=1$ and $\neg (p \wedge q \wedge r) = \neg (p \wedge q)\vee (q \wedge r)\vee (r \wedge p) $ as well as infinitary join and meet rule, will we be able to recover, up to an isomorphism, a single graph ? Well no, because the opposite of a graph, obtained by reversing the direction of arrows, will have a subgraph lattice that is isomorphic to the subgraph lattice of the original graph, and of course a directed graph is not generally isomorphic to its opposite. There is something that can be done to correct the situation however. If we add a single unary "orientation" operation $ \tau $ satisfying $\tau p \vee \tau \neg p =1$ and $\tau p \wedge \tau \neg p = p \vee \neg p,$ then these "graphic" algebras, with the two extra Heyting algebra rules and the infinitary operations and equations, form a category dually equivalent to the category of graphs.The unary operation $\tau,$ has two possible interpretations on the algebra of subgraphs of all graphs. One interpretation assigns to a subgraph $H$ of each graph $G$ the subgraph $\tau H$ of $G$ that has the same vertices as $G$ and whose arrows are all arrows that start in $H$ and end outside $H.$ For the other interpretation the arrows start outside and end inside the subgraph. For the first, $\tau$ on $\Omega$ is the morphism that classifies the subgraph of $\Omega$ generated by the arrow that starts at 1 and ends at 0. For the second, the arrow starts at 0 and ends at 1.

If you are interested in more details, here's a url where I posted a similar duality (it was published in Jan 2005 in "Mathematical Reports of the Academy of Sciences of the Royal Society of Canada".)

https://www.researchgate.net/publication/266304536_A_duality_for_the_category_of_directed_multigraphs

Lawvere calls the graphs you are looking at reflexive and the graphs in my article irreflexive. The generator, in the sense of category theory, of the category of reflexive graphic algebras, is the free reflexive graphic algebra on one generator, $x$; it has 12 elements $(0,x,\neg x, \neg \neg x, x \vee \neg x, \neg x \vee \neg \neg x, \neg \neg x \Rightarrow x, \tau x, \tau \neg x, \tau x \vee \neg \neg x, \tau \neg x \wedge (\neg \neg x \Rightarrow x),1)$, whereas for the irreflexive algebra its more complicated, there are 39 elements (all 39 polynomials are identified at the url). The irreflexive graphs have an interesting graph that is internally isomorphic to but not isomorphic to the subgraph classifier, which is not the case for reflexive graphs ( this is related to my first post (version: 2011-03-02): https://mathoverflow.net/q/57032).

I don't have an answer to question 5, but the other four questions have answers that follow from the duality. My article has the references I used, but in addition there is an earlier papers by Marta Bunge that shows that in principle there should be such a duality for Grothendiek toposes( sorry I don't have the exact reference). I was strongly influenced by a paper of Andrew Pitts : On an Interpretation of Second Order Quantification in First Order Intuitionistic Propositional Logic, Jour. Symbolic Logic 57(1992) 33-52. In fact I started writing the duality paper shortly after reading his paper. I have seen essentially this duality in a suprisingly different context: a paper by Katarzyna Idziak , Undecidability of Brouwerian Semilattices, Algebra Universalis 1986, that establishes the undecidability of the first order theory of algebras that are similar to the Heyting algebras that satisfy the two extra equations I gave above. The author constructs undirected graphs out of this type of algebra (in the same way that I construct directed graphs out of graphic algebras) and uses the fact that the first order theory of the undirected graphs is undecidable. There is no category theory in the paper.