User:Lord Farin/Archive/Graph Theory Axioms

Graph Theory axiomatisation

I thought of a sort of viable system; it might seem cumbersome, but I think it provides first-order rigidity (up to a point, of course).

Let $\mathsf{Graph}$ be the following language:

• It has three relations:
  1. The unary relation $\mathsf V$, intended to mean $\mathsf V x$ iff $x$ is a vertex
  2. The unary relation $\mathsf E$, intended to mean $\mathsf E x$ iff $x$ is an edge
  3. The ternary relation $\mathsf{Edge}$, intended to mean $\mathsf{Edge}(x,y,z)$ iff $x$ is an edge with end points $y, z$ (be it in specified order or not, that can be chosen by adding axioms)

• It has no function symbols

• It is subject to the following axioms:
  1. $\forall x: \mathsf V x \lor \mathsf E x$ (everything is a vertex or an edge)
  2. $\forall x: \neg \left({\mathsf V x \land \mathsf E x}\right)$ (nothing is both a vertex and an edge)
  3. $\forall x,y,z: \mathsf{Edge} \left({x, y, z}\right) \implies \left({\mathsf E x \land \mathsf V y \land \mathsf V z}\right)$ (expressing what each component of $\mathsf{Edge}$ is)
  4. $\forall x,y,z,\tilde y, \tilde z: \mathsf{Edge} \left({x, y, z}\right) \land \mathsf{Edge} \left({x, \tilde y, \tilde z}\right) \implies \left({ \left({y = \tilde y \land z = \tilde z}\right) \lor \left({y = \tilde z \land z = \tilde y}\right) }\right)$ (an edge concerns itself with at most two vertices)
  5. $\forall x: \mathsf E x \implies \exists y,z: \mathsf{Edge} \left({x, y, z}\right)$ (there are no void edges)

In principle, this will be enough (I think). However, one can add:

• $\forall x,y,z: \mathsf{Edge} \left({x, y, z}\right) \implies \mathsf{Edge} \left({x, z, y}\right)$ (signifying an undirected graph)
• $\forall x,y,z: \mathsf{Edge} \left({x, y, z}\right) \implies \neg \mathsf{Edge} \left({x, z, y}\right)$ (a directed graph)
• $\forall x,y,z: \mathsf{Edge} \left({x, y, z}\right) \implies \neg \left({y = z}\right)$ (a loop-free graph)
• $\forall x,y,z,\tilde x: \mathsf{Edge} \left({x, y, z}\right) \land \mathsf{Edge} \left({\tilde x, y, z}\right) \implies x = \tilde x$ (a non-multigraph)

I have discovered that it is hard to formulate the notion of a path in first-order logic. This isn't strange, it's like saying that a set has cardinality $n$. An $n$-path can be achieved though.

I have put a moment's thought into dropping axiom 4. It may be interesting for investigation of, for example, non-injective maps (described by an edge with multiple starts... well, you get it).

The unary symbols $\mathsf E, \mathsf V$ combined with axiom 1,2 are effectively splitting the set that is a model into two parts, similar to the ordered pair used in the definition at the moment. What do you think? --Lord_Farin 17:59, 20 February 2012 (EST)

That seems like a reasonable axiomatization, though I'm not sure if it's really necessary. It seems at first blush like it would make a number of proofs much more annoying. I'll try to find a good book on digraphs and see how they manage it, and perhaps talk to someone. Scshunt 23:21, 20 February 2012 (EST)

What proofs exactly? One only needs to take care about what $\mathsf{Edge}$ does differently from normal, if it does any such thing. I'm just curious; you have of course every right to criticism. --Lord_Farin 02:56, 21 February 2012 (EST)