Four Color Theorem for Finite Maps implies Four Color Theorem for Infinite Maps

From ProofWiki
Jump to navigation Jump to search

Theorem

Suppose that any finite planar graph can be assigned a proper vertex $k$-coloring such that $k \le 4$.


Then the same is true of any infinite planar graph.


Proof

Let $G$ be an infinite planar graph.

Let $C$ be a set of vertices of $G$.

For each $c \in C$ let $p_c^1, p_c^2, p_c^3, p_c^4$ be propositional symbols, where

$p_c^i$ is true if and only if the color of vertex $c$ is $i$.

Let $\PP_0$ be the vocabulary defined as:

$\PP_0 = \set {p_c^1, p_c^2, p_c^3, p_c^4: c \in C}$

Let $\mathbf H$ be the set of all statements with the following forms:

$(1): \quad$ $p_c^1 \lor p_c^2 \lor p_c^3 \lor p_c^4$ for each $c \in C$
$(2): \quad$ $p_c^i \implies \neg p_c^j$ for each $c \in C$ and for each $i \ne j$
$(3): \quad$ $\neg \paren {p_c^i \land \neg p_{c'}^i}$ for each $i$ where $c$ and $c'$ are adjacent.

Let $\MM$ be a model for $\mathbf H$ which corresponds to a proper vertex $4$-coloring of $G$.

By hypothesis, any finite planar graph can be assigned a proper vertex $4$-coloring.

Thus every finite subgraph of $G$ has a proper vertex $4$-coloring.

That is, every finite subset of $\mathbf H$ has a model.

By the Compactness Theorem for Boolean Interpretations, $\mathbf H$ has a model.

Hence the entirety of $G$ can be assigned a proper vertex $k$-coloring.

$\blacksquare$


Sources