(Below I'm thinking only about computably axiomatizable set theories extending $\mathsf{ZFC}$ which are arithmetically, or at least $\Sigma^0_1$-, sound.)
Say that a theory $T$ is omniscient iff $T$ proves that the following holds:
For every formula $\varphi(x,y)$ there is some formula $\psi(z,y)$ such that $T$ proves: "For all $y$, if $\varphi(-,y)^V=\varphi(-,y)^{V[G]}$ for every set generic extension $V[G]$, then $\psi(-,y)$ is a truth predicate for $\varphi(-,y)^V$."
(That's not a typo, I do want a "$\vdash\vdash$"-situation. Note that by the soundness assumption on $T$, there really does exist such a $\psi$ for every $\varphi$.)
Two points about omniscience are worth noting:
-
For each $\varphi,\psi$, the statement in quotes is indeed expressible in the language of set theory – in particular, although we can't talk about the full theory of a generic extension via a single sentence, for each $\varphi,\psi$ we only need to talk about a bounded amount of those theories. So it does in fact make sense.
-
$\mathsf{ZFC}$ itself is not omniscient – since $\mathsf{ZFC}$ proves that $L$ is forcing-invariant, any omniscient theory must prove that $V$ is not a set forcing extension of $L$. Informally speaking, any omniscient theory must prove that $V$ is "much bigger" than any canonical inner model.
Omniscience strikes me as an implausibly strong property. However, I don't see an immediate reason why no consistent omniscient theory can exist. So my question is:
Is there a consistent omniscient theory at all?
Best Answer
There is a consistent omniscient theory, at least assuming the consistency of a Woodin limit of Woodin cardinals.
The Maximality Principle (MP) asserts that if a sentence is forceable in $V$, it is forceable in every generic extension of $V$. In other words, if a sentence can be forced to be indestructible by set forcing, then the sentence was true all along. Variants of the principle were discovered independently by many people, including Stavi, Väänänen, Bagaria, Chalons, and Hamkins. The main reference is Hamkins's paper. The Boldface MP (due to Hamkins) asserts the same but allowing hereditarily countable parameters. The Necessary MP (NMP, also due to Hamkins) asserts that the Boldface MP is true in all forcing extensions. MP and BMP are fairly weak, but Woodin [unpublished] showed the consistency strength of NMP lies between $\text{AD}$ and $\text{AD}_\mathbb R + \Theta \text{ is regular}$. I claim ZFC + NMP is an omniscient theory. Since $\text{AD}_\mathbb R + \Theta\text{ is regular}$ is consistent (by a theorem of Sargsyan its consistency follows from a Woodin limit of Woodin cardinals), so is ZFC + NMP.
The proof is essentially due to Hamkins, who showed that under NMP, if $W$ is a forcing invariant inner model, then for all cardinals $\lambda$, $H(\lambda)\cap W\preceq W$. His proof adapts to the case that $W$ is an arbitrary class with a forcing invariant definition using a parameter $x$, although of course one must assume $\lambda$ is above the hereditary cardinality of $x$. This implies that the truth predicate for $W$ is definable: $W\vDash \varphi(\overline p)$ if and only if $W\cap H(\lambda) \vDash \varphi(\overline p)$ for some/all $\lambda > |\text{tc}(p)|$.
I recite Hamkins's proof below since it's nice and I wanted to check that it works, but there are really no new ideas.
We want to show that the truth predicate for $(W,\in)$ is definable from $x$. By homogeneity, it suffices to show it is definable from $x$ over $V[G]$ where $G$ is generic for $\text{Col}(\omega,\text{tc}(x))$. We may therefore pass to $V[G]$ and assume without loss of generality that $x$ is hereditarily countable. (This is ok because $V[G]$ is also a model of NMP.)
Now fix a cardinal $\lambda$, and I will show $W\cap H(\lambda) \preceq W$. By induction on the complexity of $\varphi$, I'll show that $\varphi$ is absolute between $W\cap H(\lambda)$ and $W$. The only nontrivial step is to show that if $\varphi(\overline u) \equiv \exists t\, \psi(t,\overline u)$ and $\psi$ is absolute between $W\cap H(\lambda)$ and $W$, then $\varphi$ is absolute as well. So fix $\overline p\in W\cap H(\lambda)$ and suppose $W\vDash \varphi(\overline p)$.
Let $H$ be generic for $\text{Col}(\text{tc}(\overline p))$. In $V[H]$, one can force so that the minimum hereditary cardinality of a set $z\in W$ such that $W\vDash \psi(z,\overline p)$ is at most $\aleph_0$. Once this is true, it is of course true in any outer model, so applying the Boldface MP in $V[H]$, $V[H]$ satisfies that the minimum hereditary cardinality of a set $z\in W$ such that $W\vDash \psi(z,\overline p)$ is at most $\aleph_0$. Fix such a set $z\in W$. Then $z\in V$ (since $W\subseteq V$) and the hereditary cardinality of $z$ is at $|\text{tc}(\overline p)| < \lambda$. Thus there is some $z\in W\cap H(\lambda)$ such that $W\vDash \psi(z,\overline p)$, and so by our induction hypothesis, $W\cap H(\lambda)\vDash \psi(z,\overline p)$, and hence $W\cap H(\lambda)\vDash \varphi(\overline p)$ as desired.