[FOM] Proof-theoretic strength of relativizable arguments in computational complexity

[Timothy Y. Chow]

I am new to this list; "hello" to those of you I know from other contexts.

Let P (respectively, EXP) denote the set of languages accepted by a
deterministic polynomial-time (respectively, exponential-time) Turing
machine.  The usual proof that P <> EXP *relativizes*; i.e., it is
easily adapted to prove that for any oracle A, P^A <> EXP^A.

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?

This question has been around a long time; e.g., it was explicitly posed
by Hartmanis et al. in 1988.

  http://people.cs.uchicago.edu/~fortnow/beatcs/column35.ps

However, I am not aware of any work that has been done on it.  There are
plenty of examples of conjectures with contradictory relativizations, but
the statement that "conjectures with contradictory relativizations are
hard" seems to be just as imprecise today as it was 15 or even 25 years
ago.  (I would be glad to be proved wrong.)

I guess what I'm looking for is a suitable language and axiom set.  The
axioms have to be very weak since "P = NP" has to be provably undecidable,
but the language should be expressive enough to handle arbitrary infinite
families of infinite sets of integers, or at least most of the classes in
the "complexity zoo":

  http://www.cs.berkeley.edu/~aaronson/zoo.html

Any thoughts?

Tim