Tiling $\mathbb{R}^2$ with polyomino

Divide $\mathbb{R}^2$ into disjoint unit squares, let Q be a tile (a polyomino, a finite set of connected unit squares). If, for every finite set S of unit squares in $\mathbb{R}^2$, - I can find a finite set of disjoint Q-tiles (a tiling) such that S is a subset of this tiling, how to prove that I can tile entire $\mathbb{R}^2$ with Q-tiles, (without axiom of choice)?

-
I guess you would need a little more information. Can you find a tiling of $S$, that you can extend to a tiling of an arbitary $S'$ with $S \subset S'$? – Alexander Thumm May 12 '11 at 19:22
I think the (general-topology) tag is wrong? – GEdgar Jun 14 '11 at 12:31

I know three different proofs of this.

• First, you can appeal to König's lemma. View the set of tilings of increasingly large squares based at the origin (that is, they minimally cover such a square) as a tree under the subtiling relation. This is a finitely branching tree, since any tiling of a square has only finitely many extensions to cover the next larger square. But your assumption says that this tree is infinite. Thus, it has an infinite branch, by König's lemma. Such a branch gives a tiling of the entire plane.

• Second, you can view the previous argument as a compactness argument, if you consider the right topology.

• Third, one can argue from nonstandard analysis. Take a nonstandard model of the natural numbers. By the transfer principle, there must be a tiling of some nonstandard size square using tiles from your tile set. But a nonstandard (pseudo)finite square includes many actual copies of the standard plane inside it, around the nonstandard numbers in the very center of the nonstandard square. Thus, there is a tiling of the actual standard plane.

-
Here is a fourth proof: Use the compactness theorem of first order logic. Consider a language that allows you to express of each small square what part of the Q tile it is, and write down the natural axioms that state that these assignments are coherent, in the sense that each small square occupies only one part of Q, and that adjacent parts match, and so on. This theory is finitely consistent, since we may tile any finite region, and therefore by compactness, it is consistent. So there is a model of the theory, and this provides a tiling. – JDH May 12 '11 at 19:25

Consider a sequence $S_1, S_2, S_3, \ldots$ of finite regions that exhaust the plane, namely $\cup S_i = \mathbb{R}^2$. For instance, you may take $S_i$ to be the square of edge side $2i+1$ centered at the origin.

Each $S_i$ is coverable with copies of your tile $Q$. Define a tree as follows: The vertices at level $i$ are all the possible coverings of $S_i$, and a vertex at level $i$ is a connected with a vertex at level $i+1$ iff the latter is an extension of the former - namely, a covering of $S_{i+1}$ that contains the covering of $S_i$ and possibly adds a finite number of additional tiles. (to give our tree a root we can just add a vertex, representing "S_0", connected to all the ways to position a single tile $Q$ over $S_1$).

It should be easy to prove that this is indeed an infinite tree. By Kőnig's lemma it contains an infinite branch which defines a tiling of the while plane. Kőnig's lemma is equivalent to a weak form of AC, probably countable-AC or something similar; I don't think you can avoid some form of choice or dependent choice for your proof.

-
Alon, it looks like we had the same idea at the same time! Incidently, you don't need any AC to prove Konig's lemma for trees built on a well-ordered set, and that suffices here, since we can easily order the set of finite tilings by encoding them with integers. – JDH May 12 '11 at 19:55
@JDH, I'm honored :-) and good point re AC. – Alon Amit May 12 '11 at 23:56