Somehow it came across me, on first seeing a sketch of them, that the standard proofs of basic Ramsey theory results made use of impredicativity in an essential way. (There may be longer proofs that do not, OC.) Can anyone confirm please? Do basic Ramsey theory proofs require it? Bill Taylor