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.



Is the forcing relation defined for mathematical formulas?
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.


