In [1]:

```
using Catlab.Graphs, Catlab.Graphics
using Catlab.Theories, Catlab.CategoricalAlgebra
```

A *subgraph* of a graph $G$ is a monomorphism $A \rightarrowtail G$. Because
the category of graphs is a presheaf topos, its subobjects have a rich
algebraic structure, which we will explore in this vignette.

Throughout the vignette, we will work with subgraphs of the following graph.

In [2]:

```
G = cycle_graph(Graph, 4) ⊕ path_graph(Graph, 2) ⊕ cycle_graph(Graph, 1)
add_edge!(G, 3, add_vertex!(G))
to_graphviz(G, node_labels=true, edge_labels=true)
```

Out[2]:

In [3]:

```
(A = Subobject(G, V=1:4, E=[1,2,4])) |> to_graphviz
```

Out[3]:

In [4]:

```
(B = Subobject(G, V=[2,3,4,7,8], E=[2,3,6,7])) |> to_graphviz
```

Out[4]:

The *join* is defined as left adjoint to the diagonal, making it the *least
upper bound*:

In [5]:

```
A ∨ B |> to_graphviz
```

Out[5]:

Dually, the *meet* is defined as right adjoint to the diagonal, making it the
*greatest lower bound*:

In [6]:

```
A ∧ B |> to_graphviz
```

Out[6]:

The other operations, beginning with implication ($\Rightarrow$) and negation ($\neg$) are more interesting because they do not have pointwise formulas.

*Implication* is defined as the right adjoint to the meet:

In [7]:

```
(A ⟹ B) |> to_graphviz
```

Out[7]:

*Negation* is defined by setting $B = \bot$ in the above formula:

In [8]:

```
¬A |> to_graphviz
```

Out[8]:

The logic of subgraphs, and of subobjects in presheaf toposes generally, is not classical. Specifically, subobjects form a Heyting algebra but not a Boolean algebra. This means that the law of excluded middle does not hold: in general, $\neg \neg A \neq A$.

Applying the double negation to a discrete subgraph gives the subgraph induced by those vertices.

In [9]:

```
(C = Subobject(G, V=1:4)) |> to_graphviz
```

Out[9]:

In [10]:

```
¬(¬C) |> to_graphviz
```

Out[10]:

The subojects also form co-Heyting algebra and hence a bi-Heyting algebra.

*Subtraction* is defined dually to implication as the left adjoint to the
join:

In [11]:

```
(A \ B) |> to_graphviz
```

Out[11]:

*Non* is defined by setting $A = \top$ in the above formula:

In [12]:

```
~A |> to_graphviz
```

Out[12]:

In [13]:

```
(A ∧ ~A) |> to_graphviz
```

Out[13]: