How to express a structure of a 5-colorable graph in logic

A graph can be expressed as an structure $G = <A,R>$ satisfying the axioms $\forall xy R(x,y) \rightarrow R(y,x)$ and $\forall x \lnot R(x,x)$.

How to extend the structure and/or axioms to express a 5 colourable graph?

• What have you tried? Where did you get stuck? Hint: add a predicate for every color, and add axioms that define the properties of a legal coloring. May 13 '18 at 13:04
• I fail on the axioms part. A predicate for each color seems to be obvious. May 13 '18 at 13:06
• – D.W.
May 13 '18 at 14:46

General ideas:

• Require that each vertex ($\forall x \ldots$) satisfies at least one color predicate (Use $\lor$ among five color predicates).
• Also require that no vertex ($\lnot\exists x \ldots$) has two distinct colors (you can enumerate all the ten distinct pairs: $\lnot({\sf red}(x)\land{\sf blue}(x))\land \lnot(\ldots)\land \cdots$).
• For each color (repeat this axiom five times, once for each color), require that if $x$ has that color and $R(x,y)$ then $y$ has not that color (e.g. $\forall x y.\ {\sf red}(x)\land R(x,y) \implies \lnot{\sf red}(y)$).
• Point two: How would a general requirement look like? May 13 '18 at 13:43
• @brandstifter See the edit.
– chi
May 13 '18 at 13:50
• You actually don't need the second requirement. May 13 '18 at 15:54
• @YuvalFilmus That's true -- for formalizing color-ability we do not need to state that each vertex has exactly one color, but only that it has at least one color. For some other properties it could be useful to require it.
– chi
May 13 '18 at 16:34