# Re: [isabelle] Ramsey.thy

On Fri, 2012-05-18 at 08:28 +0100, Lawrence Paulson wrote:
> 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
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

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*