*To*: Lawrence Paulson <lp15 at cam.ac.uk>*Subject*: Re: [isabelle] Ramsey.thy*From*: Tjark Weber <webertj at in.tum.de>*Date*: Fri, 18 May 2012 14:12:51 +0200*Cc*: Christian Sternagel <c-sterna at jaist.ac.jp>, isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <DE13A61F-E13F-4E16-9275-80807207BE7C@cam.ac.uk>*References*: <4FB4ACC5.2080106@jaist.ac.jp> <6389563D-9309-459F-B550-BDEFA80E771A@cam.ac.uk> <1337282073.5076.34.camel@weber> <E4AE1EBA-935A-4638-86A1-EB698D86999F@cam.ac.uk> <1337331974.7911.26.camel@weber> <DE13A61F-E13F-4E16-9275-80807207BE7C@cam.ac.uk>

On Fri, 2012-05-18 at 10:42 +0100, Lawrence Paulson wrote: > 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. Even in the binary case, the exact value of R(r,s) is mostly unknown. What is known are (lower and upper) bounds. (A table of such bounds can be found in the Wikipedia article that you quoted.) In particular, R(s,s) grows (only) exponentially. Anyway, my point was merely that one could easily (using the existing proof) prove a stronger version of Ramsey's theorem that could be applied to concrete graphs of sufficient size, while the current (neatly quantified) formulation does not allow the theorem to be applied to any fixed graph. Of course, whether that's an issue depends on the intended use of the theorem. Best regards, Tjark

**References**:**[isabelle] Ramsey.thy***From:*Christian Sternagel

**Re: [isabelle] Ramsey.thy***From:*Lawrence Paulson

**Re: [isabelle] Ramsey.thy***From:*Tjark Weber

**Re: [isabelle] Ramsey.thy***From:*Lawrence Paulson

**Re: [isabelle] Ramsey.thy***From:*Tjark Weber

**Re: [isabelle] Ramsey.thy***From:*Lawrence Paulson

- Previous by Date: [isabelle] Proof mode maintained after outcommenting [Re: Isabelle2012-RC3 available for testing]
- Next by Date: Re: [isabelle] Proof mode maintained after outcommenting [Re: Isabelle2012-RC3 available for testing]
- Previous by Thread: Re: [isabelle] Ramsey.thy
- Next by Thread: [isabelle] fun termination, mutual-recursive datatype
- Cl-isabelle-users May 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list