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?