[FOM] Reverse mathematics of spectral graph theory

[Timothy Y. Chow]

Some months ago, someone asked on cstheory.SE for examples of statements 
in graph theory that can be proved only by spectral means.

http://cstheory.stackexchange.com/questions/5099/proofs-obtained-only-through-spectral-graph-theory

It's not so easy to come up with definitive examples, because it is 
sometimes possible to unpack the linear algebra into a combinatorial proof 
that makes no explicit reference to linear-algebraic concepts.  For 
example, Sundar Vishwanathan posted a preprint to the ArXiv not long ago 
giving a combinatorial proof of the Graham-Pollak theorem, which for a 
long time was an example of a purely graph-theoretic statement that seemed 
to require linear algebra (if not eigenvalues explicitly):

http://arxiv.org/abs/1007.1553

Vishwanathan makes some intriguing comments at the end that, roughly 
speaking, suggest that fast-growing functions might be needed to prove the 
Graham-Pollak theorem.  "Fast-growing" here doesn't mean Ackerman and 
beyond but just exponential versus polynomial.

This makes me wonder whether there is, at least potentially, some way to 
prove that certain classical theorems of spectral graph theory (like the 
Graham-Pollak theorem, the friendship theorem, the Hoffman-Singleton 
theorem, etc.) "require" some strong assumption in a reverse-mathematical 
sense.  I know that Cook and others have looked in the proof complexity of 
linear algebra and have isolated some candidates for hard tautologies 
coming from linear algebra.  Perhaps some of these spectral graph theorems 
are "equivalent" in some sense one of these hard tautologies?  Has anyone 
looked into this kind of thing?

Tim