Suppose G is a planar graph embedded into the plane. The graph divides the plane into regions. Let us say that two regions are adjoint if they have a common edge. Question:
(Q) Is it possible to colour the regions using four colours such that any adjoint regions have different colours? (Each region must be coloured into one of the four colours.)
This is often formulated in terms of a map and countries which was the original motivation to study this problem. I did not specify above whether the graph G is finite or infinite. In fact we will prove a theorem connecting these two:
Theorem. If the answer to (Q) is yes for all finite graphs G, then it is yes for all infinite graphs G.
In the proof we will use Compactness Theorem for propositional calculus see this post. Some times Compactness Theorem is used to deduce something about finite objects from knowing something about infinite objects. Some times the other way around. Here we have an example of the latter usage.
There are of course restrictions on what we mean by an infinite planar graph and its embeddings into the plane: by these we mean a countable graph which is embedded into the plane such that each region has finite area which is at least 1.
So let us suppose that the answer to (Q) is yes for all finite graphs and let G be an infinite (countable) graph embedded into the plane, and let us show that it is 4-colourable. Let us enumerate the regions [tex]A_0,A_1,A_2,\dots[/tex]. Let us have proposition symbols [tex]p_{n,k}[/tex] for each [tex]n\in\mathbb{N}[/tex] and [tex]k\in\{0,1,2,3\}[/tex]. n is for regions and k is for colours. Let T be the following theory.
for all [tex]n\in \mathbb{N}[/tex] there is [tex]k\in \{0,1,2,3\}[/tex] such that [tex]p_{n,k}\in T[/tex] (at least one colour for a region)
for all [tex]k\in \{0,1,2,3\}[/tex] and all [tex]i\in \{0,1,2,3\}\setminus \{k\}[/tex], [tex](p_{n,k}\rightarrow \lnot p_{n,i})\in T[/tex], (at most one colour for a region)
if [tex]A_n[/tex] and [tex]A_m[/tex] are adjoint, then for all [tex]k\in \{0,1,2,3\}, (p_{n,k}\rightarrow \lnot p_{m,k})[/tex] (adjoint regions have different colours)
Clearly if we show that T is consistent, then there is a four-colouring of G (just colour the region [tex]A_n[/tex] by the unique colour k such that [tex]p_{n,k}\in T[/tex]). By the Compactness Theorem it is sufficient to show that all finite subsets of T are consistent. But this follows from the assumption that every finite graph is four-colourable!
