Forcing: The ground model is a proper class

Question

If $M \in V$ is a transitive, countable model of ZFC and $G$ a generic filter on a forcing poset $P \in M$, then we can construct the forcing extension M[G] of M. It is the smallest transitive model of ZFC such that $M[G] \supset M$ and $G \in M[G]$. Is it possible to do the same if we assume that the ground model $M \subset V$ is a proper class?

Answer 1

The most beautiful point about forcing, is that ultimately, this is all something you can do internally, granted that there are generic filters (which you can sometimes prove to exist).

More specifically, given a class $M\subseteq V$, and some $\Bbb P\in M$, if there is some $G\subseteq\Bbb P$ such that $G$ is an $M$-generic filter over $M$, then $M[G]$ is the least transitive class satisfying all the axioms of $\sf ZF$ such that $M$ is a subclass of $M[G]$ and $G\in M[G]$.

It even follows that:

1. $M[G]=\bigcup\{L[x,G]\mid x\in M\}$, and
2. $M$ is a class of $M[G]$, granted that $M$ was a model of $\sf ZFC$ (in which case $M]G]$ also satisfies choice).

There are some caveats, though:

1. The forcing theorem is not a theorem, but rather a schema, or a meta-theorem. But this is the same situation as when working with countable transitive models of $\sf ZFC$. In the set-model case, this is because we prove the theorem about $M$ in $V$, and $V$ is the meta-theoretic universe as far as $M$ is concerned.

2. The existence of generic filters is no longer a theorem. This, however, also happens when we force over uncountable models. For example, if $M$ is a transitive model which contains all the reals (in particular $M$ is uncountable), then there are no generic filters for any forcing in $M$ which "should add reals". Simply because all the reals are already in $M$, so we can't add anything new.