Skip to content

I Hate Oracle Results

May 21, 2009


A problem I have with oracle results

solovay

Robert Solovay is one of the greatest problem solvers in mathematics, or complexity theory, or anything else for that matter. Bob is one of the top set theorists in the world, one of the top logicians in the world, and certainly one of the top theorists in the world.

He is the answer, legend has it, to the question: “what is the minimum number of conference-journal publications that one needs to get tenure at the Berkeley mathematics department?” The answer is {0}. None. Of course he had just solved a long standing open problem in set theory, and was circulating a hand-written draft of his paper, when he was up for tenure. But still, a very impressive result: tenure with zero publications.

There is also what I call the “{n>1}” story. In the 1970’s a visitor–let’s call him W–was spending a semester at Berkeley. He was working on a certain combinatorial problem about languages. The theorem that he was trying to prove was of the following form — for all languages {L}, the property {\dots} held. W worked hard and finally proved the theorem for any {L \subseteq \{a\}^{*}}. Even this case of languages over a single letter alphabet was a complex combinatorial argument.

The next step for W, naturally, was to try and generalize his proof to the case of alphabets of two or more letters. Unfortunately, all the methods W tried would not break the problem and yield a proof. Finally, he went to see Solovay, who is an expert problem solver, as I already stated. Bob listened to W explain his problem, and then he told W that he liked the problem, and he would be happy to think about it.

The next week Bob called W and told him that he should come by and see Bob, since he had solved the general case of any finite alphabet. W was delighted, and soon was in Bob’s office listening to the details of the proof. The proof was complete, W’s problem was finally solved. Wonderful.

Finally, W asked Bob if they should write up a joint paper on the problem. Solovay politely declined. W insisted, since after all Bob had found the general proof. Bob again said no thanks. So finally W left the office. I believe the reason Solovay declined was that he was busy writing up a big result he had just gotten in set theory. But in any event he declined.

On his own, W wrote up the paper, submitted it to a quality journal, and it finally passed all the refereeing process and appeared. On the first page of the paper, W placed a footnote that said:

“The author wishes to thank Bob Solovay for proving the special case of the main theorem when {n} is greater than {1} .”

I checked it, the quote is really there.

Oracle Results

Of course, Theodore Baker, John Gill, Robert Solovay brought oracle results to computer science. In their famous paper they proved the original oracle theorems. In particular they proved, among other results, the following theorem:

Theorem: There is an oracle {A} so that

\displaystyle  \mathsf{P}^A = \mathsf{NP}^{A}.

Also there is another oracle {B} so that

\displaystyle  \mathsf{P}^B \neq \mathsf{NP}^{B}.

Since then hundreds of oracle results have been proved in all parts of complexity theory. Oracle results are sometimes easy to prove, sometimes very difficult, and sometimes remain open. For example, the problem of finding an oracle that shows that probabilistic polynomial time computation could collapse to linear time is still open.

Oracles?

I do not like oracle results. With all due respect, there is something wrong with oracle results that I would like to share with you today.

Let’s look at one classic result: there is an oracle {A} so that

\displaystyle  \mathsf{P}^A = \mathsf{NP}^{A}.

What does this mean? Suppose that you send me an email with a pdf file. I open the file and see what looks like a latex-ed mathematics paper. The paper has a bunch of definitions and lemmas, and then the main theorem that proves that

\displaystyle  \mathsf{P} \neq \mathsf{NP}.

Should I try and read the proof carefully or not? I scan the proof and I claim that it must be wrong, because it relativizes. I can throw the paper away.

That is how oracle results are supposed to work. My problem is this. How do I know if the proof relativizes or not? If I look at a proof, what is the predicate that determines whether or not a proof about Turing machine behavior relativizes or not? Theorists say that this argument relativizes and this one does not. What is the exact predicate? This is the problem that I have with oracle results. There is no precise, in my opinion, test for whether or not a proof “relativizes”. This is a major problem.

I see claims all the time of the form: “the proof by X clearly relativizes”, but the one by “Y does not.” For example, Vinodchandran Variyam’s beautiful result that {\mathsf{PP}} has circuits of size {n^{k}} for any {k>1} does not relativize. Yet, I do not see many formal proofs that show all the details why a proof does or does not relativizes. I am not saying that any mistakes are being made, but I this is the part of the oracle technology that I do not like.

Independence Theorems

Compare the situation in set theory. Consider the following famous theorem due to Solovay:

Theorem: It is consistent with {\mathsf{ZF}} that every set of real numbers is measurable.

Note, with the Axiom of Choice it is easy to prove that there are non-measurable sets of real numbers.

Suppose that you send me a pdf file that claims to prove that there are non-measurable sets of real numbers–without using the Axiom of Choice. I could scan the proof quickly and as long as I was convinced that your proof was formalizable in Zermelo-Fraenkel Set theory, then I could throw your paper away. If your proof was correct, of course, then {\mathsf{ZF}} would be inconsistent. The point is that telling if the proof fits in {\mathsf{ZF}} should be quite doable, almost mechanical.

From time to time there have been close calls with extensions of {\mathsf{ZF}}. Once I saw Bob and wanted to chat with him. But he told me that he could not talk, and would busy for the next week or more. At that moment he told me, he had on his desk two papers that contradicted each other. If both were correct, then {\mathsf{ZF}} plus certain “large cardinal” axioms would be inconsistent. The papers were from top set theorists and Bob said he had to unravel which, if either, was correct. He pointed out that there were a number of graduate students who were on the ledge–ready to jump–if both the papers were correct. If {\mathsf{ZF}} plus these extra axioms was inconsistent, then their PhD theses would disappear.

Luckily for the students one of the papers had an error.

An Oracle Logic

I do not like oracle results. Okay, that is not going to stop the flood of results of this type. So to be constructive, I would like to make two suggestions.

First, could we create a formal notion of machine proofs so that any proof in this style would automatically relativize? For example, you could imagine that you are allowed to use something like Blum axioms that are specific to time or space. Then, all proofs that fit this format would relativize.

Curiously, Solovay worked on a similar problem years ago. Consider Peano Arithmetic ({\mathsf{PA}}). If {\phi} is a formula, let { \ulcorner \phi \urcorner } be the Gödel number of the formula. Also let { \mathsf{Prov}(\ulcorner \phi \urcorner)} mean that {\mathsf{PA}} can prove {\phi}. Then, one can ask is the following true:

\displaystyle  \mathsf{Prov}(\ulcorner \mathsf{Prov}(\ulcorner B \urcorner) \rightarrow B \urcorner) \rightarrow \mathsf{Prov}(\ulcorner B \urcorner)?

This was proved by Martin Löb, answering a question raised by the logician Leon Henkin. See this for a “cartoon” explanation of why this theorem is true. Solovay showed in 1976 that there was a logic system that could capture all such notions about provability.

I guess what I am asking for is some kind of logic like this that would capture many–all?–proofs about Turing bounds that relativize. I doubt that such a theory exists, but can we get any partial results? Even a theory that captured many proofs would be useful.

Relativization Testing

Second, here is another approach. Suppose that I give you a proof of a complexity result: does it relativize? To be concrete assume that the proof is in Peano Arithmetic ({\mathsf{PA}} ). We are given the proof as usual:

\displaystyle  \phi_{1},\dots,\phi_{m}=\phi

where each step of the proof is either an axiom of { \mathsf{PA} } or follows by a rule of inference of { \mathsf{PA} }. The statement {\phi} is a statement from complexity theory, that relativizes. How hard is it to determine whether or not the proof itself relativizes? Is there a fast test for this? Or can we do this for a weaker system of logic, such as bounded arithmetic?

Open Problems

Solve the problem of creating a reasonable logic that captures all proofs that relativize. Another question is can we “look” at a proof and tell if it relativizes or not? If that is hard, which is my guess, then what does that mean for oracle results?

About these ads
22 Comments leave one →
  1. jmount permalink
    May 21, 2009 7:17 pm

    Robert Solovay is a very nice guy. I am proud to have my own tiny Solovay story.

    I took undergraduate set theory from him. The entire grade was 1/2 midterm and 1/2 final. I blew the midterm and come finals time asked if he could base my grade on the final alone. He agreed, I aced the final (finally got around to studying hard) and he gave me an A. Later on he emailed me that I was the first student who had made such a deal with him who had actually improved from midterm to final.

  2. Jonathan Katz permalink
    May 21, 2009 8:46 pm

    I agree with your sentiments completely. Here is an even easier version of your open problem: give a concise, convincing-but-not-necessarily-formal definition of what it means for a proof to relativize without falling back on the tautology “a proof relativizes if it holds with respect to every oracle”. Hand-wavy statements like “the proof doesn’t rely on the structure of the problem” don’t count. =)

  3. May 21, 2009 8:57 pm

    George Boolos’s book “The Unprovability of Consistency” provides an introduction to logics based on Lob’s Theorem, though from the standpoint of philosophical logic, not computer science. (I read it when I was still a philosopher.) Still, it contains a lot of results in one place, and might be a good starting point.

    http://www.cambridge.org/us/catalogue/catalogue.asp?isbn=0521092973

  4. geomblog permalink
    May 21, 2009 9:46 pm

    What timing ! We just covered the BGS result in our summer algorithms seminar. I was looking at the Arora-Barak book on complexity theory, and in the chapter that covers BGS is this line: “An article of Arora, Impagliazzo and Vazirani [AIV93] …. gives an axiomatic system analogous to Cobham’s axiomatic characterization of P, and this axiom system is shown to imply exactly those statements about P that relativize”.

    The paper is here, and Lance has a response to it in this article.

    • rjlipton permalink*
      May 26, 2009 7:29 am

      I have no read their book. Thanks for pointing this out.

  5. May 21, 2009 9:59 pm

    “I guess what I am asking for is some kind of logic like this that would capture many–all?–proofs about Turing bounds that relativize.”

    “How hard is it to determine whether or not the proof itself relativizes?

    This is a really interesting question. I don’t have any idea about what would be a suitable formal definition for the notion of a proof that relativizes. However, maybe the following note can point out some related limitations:

    http://jigpal.oxfordjournals.org/cgi/content/short/jzn023v1

  6. May 22, 2009 12:45 am

    geomblog: This axiomatic system has just recently been extended by Impagliazzo, Kabanets, and Kolokolova to cover Aaronson and Wigderson‘s extended notion of algebraic relativization or algebrization. The paper will be presented at the upcoming STOC’09, by the way.

  7. Suresh Purini permalink
    May 22, 2009 5:31 am

    While reading papers or attending conference talks, when authors claim “this proof clearly relativizes or the other way around”, I feel stupid, as I don’t see it that clearly. This post makes me feel little better :)

  8. Rahul permalink
    May 22, 2009 8:34 am

    I once heard the following story about Bob Solovay. Someone mentioned a very interesting theorem to Bob. He was impressed, and wanted to know who had proved it.

    He had.

  9. May 22, 2009 4:09 pm

    Hi,

    You might be interested in a paper I wrote characterizing the relativizing techniques,
    with Arora and Vazirani. It is now paper 1 on my website (link given.) I also have a
    paper with Kabanets and Kolokolova at the up-coming STOC on using a similar framework to characterize algebrizing techniques (related to, but not identical, that of Aaronson and Wigderson.)

    • rjlipton permalink*
      May 26, 2009 7:31 am

      I did not know it, will read it right away. Thanks.

  10. May 26, 2009 10:48 am

    Did you have to use the word “hate”? I responded on my blog.

    I took graduate set theory from Solovay. Awesome experience. Interesting tidbit I took from the course: You can’t prove independence of P v. NP via forcing since the P v. NP problem is expressible in Peano Arithmetic.

    • rjlipton permalink*
      May 26, 2009 3:21 pm

      Sorry, probably should have said I have some issues with oracle results…rjlipton

  11. May 26, 2009 3:52 pm

    The n>1 story is great!

Trackbacks

  1. More on BGS and Oracle Proofs « P vs NP
  2. Twitted by ChrisDiehl
  3. A Proof System Based on Ramsey Theory « Gödel’s Lost Letter and P=NP
  4. Math and Theory Proof Methods: A Comparison « Gödel’s Lost Letter and P=NP
  5. Game Changing Conjectures In Mathematics « Gödel’s Lost Letter and P=NP
  6. Does a Ph.D candidate have to publish a paper? - Quora

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

Follow

Get every new post delivered to your Inbox.

Join 1,879 other followers