Ramsey proved Ramsey's theorem in his famous 1930 paper, "On a problem of formal logic," in order to solve a problem in formal logic. Specifically, he gives a decision procedure for the satisfiability of universal sentences in predicate calculus with equality and no function symbols. The decision procedure is relatively tame (nondeterministic exponential).
We discuss some other decision problems connected with the finite
models of universal sentences. We give decision procedures for them
using Ramsey's theorem. We then determine the computational complexity
of these problems. These computational complexities are exotic. The
least exotic requires iterated exponential time. The most exotic has
time complexity going just beyond the provably recursive functions of
Peano Arithmetic (which are the