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 $\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{\Phi}_G$ expressed by the formula $\Phi_G(X_0,X_1)$:

$\exists v_0 \exists v_1 (X_0(v_0) \wedge X_0(v_1) \wedge \neg X_1(v_0,v_0) \wedge X_1(v_0,v_1)$ $ \wedge \neg X_1(v_1,v_0) \wedge \neg X_1(v_1,v_1) \wedge \forall z(X_0(z) \to (z = v_0 \vee z = v_1)))$  

The categoricity of the diagram formula $\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 \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 \Phi_{G}(X_0,X_1)$.

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

$\hat{\Phi}_{G} = \hat{\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{\Phi}_{\mathcal{A}}$ expressed by the diagram formula---encodes all the structural information concerning $\mathcal{A}$.

Returning to the diagram formula, $\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:

$(\exists v_0: X_0)(\exists v_1: X_0)(\forall z: X_0) (\neg X_1(v_0,v_0) \wedge X_1(v_0,v_1)$ $ \wedge \neg X_1(v_1,v_0) \wedge \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.