6 ms·

Weird. It's not my field at all but intuitively, I would have approached a proof by trying to formalise the following: 1/ Complete part of the tiling in the up

Weird. It's not my field at all but intuitively, I would have approached a proof by trying to formalise the following: 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?

ot 9y ago
That's what I meant by attempting to find a constructive proof. 2 doesn't work because no matter how much you shift down and to the left you'll always have a boundary. > our link proves something stronger No, it proves that the 3 statements are equivalent, so it is not stronger.
- soVeryTired 9y ago
  But isn't it enough to show that any point in the plane will eventually get tiled after 1 - 3 run for long enough? Because surely all points do get tiled eventually by the method above.
  - foobar__ 9y ago
    This falls short of the original goal: While your method shows that for every point, you can find a tiling large enough that covers it, the original question was to find a single tiling covering everything. 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.
    - deleted 9y ago
      [deleted]
    - nightcracker 9y ago
      With the caveat that if your tiling is inductive in the sense that the tiling of n+1 is an extension of n, a series of finite tilings will tile the plane.
    - ot 9y ago
      > like finding larger and larger natural numbers is not the same as having a single number larger than all natural numbers 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.

ot 9y ago

That's what I meant by attempting to find a constructive proof. 2 doesn't work because no matter how much you shift down and to the left you'll always have a boundary. > our link proves something stronger No, it proves that the 3 statements are equivalent, so it is not stronger.

soVeryTired 9y ago
But isn't it enough to show that any point in the plane will eventually get tiled after 1 - 3 run for long enough? Because surely all points do get tiled eventually by the method above.
- foobar__ 9y ago
  This falls short of the original goal: While your method shows that for every point, you can find a tiling large enough that covers it, the original question was to find a single tiling covering everything. 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.
  - deleted 9y ago
    [deleted]
  - nightcracker 9y ago
    With the caveat that if your tiling is inductive in the sense that the tiling of n+1 is an extension of n, a series of finite tilings will tile the plane.
  - ot 9y ago
    > like finding larger and larger natural numbers is not the same as having a single number larger than all natural numbers 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.