# Is this definability principle consistent?

(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?

• Of course one could consider variants of omniscience gotten by either weakening the exact-equality hypothesis on $\varphi$ to e.g. $V\cap \varphi^{V[G]} = \varphi^{V}$ or by replacing forcing extensions with some other type of model-modification, but the version above seems like the most easily analyzed version of omniscience. Jul 30 at 18:17
• Your formulas are metatheoretic formulas, right, and so being ominiscinet doesn't seem itself to be expressible, despite your remarks about the expressibility of the specific claims of $\varphi$, $\psi$. Is that correct? Thus, to be omniscient is a purely metatheoretic claim about a theory, rather than a set-theoretically expressible property. Right? Jul 30 at 19:23
• @JoelDavidHamkins I don't think so. I never refer to the truth of a sentence, only it's provability in $T$. Also the quantification over sentences happens inside a provability claim (the now-bolded "$T$ proves" preceding the indented clause), so im not restricting to standard sentences. Unless I'm missing something, "$T$ is omniscient" is just "$T$ proves that for all $a$, $T$ proves $p(a)$." While the $p$s involved are of arbitrary complexity, I only talk about their provability. So omniscience is $\Sigma^0_1$. Jul 30 at 20:23
• I think this is equivalent to the following question: is there a total recursive function $t$ sending formulas to formulas such that the theory ZFC plus the scheme asserting, for each formula $\varphi$, "If $\varphi$ is absolute from a parameter, then $t(\varphi)$ defines its truth predicate from that parameter" is $\Sigma^0_1$-sound? If so, one has an omniscient theory: ZFC plus the scheme plus "$t$ is total." On the other hand, given an omniscient $\Sigma_1^0$-sound theory $T$, one can define $t$ to send $\varphi$ to the first $\psi$ that $T$-provably witnesses the scheme. Sound right? Aug 1 at 23:57
• More substantively, as you probably know, the scheme is inconsistent with ZFC + an extendible cardinal by Usuba's theorem: the mantle has a generically absolute definition, but being a ground, its satisfaction predicate is not definable. In general, before turning to the omniscience question, one might warm up with the question: can the satisfaction predicate of the mantle be definable (without parameters). The answer is yes: assuming $\Delta^1_2$-determinacy, for a Turing cone of $x$, satisfaction predicate of the mantle of $L[x]$ is definable over $L[x]$. Aug 2 at 0:05

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.

• Out of curiosity, do you see an interesting lower bound on the possible consistency strength of an omniscient theory? Sep 23 at 20:03
• I don’t even see how to get an inaccessible right now. Sep 23 at 20:58

I shall make two points, but unfortunately neither of them fully answers your question.

First, let me elaborate on the applicability of Usuba's results to this question, as pointed out also by Gabe in the comments.

Every omniscient theory has some large cardinal strength, since we will get truth predicates for $$L$$ and indeed $$L[y]$$ for every set $$y$$, and this requires strictly greater consistency strength than ZFC. But omniscience, meanwhile, will be incompatible with certain very large cardinals, such as an extendible cardinal.

Theorem. Every omniscient theory refutes the existence of an extendible cardinal.

This is because a theorem of Toshimichi Usuba (Extendible cardinals and the mantle, ZBL07006127) shows that if there is an extendible cardinal, then the universe has a bedrock, a ground model of the universe by set forcing that is least among all such grounds. This ground model is the mantle $$M$$, which is a parameter-free definable class, defined as the intersection of all ground models. (For background on bedrocks, the mantle, and set-theoretic geology generally, see Fuchs, Gunter; Hamkins, Joel David; Reitz, Jonas, Set-theoretic geology, Ann. Pure Appl. Logic 166, No. 4, 464-501 (2015). ZBL1348.03051.)

The relevance of this is that if the universe has a bedrock model $$M$$, then $$V=M[G]$$ for some $$M$$-generic set forcing $$G\subset\mathbb{P}\in M$$, and since $$M$$ is definable as the mantle in a forcing-absolute manner, it would follow that $$V$$ itself has a forcing-invariant parametric definition—it is "the forcing extension of the mantle $$M$$ using $$G$$ and $$\mathbb{P}$$."

In particular, if $$V$$ has truth predicates for every forcing-invariant definable class, then this would have to include $$V$$ itself. But we cannot have a truth predicate for $$V$$ definable in $$V$$, since this contradicts Tarski's theorem.

Second, let me offer a positive answer to a weakened version of your question. I would like to weaken the notion of omniscience by modifying the notion of forcing-invariance in the following ways:

• You had wanted the class defined by $$\varphi(\cdot,y)$$ to be forcing invariant from $$V$$ to its forcing extensions; but I shall consider such classes that are invariant both upward and downward, also from $$V$$ to its ground models $$W$$, provided they contain the parameter $$y\in W$$. (In fact, I shall need only the downward part of absoluteness.)
• I would like to consider not just set forcing, but also certain very-well-behaved class forcing notions, the progressively closed Easton iterations. (In fact, I shall be able to handle every $$\varphi$$ that is invariant merely for a very specific type of Easton support progressively closed iteration.)

This kind of class forcing is always very nice: it is tame; it preserves ZFC, GBC, and KM; it has definable forcing relations; and so on.

To achieve weakened omniscience, let me begin with any model $$V$$ of Kelley-Morse KM set theory, although it is sufficient to have GBC+ETR$${}_\omega$$ and even less than this. I shall construct a class-forcing extension $$V[G]$$ by progressively closed Easton-support forcing iteration of length Ord, such that for any first-order formula $$\varphi$$, ordinal $$\alpha$$ and parameter $$y\in V[G_\alpha]$$, there is a definable truth predicate for the class $$\{x\mid\varphi(x,y)\}^{V[G_\alpha]}$$ defined in that model.

We can easily obtain this simply by coding into the GCH pattern. We had started with KM, which has plenty of truth-predicate classes for first-order truth over any class. So we can reserve a definable class of coding points (which will be sufficiently absolutely definable as in the usual geology arguments) for $$\langle\varphi,\alpha,y\rangle$$, and then gradually force the GCH to hold or fail at those coding points in such a way so as to code a truth predicate for that class. It seems to me that it suffices for us to code a truth predicate for each $$V[G_\alpha]$$ itself, since truth about $$\varphi$$ in this model reduces to truth in this model. We can interleave all this coding forcing together into one big progressively closed iteration.

Consider the final model $$V[G]$$. Consider any formula $$\varphi$$ and parameter $$y$$, which must have been added by some stage $$V[G_\alpha]$$. If $$\varphi(\cdot,y)$$ defines an invariant class in $$V[G]$$, then by the downward aspect of this, the class defined in $$V[G]$$ will be the same as defined in $$V[G_\alpha]$$. And we specifically coded a truth predicate for this into the GCH pattern of $$V[G]$$.

So we have constructed a model of KM in which every first-order definable invariant class admits a definable truth predicate.

One can produce a theory $$T$$ that simply describes what we have done: the theory $$T$$ asserts that the universe was obtained by forcing over a model $$W$$ so as to code truth predicates into the GCH patter for every model $$W[G_\alpha]$$ that was used along the way.

This theory is entirely first-order expressible, and so we can throw away the classes after doing the forcing. The theory $$T$$ expresses:

• There is a definable inner model $$W$$ such that the GCH pattern at the first class of coding points codes a truth predicate for $$W$$.
• and there is a class $$G$$ that is defined by the GCH pattern at the second class of coding points, which is a sequence of sets $$G_\alpha$$
• the GCH pattern at the $$\alpha$$th class of coding points codes a truth predicate for $$W[G_\alpha]$$
• The class $$G$$ is $$W$$-generic for the class forcing that would perform the forcing creating this very situation.

This all seems to involve only first-order matters.

So we've got a first-order theory $$T$$ extending ZFC, which is consistent relative to KM, which satisfies the omniscience property for definable forcing-invariant classes, when this is understand to refer to downward-invariance by progressively closed class forcing.

• Oh dear, I see now that Gabe has already made this point in the comments! I guess I'll delete. Aug 8 at 10:23
• I have now expanded my answer with a second part, addressing a version of the question for certain kinds of class forcing. Aug 8 at 13:46
• I think I should write up this construction into a paper, since the resulting axiom is quite interesting... The Truth-encoding axiom: the universe was obtained by a forcing iteration over an inner model that coded truth predicates for each of its partial extensions into the GCH pattern. Aug 8 at 15:42
• Thanks Joel - while I'm still interested in the broader question (so I've held off on accepting) this is definitely worth the bounty. I'm interested in thinking about this more; would you mind if I emailed you? (I'm rather new to set-theoretic geology.) Aug 8 at 20:31
• Sure, please do, at my Oxford address. Thanks for the bounty! Aug 8 at 20:34