Abstract Structure and Types

If $G=(V,E)$ is a graph, with vertex set $V$ and edge relation $E$, the suggestion is that its abstract structure is the the propositional function expressed by its diagram formula ${\mathrm{\Phi }}_G(X_0,X_1)$. For example, consider the two vertex directed graph:

$G=(\{0,1\},\{(0,1)\})$.

Then, the abstract structure of $G$ is the propositional function ${\hat{\mathrm{\Phi }}}_G$ expressed by the formula ${\mathrm{\Phi }}_G(X_0,X_1)$:

$\mathrm{\exists }{v}_0\mathrm{\exists }{v}_1(X_0(v_0)\wedge X_0(v_1)\wedge \mathrm{\neg }{X}_1(v_0,v_0)\wedge X_1(v_0,v_1)$ $\wedge \mathrm{\neg }{X}_1(v_1,v_0)\wedge \mathrm{\neg }{X}_1(v_1,v_1)\wedge \mathrm{\forall }z(X_0(z)\to (z=v_0\vee z=v_1)))$  

The categoricity of the diagram formula ${\mathrm{\Phi }}_G(X_0,X_1)$ ensures that it defines the isomorphism type of $G$. That is, for any graph $G^{\prime }$, we have:

$G^{\prime }\models {\mathrm{\Phi }}_G(X_0,X_1)$ iff $G\cong G^{\prime }$.

For example:

$G^{\prime }=(\{3,4\},\{(3,4)\})$.

This is isomorphic to $G$. That is,

$G\cong G^{\prime }$. 

So, $G^{\prime }\models {\mathrm{\Phi }}_G(X_0,X_1)$.

In particular, we obtain the same propositional function in both cases:

${\hat{\mathrm{\Phi }}}_G={\hat{\mathrm{\Phi }}}_{G^{\prime }}$

So, $G$ and $G^{\prime }$ have identical abstract structure.

For a mathematical object $\mathcal{A}$ (such as a group, a field, a topological space, a manifold, etc., understood as a model), the diagram formula---or, more exactly, the propositional function ${\hat{\mathrm{\Phi }}}_{\mathcal{A}}$ expressed by the diagram formula---encodes all the structural information concerning $\mathcal{A}$.

Returning to the diagram formula, ${\mathrm{\Phi }}_G(X_0,X_1)$, a special role is played by the variable $X_0$ which "picks out" the domain. Its role is more or less the same as that played by the variable $A$ in "type declarations" such as

$a:A$

in structural set theory and type theories. We could rewrite the diagram formula more type-theoretically like this:

$(\mathrm{\exists }{v}_0:X_0)(\mathrm{\exists }{v}_1:X_0)(\mathrm{\forall }z:X_0)(\mathrm{\neg }{X}_1(v_0,v_0)\wedge X_1(v_0,v_1)$ $\wedge \mathrm{\neg }{X}_1(v_1,v_0)\wedge \mathrm{\neg }{X}_1(v_1,v_1)\wedge (z=v_0\vee z=v_1))$ 

For this analysis, however, the type involved is always a type of set: i.e., the carrier set of the mathematical model.