So you got an infinite planar graph $G$. I will prove that it is four colorable.
So, construct an infinite number of statements about graphs:
- The first is "is four colorable"
- Next, for each vertex $v$ the statement "contains $v$"
- Next, for each edge $e$, the statement "contains $e$"
Every finite set of these statements is satisfiable. A finite set of those statements is satisfied by a finite subgraph of $G$ (which will be planar).
Therefore, we can use the saturation principle to say there is a hypergraph $H$ that satisfies all of the above statements (a hypergraph is to a graph what a hyperreal number is to a real number). Color $H$ using four colors.
Now, for each vertex $v$ in $G$, we color it with the color used for $v$ in $H$. Now for every $v_1$ and $v_2$ in $G$, $v_1$ and $v_2$ will be adjacent and different colors in $H$. Therefore, the coloring is valid for $G$.
Here is the problem I have. We know by the transfer principle that all $v_1$ and $v_2$ that are adjacent in $G$ are adjacent in $H$. The problem is, we need to use an infinite number of such statements. This would seem to imply that the proof would need to be infinitely long, sense it refers to an infinite number of individual statements.
For example, for an infinite hyperreal $H$, we know that $H > 1$, $H > 1 + 1$, $H > 1 + 1 + 1$, and so on, but we can't conclude that is bigger than every number, since that would be contradiction.
Can you use the transfer principle an infinite number of times but still have a finite proof?
Note: A hypergraph is a graph in a nonstandard model.