Email Gateway (Aug 18 2022 at 19:44): Email Gateway (Aug 18 2022 at 19:44):From: Christian Sternagel <c-sterna@jaist.ac.jp>
Dear all,
I am a bit confused concerning Ramsey.thy from HOL's library. More
specifically @{thm ramsey2}. How am I ever able to discharge the
assumption when the whole theorem is wrapped inside an "EX r >= 1. ..."?
Did anybody use @{thm ramsey2} before? Any hints are appreciated.
cheers
chris
Email Gateway (Aug 18 2022 at 19:44):From: Lawrence Paulson <lp15@cam.ac.uk>
You use it to obtain a positive integer r, the Ramsey number, satisfying the Ramsay condition, which is the body of the quantified formula. Have fun!
Larry Paulson
Email Gateway (Aug 18 2022 at 19:44):From: Tjark Weber <webertj@in.tum.de>
But the theorem places no upper bound on r. In its present form, it is
only useful if one has a family of graphs of unbounded size. Otherwise,
there will be no way to discharge the assumption "card V ≥ r" in the
Ramsey condition.
It seems unfortunate that the upper bound on r that is implicit in the
proof is lost through the existentially quantified formulation of the
theorem.
Best regards,
Tjark
Email Gateway (Aug 18 2022 at 19:45):From: Lawrence Paulson <lp15@cam.ac.uk>
An upper bound on r? There is no such thing. Ramsey's theorem states a certain conclusion “for all sufficiently large graphs". The number r defines what is meant by “sufficiently large".
There's more information on Wikipedia:
http://en.wikipedia.org/wiki/Ramsey's_theorem
Incidentally, these Ramsey numbers are inconceivably large, well beyond human comprehension.
Larry
Email Gateway (Aug 18 2022 at 19:45):From: Tjark Weber <webertj@in.tum.de>
But the proof constructs an explicit witness for r, i.e., it shows that
a specific r (which depends on the parameters m and n, of course) is in
fact sufficiently large.
"The numbers R(r,s) in Ramsey's theorem (and their extensions to more
than two colours) are known as Ramsey numbers. An upper bound for R(r,s)
can be extracted from the proof of the theorem [...]"
http://en.wikipedia.org/wiki/Ramsey%27s_theorem#Ramsey_numbers
For instance, the usual proof of the theorem tells us that R(3,3) <= 6.
In contrast, the existentially quantified statement merely shows that
R(3,3) exists, but does not give an upper bound for it.
Best regards,
Tjark
Email Gateway (Aug 18 2022 at 19:45):From: Lawrence Paulson <lp15@cam.ac.uk>
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.
Larry
Email Gateway (Aug 18 2022 at 19:46):From: Tjark Weber <webertj@in.tum.de>
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.
Best regards,
Tjark
Last updated: Apr 18 2024 at 20:16 UTC