What is needed to prove Monsky's theorem?
Timothy Y. Chow
tchow at math.princeton.edu
Mon Sep 19 11:27:28 EDT 2022
In 1970, Monsky proved that it is not possible to dissect a square into an
odd number of triangles of equal area. Monsky's proof of this
innocent-looking result attracted considerable attention, in large part
because it unexpectedly used the fact that the 2-adic valuation on the
rationals can be extended to the real numbers. To be clear, John Thomas
had previously proven the special case in which the vertices of the
triangles are rational numbers with odd denominators, so the relevance of
the 2-adic valuation did not appear completely out of left field.
Nevertheless, extending the 2-adic valuation to a transcendental extension
is not something that one typically expects to be relevant to what seems
to be a simple question in elementary plane geometry.
Occasionally someone will ask whether Monsky's theorem relies on the axiom
of choice. The answer of course is no---Monsky himself pointed out that
the valuation only needs to be extended to the subfield generated by the
coordinates of the vertices in question.
It's still interesting (to me at least) to ask what is really needed for
Monsky's theorem. Does any FOM reader know? My shoot-from-the-hip guess
is ACA_0, because it does seem that that the proof does have to consider
transcendental extensions of the rationals. So that makes me think
"transcendence basis," which in turn makes me think ACA_0. But it's not
clear to me how to show that ACA_0 is really needed.
If ACA_0 is really needed, this might partly answer the question of
whether Monsky's theorem is "intrinsically hard to prove"---a question
that has fascinated many people over the decades.
I should mention that there's another ingenious ingredient in Monsky's
proof, which is the use of a clever coloring, and a Sperner's-lemma-type
argument. But my guess is that this part of the proof does not require
anything beyond RCA_0.
By the way, another question is whether Monsky's theorem can be proved
using intuitionistic logic. I don't immediately spot any use of LEM in
the proof, but I'm not fluent in that sort of thing.
More information about the FOM