DIMACS Princeton Theory Seminar


Title:

RAMSEY'S THEOREM AND ENORMOUS LOWER BOUNDS

Speaker:

Harvey Friedman

Place:

Room 402, Computer Science Building
35 Olden Street
Princeton University.

Time:

12:05 PM (Lunch will be served at 11:45 AM)
Friday, May 2, 1997

Contact:

Sanjeev Arora (arora@cs.princeton.edu)

Abstract:

We begin with a brisk but self contained review of Ramsey's theorem and its well known fantastic upper and lower bounds.

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.


Document last modified on April 24, 1997