Re: [isabelle] Ramsey.thy

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

Best regards,

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