Four-coloring infinite graphs

The four-color theorem states that every planar loopless graph can be four colored. That is, there is an assignment to each vertex of one of four distinct “colors” such that adjacent vertices are assigned distinct colors. The case of finite graphs was proved by Appel and Haken in 1976 with computer assistance (with some errors corrected in 1989), and in 2005 Werner and Gonthier formalized a proof of the theorem inside the Coq proof assistant.

A remarkable fact is that the case of infinite graphs follows from the finite case as a matter of pure logic. All you need to extend to infinite graphs is the fact that subgraphs of planar graphs are planar! This was originally proved by De Bruijn and Erdős in 1951.

In this post, we’ll go through a few ways of organizing the ideas for four coloring infinite graphs. It should be said that they are all highly non-constructive. While there might be some comparison to a limiting process, it would be at the level of colorings themselves — the limit does not descend to the level of the individual edges being colored, since the color assignments to an edge do not necessarily eventually stabilize in any way.

1. With model theory

There is a straightforward way to encode the four coloring problem using first-order logic, and then the infinite case follows immediately from the Compactness theorem. But first, we need a few definitions.

A signature consists of a collection of abstract sets called domains and a collection of abstract relations on these domains of any arity. By convention, unary relations are known as predicates. A theory for a signature is a collection of first-order sentences, where the quantifiers range over domains.[1] The theory might include sentences that imply certain relations are functions, in such a case we will write y=f(x) rather than, say, assert that f(x,y) is true. A model for a theory is an assignment of concrete sets and relations for the signature that satisfy the theory.

The Compactness Theorem states that if every finite subset of a theory has a model, then the whole theory has a model. The argument here is surprisingly straightforward, which we will sketch because it’s kind of cool. Let T be the theory, and let FT denote the set of all finite subsets of T. By assumption, each IFT has a model MI. We construct a filter on FT (that is, on the poset P(FT) of all subsets of FT) generated by elements of the form

AI:={JFT:IJ}P(FT) for all IFT. These elements satisfy the finite intersection property since AIAJ=AIJ for all I,JFT, so the resulting filter is proper. By Zorn’s lemma, the filter extends to an ultrafilter U on FT (ultrafilters are defined in the next section). For ϕT, we have Bϕ:={IFT:ϕ is true in MI}{IFT:ϕI}A{ϕ}. Since A{ϕ}U, then BϕU as well. Thus, by Łoś’s theorem[2] the ultraproduct M=(IFTMI)/U is a model for T. (By definition, ϕT is true in M iff BϕU.)

Ok, so how do we apply the compactness theorem? Let G be a loopless planar graph with vertex set V(G). Define a signature with domains V and C and a function f:VC. For each vV(G), throw in constants nvV (i.e., nullary functions nv:()V). Define a theory T by having, for each edge (v,w)E(G), the axiom f(nv)f(nw), and add in the additional axiom that C has at most four elements.[3]

Each finite subset of T corresponds to some finite subgraph of G. Since finite subgraphs are, by assumption, four-colorable, the finite subset has a corresponding model. Hence, the compactness theorem says there is a model for T itself. The domain V in this model might have no relation to V(G) (and in fact the ultraproduct construction will have constructed an absurdly large four-colored graph), but we may use the nullary functions to get a handle on things, since we may color vV(G) by the color f(nv). Since we had the axiom that C have at most four colors, we are done!

Remark. Except for the assertion that C have at most four elements, none of the axioms really involve quantifiers (there are some hidden in the function applications, but by using four mutually exclusive proposition variables per vertex these could be eliminated). It would suffice to use the compactness theorem for propositional logic rather than the full compactness theorem for first-order logic.

2. With ultrafilters

The compactness theorem is worthwhile to know, but it can be illuminating to expand things out to see how the pieces fit together. Luxemburg[4] essentially gave this argument in 1962.

Recall that an ultrafilter U on the poset PX of subsets of a set X is a subset of PX satisfying the following axioms:

  1. If A,BU, then ABU.
  2. If ABX and AU, then BU.
  3. U.
  4. If AX, then either AU or XAU.
