P vs. NP in a logic with a random oracle

Question

Choose a random oracle $f : \{0,1\}^\ast \to \{0,1\},ドル and define the logic $ZFC^f$ by adding a fresh symbol $g,ドル an axiom that $g$ has the correct type, and one axiom $g(s) = f(s)$ for each $s \in \{0,1\}^\ast$. This is a countably infinite set of axioms since $f$ is not a symbol in $ZFC^f$.

Within $ZFC^f$ we can define $g$-oracle Turing machines in the standard way, for example by using a second tape for the input to $g$ and letting the machine branch on the value of $g$ on the second tape. We then have the complexity classes $P^g,ドル $NP^g,ドル etc. Since $f$ was chosen at random in the metalogic, $P^g \ne NP^g$ is true with probability 1.

Question 1: Is $P^g = NP^g$ independent over $ZFC^f$?

The proof seems immediate: any finite proof in $ZFC^f$ can interrogate at most finitely many values of $g$. However, I am not confident the definitions are sensible.

Question 2: Is there a good reference exploring this type of logic + random oracle construction?

• Emil Jeřábek: This will not do what you presumably intend. Any proof may include only finitely many axioms, hence it may only use information on a finite part of the oracle. In particular, it makes no difference whatsoever if you choose the oracle randomly or otherwise. Since interesting properties are invariant under a finite change in the oracle anyway, you may as well omit the $g(s)=\dots$ axioms entirely.
• Emil Jeřábek: For what its worth, relativization by means of adding an extra symbol in the language (with no specific axioms) is used extensibly in bounded arithmetic.
• Emil Jeřábek: For example, $P^g=BPP^g$ is still independent of $ZFC^g,ドル even though for a random oracle $f,ドル $P^f=BPP^f$ holds with probability 1.

Answer 1

Yes on Question 1 (assuming ZFC is consistent). You don't need $f$ to be random exactly, any $f$ will do. And for the proof you need to also use the fact that there is an oracle $h$ with NP$^h=$P$^h$.