Re: [isabelle] Ramsey.thy

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.


On 18 May 2012, at 10:06, Tjark Weber wrote:

> 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:
> 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 [...]"
> 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.