 This corollary would seem to justify Ramsey’s stated aim in this paper to provide a step towards a positive solution to Hilbert’s Entscheidungsproblem though it is possible that the aim he actually had in mind was the related Spectrum Problem. Hilbert’s goal was later shown to be not achievable by the undecidability results of Alonzo Church (1936) and independently Alan Turing (1937). In fact Ramsey’s positive contribution turned out to be the best possible in the sense that decidability fails once the order of the blocks of existential and universal quantifiers is reversed, see Kalmár &amp; Surányi 1950, and Mortimer 1975.