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

Question

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 ?

Answer 1

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)$:

3. 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.

Answer 2

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.

Answer 3

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$.