The Undecidability of the Domino Problem

One of the most fundamental problems in tiling theory is to decide, given a surface, a set of tiles and a tiling rule, whether there exists a way to tile the surface using the set of tiles and following the rules. As proven by Berger (The Undecidability of the Domino Problem. Ph.D. thesis, Harvard University, 1964) in the 1960s, this problem is undecidable in general. When formulated in terms of tilings of the discrete plane ℤ² by unit tiles with colored constraints, this is called the Domino Problem and was introduced by Wang (Bell Syst Tech J 40:1–41, 1961) in an effort to solve satisfaction problems for ∀∃∀ formulas by translating the problem into a geometric problem. There exist a few different proofs of this result. The most well-known proof is probably the proof by Robinson (Invent Math 12(3):177–209, 1971) which is a variation on the proof of Berger. A relatively new proof by Kari (Machines, computations, and universality (MCU). vol. 4664, 2007, pp. 72–79) has some nice ramifications for tilings of surfaces and groups. In terms of ingredients, one can divide the proofs in 4 categories. The remaining two categories are given by the proof of Aanderaa and Lewis (J Symb Log 39(3):519–548, 1974) and the fixed point method of Durand et al. (J Comput Syst Sci 78(3):731–764, 2012). In this course, we will give a brief description of the problem and to the meaning of the word “undecidable”, and then give the four different proofs. As we will explain, the undecidability of the Domino Problem has as a consequence the existence of an aperiodic tileset. All four sections will be organized in such a way that the interested reader can first extract from the proof the aperiodic tileset into consideration, before we go into more details to actually prove the undecidability of the problem.