P vs. NP in a logic with a random oracle 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?
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$.