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:
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
> 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
> Best regards,
This archive was generated by a fusion of
Pipermail (Mailman edition) and