[FOM] Proof theoretic strength of relativisable arguments in computational complexity

[Alasdair Urquhart]

Timothy Chow raises a question that I have thought
about quite a lot, but to no avail, i.e.


	The Baker-Gill-Solovay theorem tells us that there exist oracles A and B
	such that P^A = NP^A and P^B <> NP^B.  That is, any proof that P <> NP
	cannot relativize.

	Conventional wisdom says that if a separation argument (i.e., an argument
	that separates complexity classes) is "simple," then it relativizes.
	Baker-Gill-Solovay is often interpreted as saying that P <> NP is
	undecidable by "simple" arguments.

	Question: Have there been any efforts to determine the precise proof-
	theoretic strength of relativizable arguments?

Oracle results are often discussed in the literature of complexity 
theory as if they were independence results, but this is clearly
a misinterpretation.  In other words, the exact import of oracle
results in complexity theory is really very obscure, from the logical
point of view.  

Obviously, polynomial-time machines and polynomial-time machines
with oracles share certain closure conditions, so if you have
proved "P=NP" or "P <> NP" using only these conditions, then
your proof must be wrong.  But can't we say more?

For example, what is to be made of the frequently heard remark:

	"Diagonal arguments relativize"?

I really have no good ideas here, but I do think that Tim Chow's 
question is a very important problem in the foundations of
computer science.  I would very much like to hear from other
people on this topic.

Alasdair