[FOM] Hall's theorem

[Stephen Cook]

To answer Andrej Bauer's question below "Have finite-combinatorics
theorems been reversed (in the sense of reverse mathematics)?",
that is the subject of Phuong Nguyen's PhD thesis, available
on his web site http://www.cs.toronto.edu/~pnguyen/

It is also partly the subject of our forthcoming book
"Logical Foundations of Proof Complexity".  (A preliminary
version is available on my web site.)  We have a very weak base
theory that is limited to reasoning in the complexity class AC0
(which cannot even count mod 2).  Chapter 9 shows how to define
theories based on various complexity classes contained in
polynomial time, and gives examples of what each theory can prove.
     To formulate Hall's theorem we need functions that can count,
so it can be naturally formulated in our theory VTC0 which
corresponds to the counting complexity class TC0.  Indeed in this
theory one direction is easy to prove, namely if a bipartite graph
has a perfect matching then every set of left vertices must have at
least as many right vertices among its neighbors.  But the converse
requires constructing a perfect matching, and this is not thought to be
possible in the complexity class TC0.  Certainly a maximum
matching can always be contructed in polynomial time, and the
converse can be proved in the theory VP for polynomial time
reasoning (as well as in Buss's theory S-1-2).  The smallest
compexity class known to compute maximum matchings is random
NC2, but we have not yet developed a theory for reasoning within
that class.

Stephen Cook

On Sun, 28 Dec 2008, Andrej Bauer wrote:

> 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
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>