[FOM] Hall's theorem

[Timothy Y. Chow]

"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.

Tim