Hanf and Myers showed in 1974 that there exists a single set of tiles that will tile the plane only in a non-computable way. How are we to interpret this? Does it imply that there is a particular Turing Machine which halting is undecidable in whatever formal system?
I know that non-computability is a feature of a family of problems, not a single problem. So I am not sure if I understood this correctly.
Edit: This is the link to the article by Hanf (1974) where he proves that there exists a single set of tiles tiling the plane in a non-recursive way: https://www.jstor.org/stable/2272640 (the article is only 2 pages long)
Is this an example of a single problem to which no algorithm can decide? Any insights would be helpful.
There is a crucial type difference here: we have to distinguish between problems with a single-bit (or natural number) answer, and problems with a more complicated (= "morally equivalent" to a real number or set of integers) answer. In fact, we should also allow problems with multiple solutions - so-called "mass problems."
Given a tileset $T$, there are two natural questions we can ask about it:
"Does $T$ tile?" This question has exactly one correct answer, and that answer is a single bit.
"How can $T$ tile?" (assuming that $T$ can in fact tile the plane). This question may have many correct answers (= valid tiling methods), but each individual answer is a highly structured object: at first glance, it may take infinitely many bits of information to fully describe a tiling of the plane.
The Hanf/Meyers result addresses the second type of question. Meanwhile, questions of the first sort can never be undecidable in all formal systems, because we can always add the correct solution as a single axiom to our favorite formal system (whereas the whole point of Hanf/Meyers is that no correct solution is simple enough to be so added).