Is the forcing relation defined for mathematical formulas?

Question

Meta-matematical formulas of the language of set-theory (which are not sets, but just sequences of signs) should not be confused with mathematical ones (i.e. formulas coded as sets, e.g. finite sequences of natural numbers or even just natural numbers, if we wish). For instance, for each meta-mathematical formula $\phi$, we can define its relativization $\phi^M$ to any class $M$, but the relation $M\vDash \phi[v]$ in the model-theoretic sense can be only defined when $M$ is a set, but not a proper class.

The impossibility of defining $M\vDash\phi[v]$ for proper classes is due to two kinds of reasons: on one hand, if so, we could prove Con ZFC within ZFC, and technically, the problem is that a "typical" recurrence definition of $M\vDash \phi[v]$ would require having defined $M\vDash \psi[w]$ for each subformula $\psi$ of $\phi$ and for each valuation $w$ from the set of free variables of $\psi$ to $M$, and such valuations form a proper class if $M$ is a proper class, and this does not fit the recursion theorem.

My first question is that I suspect that this is also valid for the definition of the forcing relation $p\Vdash \phi$, i.e.:

Question 1: Can the forcing relation $p\Vdash \phi$ be defined for mathematical formulas $\phi$ or just for meta-mathematical ones?

I suspect that only for meta-mathematical ones because in order to define $p\Vdash \forall x\phi(x)$ we must assume that $p\Vdash \phi(\tau)$ is defined for each $\mathbb P$-name $\tau$, and the class of $\mathbb P$-names is a proper class.

This question is related to theorem III 2.11 of Shelah's book Proper and Improper Forcing (second edition). It states that if $\lambda$ is an uncountable cardinal, $N\prec H(\lambda)$ is an elementary submodel of the set of all sets whose transitive closuse has cardinality less than $\lambda$, and $\mathbb P\in N$ is a pre-ordered set, then, for each generic filter $G$ over $V$ we have $N[G]\prec H^{V[G]}(\lambda)$.

The proof is clear, but in order to show that the definition of elementary submodel holds for a formula $\phi$ (in fact, the Tarski-Vaught criterion is considered instead of the definition), the forcing relation $p\Vdash \psi$ is used for a formula $\psi$ involving $\phi$. Hence, if the answer to Question 1 is that it only makes sense for meta-mathematical formulas, we conclude that $N[G]$ is an elementary submodel just in the weak meta-mathematical sense that we have a family of theorems, each one stating that an arbitrary meta-mathematical formula is absolute for $N[G]-H^{V[G]}(\lambda)$.

So, my second question is:

Question 2: Under the hypotheses of Shelah's theorem, can we conclude that $N[G]\prec H^{V[G]}(\lambda)$ in the usual model-theoretic sense (for mathematical formulas) or just in the weak meta-mathematical sense?

I feel that the answer should be positive even if the answer to question 1 is negative.

Answer 1

To answer Question 2, I think your intuition is right. Assume $N \prec H_\lambda$, where $\lambda$ is a regular cardinal bigger than $2^\mathbb{P}$, where $\mathbb{P} \in N$ is a partial order. (Maybe Shelah has a more subtle argument where we assume less about $\lambda$, not sure.) Then $H_\lambda$ is a model of $ZFC$ minus powerset, and we can consider in $V[G]$ the model $H_\lambda[G]$, defined the same way as usual. We have:

• For any generic $G \subseteq \mathbb{P}$, $H_\lambda^{V[G]} = H_\lambda[G]$.
• $G$ is generic over $V$ iff $G$ is generic over $H_\lambda$.
• The basic forcing lemmas, including the "truth lemma," go through for forcing with $\mathbb{P}$ over $H_\lambda$.

The point is that by working in $V[G]$, we can treat $H_\lambda[G]$ as an ordinary set model and carry out the argument that $N[G] \prec H_\lambda[G]$ within the language of set theory in $V[G]$, rather than as a meta-mathematical scheme.

Answer 2

Although the common slogan about forcing is that the forcing relation is definable in the ground model, nevertheless the slogan must be qualified for precisely the issue in your question, and the answer to question 1 is that no, the forcing relation is never definable in full generality as a binary relation in $(p,\varphi)$. That is, if $M$ is a model of ZFC and $\mathbb{P}$ is any forcing notion in $M$, then the relation $p\Vdash\varphi$, as a relation in $(p,\varphi)$, where $p$ is a condition in $\mathbb{P}$ and $\varphi$ is an assertion in the forcing language, is not definable in $M$.

One can prove this using the fact that the ground model $M$ is (uniformly) definable in its forcing extensions $M[G]$, using a parameter in $M$. (This was recently proved by Laver, independently Woodin.) So if we could define the forcing relation in $M$ then we could define in $M$ the relation $\mathbb{1}\Vdash\varphi^M(\check x)$, which is equivalent to $M\models\varphi[x]$. But this is not definable by Tarski's theorem on the non-definability of truth.

Meanwhile, the slogan survives in a way that is strong enough to be extremely useful:

• For any fixed $\varphi(x)$ with a free variable, the relation $p\Vdash\varphi(\tau)$ is definable in $M$ as a relation in $(p,\tau)$. This is how the definability is most often used.

• For any fixed (meta-theoretic) level of complexity $\Sigma_n$, the relation $p\Vdash\varphi$ for conditions $p$ and $\Sigma_n$ formulas $\varphi$ is definable in $M$ as a relation in $(p,\varphi)$. Indeed, the quantifiers of $\varphi$ amount essentially to quantifying over names in $M$, and so one can make a tight connection between the complexity of $\varphi$ and the complexity of $p\Vdash\varphi$.