If a finite set of tiles can tile a quadrant of the plane, it can also tile the full plane.
One would guess that there is a constructive proof, but in fact the proof relies on a weak version of the axiom of choice (see for example this proof https://caicedoteaching.wordpress.com/2009/08/24/502-konigs-... ).
1/ Complete part of the tiling in the upper right quadrant (this tiling exists by assumption)
2/ Shove all the tiles down and to the left
3/ Repeat.
It's very surprising that step 2 needs the axiom of choice. (Usually when I'm this surprised it means I've misunderstood something!)
Edit: your link proves something stronger - that the ability to tile an nxn square for all n is equivalent to tiling a quadrant and tiling a plane. I guess that's where choice comes in, is it?
> our link proves something stronger
No, it proves that the 3 statements are equivalent, so it is not stronger.
Because surely all points do get tiled eventually by the method above.
Finding progressively larger, finite tilings is not the same as having a single infinite tiling, just like finding larger and larger natural numbers is not the same as having a single number larger than all natural numbers (which wouldn't be a natural number).
König's lemma implies that for tilings both statements are in fact equivalent.
Very nice analogy!
> König's lemma implies that for tilings both statements are in fact equivalent.
Exactly, and instead of working by shifting the tiling (which would produce a sequence of incompatible tilings) it works by finding a sequence of finite tilings where each is a subset of the next, so it makes sense to take the union of the sequence.