An ultrafilter is a consistent choice of what are the “big” subsets of X. The intersection of big subsets is big, the superset of a big subset is big, the empty set is not big, and every set or its complement is big. One can check the intersection of a big set and a small set is small. In other words, there is a homomorphism from (PX,,) to the boolean lattice ({0,1},,).

A use of (ultra)filters in topology is generalized limits. An (ultra)filter U on a topological space X is said to converge to a point xX if for all open sets VX containing x then VU. The ultrafilter convergence theorem states that (1) X is compact iff every ultrafilter converges to at least one point and (2) X is Hausdorff iff every ultrafilter converges to at most one point.

Example. Given an index set J, consider the space X={0,1}J with the product topology, which is compact by Tychonoff’s compactness theorem. For every finite subset IJ, the set

VI={xX:xi=1 for all iI} is an open. Furthermore, for every pair of finite subsets I1,I2J, we have VI1VI2=VI1I2, so the collection {VI:IJ is a finite subset} satisfies the finite intersection property. Collections that do not contain the empty set and that satisfy the finite intersection property extend to an ultrafilter; let U be such an ultrafilter on PX extending this collection. Hence, by the ultrafilter convergence theorem, there is unique point xX that U converges to since the product of Hausdorff spaces is Hausdorff. This point is just the all-ones point (1)iJ.

Example. Let M be a manifold and C(M) the R-algebra of continuous functions MR. If mC(M) is a maximal ideal, then consider the collection of sets f1(0) for fm. Since mC(M), we know none of these is the empty set. And, for f,gm, one can construction a function hm with f1(0)g1(0)=h1(0) since manifolds have bump functions. Hence, the collection extends to an ultrafilter. If M is compact, then the ultrafilter has a limit point aM and thus m is principal and generated by the function xxa, and hence the quotient map C(M)C(M)/m is equivalent to the evaluation map ff(a).

Gottschalk’s argument[5] for colorings of infinite graphs uses compactness. It is somewhat overkill to use ultrafilters here, but it doesn’t hurt to use the language. Given a loopless graph G and a finite set C of colors such that every finite subgraph of G is C-colorable, let X=CV(G) be the set of all assignments of colors to vertices of G, endowed with the product topology. For each finite subset IE(G), define XIX to be the set of all points xX such that xvxw for every edge (v,w)I. These are open subsets, and the collection of all of them satisfies the finite intersection property. Since finite subgraphs of G are all C-colorable, then none of the XI’s are empty, hence there is an ultrafilter containing them. The ultrafilter convergence theorem implies there is a unique point xX that the ultrafilter converges to, and one can check it is a proper C-coloring of G. (Without ultrafilters, one may use the fact that these XI sets are closed and have the finite intersection property, hence their intersection is nonempty.)

For the rest of this section, we’ll go for a direct proof that sort of combines Gottschalk’s approach and ultraproducts and expands out the definitions.

Let G be a loopless planar graph, and let FG denote the set of all spanning subgraphs HG with finitely many edges (that is, V(H)=V(G) and E(H) is finite). By assumption, each HFG has a proper four coloring, hence there is a function fH:V(G)4 such that fH(v)fH(w) for every edge (v,w)E(H). Consider the collection of sets of the form AH={HFG:HH}. This collection satisfies the finite intersection property since AHAH=AHH for each pair H,HFG. Since each AH is nonempty, this collection extends to an ultrafilter U on P(FG). Now we use the ultrafilter to “vote” on the coloring of G itself in the following way.

For vV(G), consider the function Fv:FG4 defined by Fv(H)=fH(v), and let C(v) denote the set of colors c4 such that Fv1(c)U. That is, C(v) is the set of colors for which a “majority” of the spanning subgraphs chose that color for that vertex. A first fact is that C(v) is nonempty. If it were empty, then for each c4 we would have FGFv1(c)U, and hence the intersection of all these complements would be in U. But

i4(FGFv1(i))={HFG:fH(v)4}=, and U does not contain the empty set! A second fact is that C(v) has at most one element. For c,cC(v), then we have Fv1(c)Fv1(c)U. This intersection consists of all those graphs HFG such that fH(v)=c and fH(v)=c, hence c=c since the intersection is nonempty. Therefore, |C(v)|=1 for each vV(G). Define f:V(G)4 by letting f(v) be the sole element of C(v) for each v, which is to say f is defined by the relation Fv1(f(v))U for each vV(G).

