Infinity graph, $k$ colours. Prove that it is possible to colour it. Firstly, I write theorem:
If infinite set of first-order predicate is contradictory, at least one of its finite subset is contrary.  
Now, I must use this theorem to prove following thing:
Lets consider infinite graph $G=(V,E)$ such that each finite subgraph of $G$  may be coloured using $k$ colours.  My task is to prove that graph $G$ may be coloured with $k$ colours.  
Can you help me, please ? I am starting at logic, and I have a problem with this thing :(
 A: There are two keys to a problem like this:


*

*Figure out what kind of structure a solution represents.

*Break your "big requirement" down into a collection of "small requirements."
These are vague, but hopefully what I mean will become clear below.

You want a $k$-coloring of $G$. There are a few ways to view a $k$-coloring of $G$ as a first-order structure, but the following is probably the most natural:


*

*Let $L$ be the language consisting of one binary relation $E$, $k$ unary relations $U_1, . . . , U_k$, and constants $c_v$ for every vertex $v\in V$.

*We then want an $L$-structure $M$ such that


*

*$c_vE^Mc_w$ iff $vEw$ in $G$,

*for each vertex $v\in M$, we have $U_i(c_v)$ for exactly one $i\in\{1, . . . , k\}$

*and if $vEw$ and $U_i(c_v)$, then $\neg U_i(c_w)$.
These are our "big requirements". We can break them into "small requirements" as follows:


*

*For $vEw$, let $\varphi_{v, w}$ be the sentence $c_vEc_w$

*For $v\not Ew$, let $\psi_{v, w}$ be the sentence $\neg c_vEc_w$.

*For each $v$, let $\chi_v$ be the sentence $(\bigvee_{1\le i\le k}U_i(c_v))\wedge \neg(\bigvee_{1\le i<j\le k}U_i(v)\wedge U_j(v))$.

*For $vEw$, let $\theta_{v, w}$ be the sentence $\bigwedge_{1\le i\le k}(U_i(v)\rightarrow \neg U_i(w))$.
The set $$\Gamma=\{\varphi_{v, w}: vEw\}\cup\{\psi_{v, w}: \neg vEw\}\cup\{\chi_v: v\in V\}\cup\{\theta_{v, w}: vEw\}$$ is a set of first-order sentences (crucially since $k$ is finite, all the disjunctions and conjunctions are finite), so now we're in business!
We now have to show two things:


*

*$\Gamma$ is finitely satisfiable (so it has a model)


and


*

*From any model of $\Gamma$, we can recover a $k$-coloring of $G$.


The first of these will follow directly from the assumption that any finite subgraph of $G$ has a $k$-coloring, and so I leave it as an exercise.
The second has kind of a subtle point: if $\mathcal{M}$ is a model of $G$, it is not true that $\mathcal{M}$ is a $k$-coloring of $G$! Why? Well, the domain of $\mathcal{M}$ might include some points which do not correspond to vertices of $G$! Indeed, while we can view $\mathcal{M}$ as a graph, it might not be irreflexive (for $m\in \mathcal{M}$ not one of the $c_v^\mathcal{M}$s, we could have $mEm$), and the colors might "overlap" (for such an $m$, we might have $U_1(m)\wedge U_2(m)\wedge . . . \wedge U_k(m)$), and even if they don't they might fail to induce a $k$-coloring on $\mathcal{M}$ (for such $m_0, m_1$ we could have $U_1(m_0)\wedge U_1(m_1)$).
We could fix the last few problems by adding more axioms to $\Gamma$; however, that still wouldn't fix the problem that $\mathcal{M}$ might have points not corresponding to vertices of $G$ (and indeed this can't be fixed by adding axioms, by the compactness theorem, if $G$ is infinite). 
Luckily, we can just ignore this completely! Suppose $\mathcal{M}\models\Gamma$. Then we just "throw away" all the extraneous information: let $$h_\mathcal{M}: G\rightarrow \{1, . . . , k\}: v\mapsto i\iff \mathcal{M}\models U_i(c_v).$$ This is indeed a $k$-coloring of $G$.
