MIT Department of Electrical Engineering & Computer Science

Ramsey's Theorem and Enormous Lower Bounds

Harvey Friedman
Ohio State University

Abstract

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 Another aspect of this is the presentation of very simple valid sentences in predicate calculus all of whose proofs in predicate calculus are of enormous length. These sentences are proved to be valid sentences using Ramsey's theorem.

HOST: Professor Albert R. Meyer