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:'s_theorem

Incidentally, these Ramsey numbers are inconceivably large, well beyond human comprehension.


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.