[FOM] Hall's theorem
Timothy Y. Chow
tchow at alum.mit.edu
Tue Dec 30 17:15:00 EST 2008
"Andrej Bauer" <andrej.bauer at andrej.com> wrote:
> Timothy Gowers in his blog wondered in what sense can a statement be
> "stronger" than an equivalent one
...for example, one half of Hall's theorem versus the other.
This is a notoriously tricky question. Some of the relevant issues came
up in the context of Gowers's earlier blog post on "when are two proofs
essentially the same"; my comment to that blog post remarked that many
people feel that Sperner's lemma and Brouwer's fixed-point theorem are
"equivalent," even though Sperner's lemma is provable in RCA_0 while
Brouwer's theorem isn't. This illustrates that reverse mathematics isn't
necessarily going to be the full answer here.
Much of what's going on here is psychological---X is stronger than Y if
it's "easy" to see that X implies Y but it's not easy to see the opposite.
Easy for whom, you ask? Well...for me, I guess? For human beings? For
computer programs? Probably there is no definitive way to formalize what
is going on. Not that we can't get some interesting insights from the
attempt to formalize, but we should be wary of assuming that there really
is some unique Platonic definition of "easy" out there that we could write
down formally if we just thought hard enough.
More information about the FOM