# Re: [isabelle] Ramsey.thy

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
On 17 May 2012, at 20:14, Tjark Weber wrote:
> On Thu, 2012-05-17 at 19:33 +0100, Lawrence Paulson wrote:
>> You use it to obtain a positive integer r, the Ramsey number,
>> satisfying the Ramsay condition, which is the body of the quantified
>> formula.
>
> 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
>
>

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