[FOM] r.e. Hall's Theorem

[Jeff Hirst]

Andrej Bauer said:
"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."


One example of such a reversal is the main result of Friedman, McAloon,
and Simpson in "A finite combinatorial principle which is equivalent
to the 1-consistency of predicative analysis," in
Patras Logic Symposion (Patras, 1980), 197–230, Stud. Logic Foundations Math., 109,
North-Holland, Amsterdam-New York, 1982.  In short, the authors formulate
a finite combinatorial statement "for every n there exists an n-dense finite set,"
and prove that it is equivalent to the 1-consistency of ATR0 over primitive
recursive arithmetic.

It seems to me that this result would still have been interesting even if the
base system was much stronger, provided that the base system did not prove
the 1-consistency of ATR0.  In particular, the proof could have been carried
out in ATR0 and the result would have had value, though clearly it would
not have been as strong as the result over PRA.  Thus, I believe that it is
possible to do reversals of finite combinatorial statements over relatively
strong subsystems and obtain results of interest.

Harvey Friedman has discovered a number of finite combinatorial statements that
are provably equivalent to large cardinal hypotheses over ZFC.  For example, see
his "Finite functions and the necessary use of large cardinals," Ann. of Math.
(2) 148 (1998) no. 3, 803-893.  A very brief exposition of the result (without
any attempt at proof) appears in section 3.9 of "Combinatorics and Graph Theory,
Second Edition" by Harris, Hirst, and Mossinghoff.  (It's section 3.8 in the
first edition.)


Since Andrej mentioned reverse mathematics and Hall's theorem in the same post,
perhaps I should point out that I formalized Philip Hall's theorem (for finite marriage
problems) in RCA0 in my PhD thesis, and then used that to prove versions of Marshall
Hall's theorem (for infinite marriage problems) which reverse to ACA0 and WKL0.
The proofs emulate earlier work of Manaster, Rosenstein, and (separately) McAloon.
For details, see "Marriage Theorems and Reverse Mathematics," in Logic and Computation,
Contemporary Mathematics 106, American Mathematical Society, 1990, 181-196.
This work did not reverse Philip Hall's theorem, and so does not address Andrej's
question about reversals of finite combinatorial statements.  On the other hand,
it should be possible to formulate a "finite miniturization" of Marshall Hall's theorem
(after the fashion of Friedman, McAloon, and Simpson) and obtain a finite combinatorial
result that would imply a strong consistency statement over RCA0 (or maybe even PRA).
Of course, this is probably much easier said than actually done.


I hope this is helpful...

Jeff Hirst

Jeff Hirst,  Professor of Mathematics
Department of Mathematical Sciences
Appalachian State University
Boone, NC 28608
828-262-2861      FAX:  828-265-8716