What is needed to prove Monsky's theorem?

[Timothy Y. Chow]

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.

Tim