Re: [isabelle] Ramsey.thy
On Fri, 2012-05-18 at 10:42 +0100, Lawrence Paulson wrote:
> In general, I don't believe that a notation exists to express these
> inconceivably large numbers other than R(r,s) itself. The binary case
> may be an exception.
Even in the binary case, the exact value of R(r,s) is mostly unknown.
What is known are (lower and upper) bounds. (A table of such bounds can
be found in the Wikipedia article that you quoted.) In particular,
R(s,s) grows (only) exponentially.
Anyway, my point was merely that one could easily (using the existing
proof) prove a stronger version of Ramsey's theorem that could be
applied to concrete graphs of sufficient size, while the current (neatly
quantified) formulation does not allow the theorem to be applied to any
fixed graph. Of course, whether that's an issue depends on the intended
use of the theorem.
This archive was generated by a fusion of
Pipermail (Mailman edition) and