How Wang's conjecture implies decidability of The Domino Problem?

Question

Wang stated following conjecture about Wang tiles (which was proven false by R. Berger):

A finite set of plates [Wang's tiles] is solvable if and only if it has at least one periodic solution.

Also Wang said that if this conjecture holds, then there is an algorithm which decides whether finite set of Wang tiles is solvable. Here is a citation from Wang's publication (1961):

Thus, we proceed to build all possible rectangles from copies of the plates of different sizes, using smaller ones first. If 4.1.2 [the Wang's conjecture] is true, the process will always terminate in one of two ways: either at some stage we arrive at a cyclic rectangle and, therefore, the original set is solvable; or else we arrive at a size such that there is no rectangle of that size in which adjoining edges always have the same colors. The latter alternative is in fact a necessary and sufficient condition under which the original set is not solvable.

I don't understand how this statement is true. We can try enumerate all possible rectangle with increasing area. If set is solvable, then we will eventually find suitable ("cyclic") rectangle. However, if set is not solvable, how do we know when to stop? How we differentiate between case that rectangle does not exist and case that such rectangle has not been found yet?

Of course, I am missing something important... A lot of papers are referencing this fact, so it cannot be false.

Answer 1

This is essentially the following combinatorial fact:

Konig's lemma: if $T$ is a finitely-branching tree, then either $T$ has an infinite path or $T$ is finite (and so we see all nodes "die out at some level").

(To see that the finite-branching-ness is necessary, consider the tree consisting of all finite sequences of natural numbers whose length is at most the first term in the sequence: it has no infinite path, but it is infinite, and it gets away with this by branching more times than we'd like.)

Proof: Supposing $T$ is infinite, we build a path through $T$ inductively by, at each stage, moving to a node ahead of our current node above which $T$ remains infinite. We can do this because $T$ is only finitely branching: if $T$ is infinite above some node, it must be infinite above at least one of that node's children as well. $\quad\Box$

As a corollary, we get:

$(*)$ A set of tiles is unsatisfiable iff for some $n$ there is no way to tile a square of size $n$.

From this corollary, it's clear that unsatisfiability is detectable. Wang's conjecture would imply that satisfiability is detectable, and that would give full decidability.

---

How do we get from Konig's lemma to $(*)$ above?

Well, we'll use a tree of possibilities idea. A node on our tree $T$ is a legal square of size $2n$, and one node $\sigma$ is the parent of another node $\tau$ if $\sigma$ is "$\tau$ minus its boundary." An infinite path through $T$ clearly describes a way to tile the whole plane; conversely, since there are only finitely many Wang tiles, every node on $T$ has at most finitely many children.