# How can I formally prove that undirected graphs cannot be axiomatised in First Order Logic with only unary predicates?

All the models of the following FOL formula are simple undirected graphs and all the simple undirected graphs are a model of this formula [source]:

$$\forall x. \neg R(x,x)$$ $$\forall x \forall y. R(x,y) \rightarrow R(y,x)$$ Now, can I express this formula somehow with unary predicates alone in a function free FOL language ? If not then how can I prove that it's not possible ?

• The basic feature of graphs is the edge connecting two vertex: how to express the fact that there is (there is not) and edge connecting $x$ and $y$ if we have no binary relation symbols? Jul 14 at 12:23
• @MauroALLEGRANZA Intuitively I think it is not possible, but I am not sure how to go about a proof like that ? Jul 14 at 13:43

The first step is to even state the claim precisely! The key notion is that of an interpretation. Their full generality is a bit technical, so I'll just treat the relevant special case here.

Suppose $$G=(V;R)$$ is a graph (= set equipped with a binary relation). Are there necessarily sets $$X_1,...,X_n\subseteq V$$ such that $$R$$ is definable in the "purely unary" structure $$(V; X_1,...,X_n)$$?

This turns out to have a very strong negative answer. First I'll prove it for the usual (first-order) notion of definability, and then I'll briefly talk about its much broader applicability.

## Main question

The key is to think about automorphisms, and specifically orbits. Recall that an orbit in a structure $$\mathcal{M}$$ is a set of the form $$Orb_\mathcal{M}(m):=\{\alpha(m): \alpha\in Aut(\mathcal{M})\}$$ for some element $$m$$. We want to count the orbits in the various relevant types of structure:

1. There is a graph $$G$$ with infinitely many distinct orbits.

2. On the other hand, in any structure whatsoever whose signature consists only of finitely many unary relations, there are only finitely many orbits (namely $$2^k$$ where $$k$$ is the number of unary relations).

Proving each of (1) and (2) is a good exercise. For (1), think about the successor graph on $$\mathbb{N}$$ (the vertex set is $$\mathbb{N}$$ and the edge relation is $$aRb\iff a+1=b$$); this graph has no (nontrivial) automorphisms whatsoever, so all the orbits are singletons. For $$(2)$$, draw a Venn diagram and show that permutations which "respect the bubbles" are automorphisms.

The point, then, is this. Suppose $$G=(V;R)$$ is a graph with infinitely many orbits and $$X_1,...,X_n\subseteq V$$. By the pigeonhole principle, there are vertices $$g,h\in V$$ such that $$g$$ and $$h$$ are in the same $$(V;X_1,...,X_n)$$-orbit but not in the same $$(V;R)$$-orbit. This means that there is some automorphism of $$(V;X_1,...,X_n)$$ which is not an automorphism of $$(V;R)$$. But this can't happen if $$R$$ is definable in $$(V;X_1,...,X_n)$$:

1. If $$S$$ is a definable relation in a structure $$\mathcal{M}=(M;[\mathit{stuff}])$$, then every automorphism of $$\mathcal{M}$$ is also an automorphism of the expansion $$\mathcal{N}:=(M;[\mathit{stuff}], S)$$.

(A relevant term here is "expansion by definitions.") We can prove (3) by induction on formula complexity, as is often the case, and this finishes the proof.

## Coda

Actually (3) is a much broader principle: it's essentially part of any reasonable definition of "logic" in general (and so e.g. holds true of second-order logic, infinitary logics, etc. as well). Meanwhile, (1) and (2) are purely "structural" - they don't mention logic or definability at all. Consequently, the question here actually has a very strong negative answer:

There is no reasonable logic in which we can "code" graphs by unary predicates.

In my opinion this is the "right" theorem - it's not good to focus on FOL to the exclusion of all other logics, and so when a theorem about FOL generalizes essentially without effort to a much broader class of logics it's important to at least state that generalization explicitly.

• +1 : Thanks for the answer. It will take me some time to digest everything :D Jul 14 at 14:48
• @SagarM Happy to help! BTW please do not accept this until you understand it (or at least not until some time has passed); accepting an answer early on may dissuade others from adding their own answers, and this is a good question which deserves multiple perspectives. Jul 14 at 14:50

So far, we have an answer that generalizes to a large class of logics, and a more specific answer that treats first-order logic. Let me give an even more specific answer: one that focuses on the finite case.

Assume that there was a predicate formula $$\varphi$$ (given in terms of unary predicates and perhaps equality) whose models are simple undirected graphs, and that all the simple undirected graphs are a model of this formula $$\varphi$$. So the $$n$$-element models of $$\varphi$$ should be precisely the simple undirected graphs with $$n$$ vertices.

Since the formula $$\varphi$$ contains only finitely many (say $$k$$) unary predicates, and each unary predicate determines a single subset of these $$n$$ vertices, we would get that there are at most $$2^{kn}$$ different graph structures on $$n$$ vertices. However, it can be shown (see Flajolet and Sedgewick: Analytic Combinatorics, p. 105, available on the author's website) that as $$n$$ goes to infinity, the number of simple graphs (up to isomorphism) grows faster than $$2^{n\left(\frac{n-1}{2} - \log n\right)}$$. Needless to say, this rapidly outgrows any function of the form $$2^{kn}$$ for fixed $$k$$.

• +1: a very nice approach. Jul 15 at 17:47

As Noah has invited alternative answers, here is mine: a first-order logic whose only non-logical symbols are unary predicate symbols is decidable. E.g., see Prove the theory of equality with a finite number of unary predicates is decidable. (Note that as any formula contains only finitely many symbols, the restriction to a finite number of possible unary predicates is not important.) However, the theory of equality together with a single binary relation is undecidable. This shows that there is no finite axiomatisation of the theory of undirected graphs using only unary predicate symbols.

• +1. Note to the OP that this is orthogonal to my answer: it's somewhat specific to first-order logic, but also gives a much stronger result than mere non-interpretability. Jul 15 at 1:45
• Does the fact that theory of binary predicate + equality is undecidable imply that the theory of (finite) undirected graph is undecidable? Jul 16 at 12:40
• @sundowner: one proof goes via an encoding of the atomic predicates of a first-order language as finite graphs. So I think the answer to your question is yes. Jul 16 at 14:07