Definability in First Order Theories of Graph Orderings

Abstract

We study definability in the first order theory of graph order: that is, the set of all simple finite graphs ordered by either the minor, subgraph or induced subgraph relation. We show that natural graph families like cycles and trees are definable, as also notions like connectivity, maximum degree etc. This naturally comes with a price: bi-interpretability with arithmetic. We discuss implications for formalizing statements of graph theory in such theories of order.

Appendix

1.1 Proof of Lemma 2

Lemma 2: Let $x_n$ be an tree with at most one degree 3 node and no node of degree 4 or more. Then for any other graph $x_0$, $x_n \le _m x_0$ iff $x_n \le _s x_0$.

We prove the result by induction on the number of contraction operations in transforming $x_0$ to $x_n$.

Base Case: There are no contraction operations, there is nothing to be done.

For the induction step there are two cases we consider:

Case 1 : $\underline{x_n}$ has no degree 3 node. Let $x_n$ be a path $u_0,u_1,...,u_m$. Let $o_1,..,o_n$ be the sequence of minor operations in normal form with $x_i$ being obtained from $x_{i-1}$ via operation $o_i$. $o_n$ must be a contraction operation (else all operations are deletions and we are done). Therefore $x_{n-1}$ is either a path of length $m+1$ or a graph such that $V(x_{n-1})=V(x_n) \cup \{ u'\}$ and there exists an i with $E(x_{n-1})=E(x_n) \cup \{ u'u_i\}$ or $E(x_{n-1})=E(x_n) \cup \{ u'u_i, u'u_{i+1}\}$. In all cases, we can delete an endpoint of $x_{n-1}$ or $u'$ respectively in order to obtain $x_n$. Thus there is a sequence $o_1,..,o_{n-1},o_n'$ of operations ($o_n'$ is a deletion) to obtain $x_n$ from $x_0$. Since this sequence has a smaller number of contractions, by induction hypothesis, $x_n$ is a subgraph of $x_0$.

Case 2 : $\underline{x_n}$ has exactly one degree three node. Let $x_n$ consist of a degree 3 node u with paths $p_1,p_2,p_3$. As before, consider the sequence of minor operations. In one case $x_{n-1}$ is a graph with a degree 3 node attached to three paths exactly one of which has length one more than previously. We can delete the end point of the appropriate path to get $x_n$ from $x_{n-1}$. Another possibility is that $x_{n-1}$ is a graph with a vertex $u' \notin V(x_n)$ such that $u'$ is attached to either one or two adjacent points of one of the paths $p_1,p_2,p_3$. As before, we can delete $u'$ to get $x_n$ from $x_{n-1}$. Then by induction hypothesis $x_n$ is a subgraph of $x_{n-1}$.

1.2 Proof of Maximum Degree Definability in Theorem 4

Theorem 4: Connectivity, maximum degree and maximum path length are de-finable in minor.

In order to apply observation 2, we construct the following family:

$\mathcal {S}\cup \mathcal {N}(x)$ iff x is formed by addition of some arbitrary number of isolated vertices to a star.

$$\begin{aligned} \mathcal {S}\cup \mathcal {N}(x) :=&\mathcal {F}(x) \; \wedge \;\exists y \; hasStarComp(y,x) \; \wedge \; onlystar(x,y)\\&\text {where}\\ hasStarComp(y,x) :=&\mathcal {S}(y) \; \wedge \; y \le _m x \wedge \; \forall z \; conn(z) \; \wedge \; z \le _m x \supset z \le _m y \\ onlyStar(x,y) :=&\forall x' \;\mathcal {F}(x') \; \wedge \;|x'|_{gr}=|x|_{gr} \; \wedge \; uc_m(x',x) \supset \\&\forall y' \; (conn(y') \; \wedge \; y' \le _m x') \supset \; uc_m(|y'|_{gr},|y|_{gr}) \end{aligned}$$

onlyStarComp asserts that y is a star minor of x and in addition, every connected minor of x is also a minor of y. To fulfill this condition, x has to contain y as a connected component.

onlyStar asserts that any forest $x'$ which is formed by adding an edge to x (by observation 2) has the property that all its connected minors have order one more than the order of y.

Clearly, any graph formed by adding isolated vertices to a star has these properties.

$\mathcal {S}\cup \mathcal {N}subGraph$ states that there is a subgraph y of x which is a $\mathcal {S}\cup \mathcal {N}$ of same order as x. Note that for $S_n \cup N_m$ and $S_{n'} \cup N_{m'}$ with $n+m=n'+m'$, $S_n \cup N_m \le _m S_{n'} \cup N_{m'}$ iff $n \le n'$. Thus maximal y satisfying the formula $\mathcal {S}\cup \mathcal {N}subGraph$ contains the largest star occuring as a subgraph of x. We extract the star from this object to obtain the maximum degree of x.

1.3 Proof of Lemma 4

Lemma 4: The following predicates are definable in first order arithmetic:

• 1. nchoose2(n, x) iff $x = {n \atopwithdelims ()2}$ where ${n \atopwithdelims ()2}=n \times (n-1)/2$. $nchoose2(n,x) := 2 \times x + n = n^2$.

• 2. div(n, x, y) iff n is the quotient when x is divided by y; denoted $n=x / y$. $div(n,x,y) := \exists z \; x = y \times n + z \; \wedge \; z < y$

• 3. rem(n, x, y) iff n is the remainder when x is divided by y; denoted $n=rem(x,y)$. $rem(n,x,y) := \exists z \; x = y \times z + n \; \wedge \; n < y$

  We note that the exponentiation relation $x^y=z$ is known to be definable in arithmetic (see [13]).

• 4. pow2(i, x) iff $x =2^i$. $pow2(i,x) := \exists y \; y=2 \; \wedge \; y^i=x$

• 5. bit(i, x) iff the $i^{th}$ bit of the binary representation of x is a 1. $bit(i,x) := rem(x,2^i) =rem(x,2^{i-1})$

• 6. length(n, x) iff the length of the binary representation of x is n. We will denote this unique n by |x|.

  $length(n,x) := bit(n,x) \; \wedge \; \forall n' \; n < n' \supset \lnot bit(n',x)$

1.4 Details of Subsection 6.1

graphOrder(x, n) iff $n\ \in \mathcal {N}$ and the order of x is |n|.

$$\begin{aligned} graphOrder (x,n) := isGraph(x) \; \wedge \; 2 \times |x| = 2 +n \times (n-1) \end{aligned}$$

We will denote by $|g_x|$ the order of the graph represented by x.

edgeExists(x, i, j) iff x denotes a graph and $v_iv_j \in E(g_x)$.

$$\begin{aligned} edgeExists(x,i,j) :=&\exists n \; graphOrder(x,n) \; \wedge \\&((1 \le i < j \le n \; \wedge \; bit((2ni -2n-i^2-i+2j)/2,x) ) \\&\vee (1 \le j < i \le n \; \wedge \; bit((2nj-2n-j^2-j+2i)/2,x) ) \end{aligned}$$

By doing some counting, we can see that the tuple $\{v_i,v_j \}, i <j$ occurs at bit position $(2ni -2n -i^2 -i +2j)/2= n(n-1)/2 - (n-i)(n-i+1)/2 + j-i$.

Defining Permutations and Isomorphism. Any permutation of vertices of a vertex labelled graph induces a permutation on the edges of a graph. To identify all numbers which represent the same graph under our encoding, we will need to represent permutations on [n] and their actions.

perm(x, n) iff x represents a permutation on [n].

$$\begin{aligned} perm(x,n) :=&|x| = 1+ n \times \lfloor log(n) \rfloor \; \wedge \; \forall i \; 1 \le i \le n \; \exists ! j \; 1 \le j \le n \\&i=(rem(x,2^{j \; |n|})- rem(x,2^{(j-1) \; |n|}))/ 2^{(j-1)|n|} \end{aligned}$$

We represent a permutation by a bit string which is of length $n \times \lfloor log(n) \rfloor + 1$, note that $\lfloor log(n) \rfloor$ is the same as |n| i.e. the length of the string n. The most significant digit is to be ignored, after which every block of $\lfloor log(n) \rfloor$ bits represents a number from 1 to n. In addition, every such block must be unique (in order to guarantee that it is a permutation). The permutation sends $i \in [n]$ to the number represented by the $i^{th}$ block from the left. The formula checks that every $i \in [n]$ is obtained from a unique block $j \in [n]$.

applyperm(x, i, j, n) iff x is a permutation on [n] and sends i to j for $i,j \in [n]$.

$$\begin{aligned} applyperm(x,i,j,n) :=&perm(x,n) \; \wedge \\&(rem(x,2^{(n-i+1) |n|}) - rem(x,2^{(n-i)|n|}))/2^{(n-i)|n|} = j \end{aligned}$$

We can now define the isomorphism of graphs:

$$\begin{aligned}&sameGraph(x,y) := \exists n \; |x|=|y|=1+{n \atopwithdelims ()2} \; \wedge \; \exists z \; perm(z,n) \; \wedge \\&\forall i \; \forall j \; 1 \le i < j \le n \supset \; (edgeExists(x,i,j) \iff (\exists i' \exists j' \; applyPerm(z,i,i',n) \\&\wedge \; applyPerm(z,j,j',n) \; \wedge edgeExists(y,i',j') \; ))\\ \end{aligned}$$

The formula states that for x and y to represent the same graph, there must exist a permutation z such that for any tuple $\{ v_i,v_j \}$ of vertices of x, $v_iv_j \in E(g_x)$ iff $v_{z(i)}v_{z(j)} \in E(g_y)$.