[FOM] Hall's theorem

[Andrej Bauer]

Dear FOMers,

Timothy Gowers in his blog wondered in what sense can a statement be
"stronger" than an equivalent one, see
http://gowers.wordpress.com/2008/12/28/how-can-one-equivalent-statement-be-stronger-than-another/

It seems to me that from the logical point of view we can explain the
phenomenon by paying attention to the base theory in which the
equivalence is proved. In the case of Hall's theorem considered in the
post, we'd need a base theory which proves only one direction of the
equivalence, see the blog post and
http://en.wikipedia.org/wiki/Marriage_theorem.

There are in fact several theorems in graph theory which are known to
be "equivalent", see e.g.,
http://robertborgersen.info/Presentations/GS-05R-1.pdf . Of course, in
the usual ZFC formalism they are trivially equivalent by virtue of
being true, but graph theorists still feel that there is more to it.
This is a nice opportunity to advertise f.o.m. by giving to "normal"
mathematicians a mathematically precise explanation of their intuitive
feeling. Read the blog post, it is calling for meta-mathematical point
of view.

Have finite-combinatorics theorems been reversed (in the sense of
reverse mathematics)? This has to happen over a very weak theory,
perhaps weaker than what is commonly considered in reverse
mathematics. Or perhaps I am wrong.

I wish you all happy holidays!

Andrej Bauer