What is left is to show that f defines a proper coloring.[6] Let (v,w)E(G) be an edge, and suppose it were the case that c=f(v)=f(w). Let HFG be the graph with E(H)={(v,w)}. Consider the intersection

AHFv1(f(v))Fw1(f(w))={HFG:(v,w)E(H) and fH(v)=fH(w)}. Since each fH is a proper coloring, this set is empty. But, this is an intersection of three elements of U, so it would be an element of U as well! Therefore f must be a proper coloring, and we are done.

Remark. Define F:FG4V(G) by f(H)=fH. Maps of sets carry ultrafilters to ultrafilters, which in particular means that FU={A4V(G):F1(A)U} is an ultrafilter on 4V(G). Since 4V(G) is compact Hausdorff, there is a unique U-limit of F (that is, a limit point of FU), and it was the f we constructed from before. With PG denoting the set of all spanning subgraphs of G, then we may endow it with the product topology using the correspondence that a spanning subgraph is a function E(G)2. The subspace FGPG is dense, and U converges to GPG, which is outside FG. Extending U to be an ultrafilter on PG, it is a principal ultrafilter generated by G, and the limit of a function with respect to a principal ultrafilter is the image of the generator.

3. By Kőnig’s lemma

One version of Kőnig’s lemma is that, given an infinite sequence S1,S2,S3, of disjoint non-empty finite sets along with a relation < on iSi such that for every xSn+1 there is a ySn with y<x, then there exists an infinite sequence x1,x2,x3, such that xnSn for each n with x1<x2<x3<.

For example, given functions fn:Sn+1Sn for each n, we could define y<x iff y=fn(x) for ySn and xSn+1. We may interpret Kőnig’s lemma as saying the inverse limit limnSn is nonempty. Note that this is true even without each fn being surjective.

Nash-Williams[7] points out how Kőnig’s lemma implies a version of infinite graph coloring in the case of a loopless planar graph G with a countably infinite vertex set.

Since there are countably many vertices, we may define n-element subsets VnV(G) with VnVn+1 for each n1 such that V(G)=nVn. Let Gn=G[Vn] be the subgraph of G that is induced by the vertex set Vn; recall this means Gn has all the edges of G that are incident only to vertices from Vn. Let Sn consist of all vertex colorings Vn4 that are proper colorings for Gn. Since Gn is a planar finite graph, Sn is nonempty.

There is a function fn:Sn+1Sn defined by restricting the vertex coloring from Gn+1 to Gn. Hence, by Kőnig’s lemma there is a sequence x1,x2,x3, with xnSn for each n and fn(xn+1)=xn. For any given vertex vG, there is an n with vVn. We may color v according to xn. We color all of G in this way.

This must be a proper coloring because every pair of adjacent vertices is contained in some Vn for a large enough n, and Vn contains the edge between them.

The fact the inverse limit is non-empty in no way gives an effective algorithm. While each extension of the graph might be four-colorable, you might not be able to extend the four coloring itself, and it might change dramatically. All Kőnig’s lemma promises is that, with infinite foresight, you could make the right coloring decisions!

[1] This has been mildly generalized from the usual definition where there are no domains. You can represent distinct domains in the usual formulation by having mutually exclusive predicates that test domain membership.
[2] Pronounced “Wash’s theorem.”
[3] For example, “for all a,b,c,d,eC, then a=b or a=c or ... or d=e.”
[4] Luxemburg, W. A. J. (1962), “A remark on a paper by N. G. de Bruijn and P. Erdős”, Indagationes Mathematicae, 24: 343–345, doi:10.1016/S1385-7258(62)50033-4, MR 0140435.
[5] Gottschalk, W. H. (1951), “Choice functions and Tychonoff’s theorem”, Proceedings of the American Mathematical Society, 2 (1): 172, doi:10.2307/2032641, JSTOR 2032641, MR 0040376.
[6] Thanks to Scott Kovach for debugging this part of the argument.
[7] Nash-Williams, C. St. J. A. (1967), “Infinite graphs—a survey”, Journal of Combinatorial Theory, 3 (3): 286–301, doi:10.1016/s0021-9800(67)80077-2, MR 0214501.