2
$\begingroup$

I've been thinking about Monsky's Theorem that it is impossible to partition a square into an odd number of triangles of equal area. The proof depends on a theorem of Chevalley to extend the $2$-adic valaution on $\mathbb{Q}$ to a $2$-adic valuation on $\mathbb{R}$, and Chevalley's theorem relies on the axiom of choice for its proof. According to "Proofs from THE BOOK" (fifth edition, p.$151$) no other proof of Monsky's theorem is known.

If Monsky's theorem were false, the counterexample would be a finite, easily comprehensible object. All the other applications of the axiom of choice I can think of assert the existence of some infinite, complicated object that we don't expect to be able to construct: a Hamel basis for the reals over the rationals, a free ultrafilter, a bounded, non-measurable subset of the reals, and so on.

I recognize that Chevalley's theorem itself asserts the existence of just such an object, but I haven't been able to think of another example where the axiom or one of its consequences is used to prove the non-existence of some "concrete" finite object. I exclude the extensions of Monsky's theorem to other polygons and higher dimensions, of course.

Are such examples really rare? Can you supply any more?

$\endgroup$

1 Answer 1

Reset to default
3
$\begingroup$

Actually, there is a precise result which says that the axiom of choice cannot be necessary for too-concrete results (and in particular that it's not necessary to Monsky's theorem). This is Shoenfield absoluteness:

Suppose $P$ is a $\Pi^1_2$ theorem of $\mathsf{ZFC}$. Then $P$ is already provable in $\mathsf{ZF}$.

Actually Shoenfield says even more - e.g. CH won't be necessary either - but the above is already enough for the OP. It's also worth noting that Shoenfield is in fact completely constructive: it gives a very concrete way to transform a $\mathsf{ZFC}$-proof into a $\mathsf{ZF}$-proof.

"$\Pi^1_2$" is a purely syntactic notion: roughly speaking, a sentence is $\Pi^1_2$ if it has the form "For all $X$ there is some $Y$ such that $H(X,Y)$," where $X$ and $Y$ are "morally equivalent" to real numbers and $H$ involves only quantification over things "morally equivalent" to natural numbers. For example, finitely sets of points in $\mathbb{R}^n$ and continuous functions $\mathbb{R}^a\rightarrow\mathbb{R}^b$ are "morally equivalent" to real numbers, while rational numbers are "morally equivalent" to nautral numbers. Monsky's theorem falls into this category: a triangulation is specified by a finite tuple of reals, and the equal-area property amounts to saying that we can get approximations to the relevant areas which are within arbitrary positive rational differences from each other. (In fact this only involved one "interesting" quantification, namely over finite tuples of reals, so in fact Monsky's theorem is $\Pi^1_1$.)

Note that the above may not truly constitute an error in PftB: Shoenfield merely transforms an existing proof into a sharper proof, and one could still claim that we have no proof of Monsky's theorem whose idea doesn't use Choice. But on a purely technical level, choice cannot be necessary for the proof of such a concrete result.

$\endgroup$
8
  • $\begingroup$ Thank you. This is way beyond my knowledge of set theory and logic. "There exists a proof of Monsky's theorem that does not rely on the axiom of choice." Amazing that such a statement can be proved. $\endgroup$
    – saulspatz
    May 22, 2020 at 16:18
  • $\begingroup$ @saulspatz Here's roughly how the proof goes, FYI. The trick is to use Godel's constructible universe. Essentially, every model $M$ of $\mathsf{ZF}$ has a "definable region" $L^M$ within which Choice holds. Via this construction $M\mapsto L^M$ we can turn correctness results into translation results: if we know "Regardless of what $M$ is, $L^M$ and $M$ agree on whether $P$ is true" then we know "If $\mathsf{ZFC}$ proves $P$ then $\mathsf{ZF}$ proves $P$" (since if $M\models\mathsf{ZF}+P$ then we would have $L^M\models\mathsf{ZFC}+P$). $\endgroup$
    – Noah Schweber
    May 22, 2020 at 16:24
  • $\begingroup$ (Below I'll suppress $M$.) So we just need to show "$L$ is correct for $\Pi^1_2$ sentences." This is a nontrivial argument, but the first piece - $\Pi^1_1$ absoluteness, which is enough for Monsky - is not too hard to describe. The first point is that every $\Pi^1_1$ statement is equivalent to the well-foundedness of a certain tree; basically, think of a tree whose nodes describe approximations to counterexamples of the $\Pi^1_1$ statement, and so whose paths would give actual counterexamples. Now $\mathsf{ZF}$ proves that such a tree either has a path or has a ranking function. $\endgroup$
    – Noah Schweber
    May 22, 2020 at 16:28
  • $\begingroup$ That's an existential statement, and the property of being a path or being a ranking function is simple enough that it's absolute between any two transitive models of $\mathsf{ZFC}$. So the relevant tree looks well-founded in $L$ iff it actually is well-founded. (Bootstrapping this to $\Pi^1_2$ then requires a clever trick, and genuinely pushes us into set theory proper: we need to construe a $\Pi^1_2$ statement as a well-foundedness statement as well, but now the relevant trees are much more complicated.) $\endgroup$
    – Noah Schweber
    May 22, 2020 at 16:30
  • 1
    $\begingroup$ (A bit of terminology: $\Pi^1_1$ absoluteness, which as I said above is sufficient for Monsky, is Mostowski absoluteness.) And the above also tells us how to whip up a choice-free proof of Monsky: $(1)$ Rephrase the usual $\mathsf{ZFC}$-proof of Monsky as a $\mathsf{ZF}$-proof of "Monsky is true in $L$." $(2)$ Prove Shoenfield absoluteness if you haven't already. $(3)$ Combine $(1)$ and $(2)$ to get Monsky. So Shoenfield is awesome but the choice-free proof we get is rather silly. $\endgroup$
    – Noah Schweber
    May 22, 2020 at 16:33

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .