I Hate Oracle Results

A problem I have with oracle results

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 . 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 “” 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 , the property held. W worked hard and finally proved the theorem for any . 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 is greater than .”

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 so that

Also there is another oracle so that

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 so that

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

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 has circuits of size for any 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 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 would be inconsistent. The point is that telling if the proof fits in should be quite doable, almost mechanical.

From time to time there have been close calls with extensions of . 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 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 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 (). If is a formula, let be the Gödel number of the formula. Also let mean that can prove . Then, one can ask is the following true:

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 ( ). We are given the proof as usual:

where each step of the proof is either an axiom of or follows by a rule of inference of . The statement 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?