The usual use of forcing begins with a "countable" and "transitive" ground model of $ZFC$ and reaches to a "countable" and "transitive" generic model of $ZFC$ with the "same ordinals". In a discussion a colleague told me about a special forcing by Solovay which begins with a countable transitive model of $ZFC$ and reaches to an "uncountable" transitive generic model. My question is about these kind of special forcings and their possible special uses.


**Question:** Please introduce a reference about any use of forcing with at least one of the below characteristics:


**(a)** The ground model is uncountable.


**(b)** The ground model is not transitive.


**(c)** The generic model is uncountable.


**(d)** The generic model is not transitive.


**(e)** The generic model has more ordinals than ground model. 



A Question on Special Forcings
I don't agree that the "usual" use of forcing uses only countable transitive models. Perhaps this used to be true, years ago, and forcing is sometimes still taught this way now, because it is somewhat easier to see where the generic filters come from, but neither hypothesis is actually needed to develop a full theory of forcing, and I think that these days it is quite common to understand forcing as an internal ZFC construction that works over any model, not just the countable transitive models.


For example, the Boolean-value approach to forcing allows us to make sense of forcing over the universe, within ZFC. One defines the Boolean values $[\![\varphi]\!]$ for any formula $\varphi$ in the forcing language, by induction on $\varphi$. This allows one to speak of which statements are forceable or not over any model of set theory, and suffices for the consistency proofs. 


Meanwhile, one can turn the Boolean-valued model $V^{\mathbb{B}}$ into an actual classical 2-valued model simply by taking the quotient by an ultrafilter $U\subset\mathbb{B}$, and there is no need for $U$ to be $V$-generic in this process, and even $U\in V$ is completely fine. The elements of the quotient are the equivalence classes with respect to the relation $\sigma\sim\_U\tau\iff [\![\sigma=\tau]\!]\in U$. This is not the same as the usual value $\text{val}(\sigma,U)$ assignment, except when $U$ is $V$-generic. This gives rise to the Boolean ultrapower map $j:V\to \check V\_U$, defined by $j:x\mapsto [\check x]\_U$, which is an elementary embedding of $V$ into the class model $\check V\_U$, and $\check V\_U$ has its forcing extension $\check V\_U[G]$ as a class inside $V$. The generic object $G$ is simply the equivalence class of the *name* of the generic object $G=[\dot G]\_U$. Thus, one never needs to leave $V$ to speak of the forcing extensions of $V$. When there are large cardinals, one can even arrange that $\check V\_U$ is transitive, and these Boolean ultrapowers can be viewed as large cardinal embeddings. 


Dan Seabold and I give a fairly thorough account of the Boolean ultrapower in our paper [Boolean ultrapowers as large cardinal embeddings](http://jdh.hamkins.org/boolean-ultrapowers/). In particular, this paper contains examples of all of the types of examples you request. 


**Update.** Here is an example that may be more like what you had wanted. 


**Theorem.** If there is a supercompact cardinal, then there is transitive inner model, containing all ordinals, with a Laver indestructible supercompact cardinal. Similarly, there is an inner model with a supercompact cardinal $\kappa$ for which $2^\kappa=\kappa^+$ and another with a supercompact cardinal $\kappa$ for which $2^\kappa>\kappa^+$. 


Proof. These results and others like it appear in [A. Apter, V. Gitman, J. D. Hamkins, “Inner models with large cardinal features usually obtained by forcing,” Archive for Mathematical Logic, 51(2012):257-283](http://jdh.hamkins.org/innermodelswithlargecardinals/). Suppose that $\kappa$ is supercompact in $V$. Let $j:V\to M$ be a $\theta$-supercompactness embedding for some $\theta$ for which $2^{\theta^{\lt\kappa}}=\theta^+$. (This is possible because the SCH holds above any supercompact cardinal.) Let $\mathbb{P}$ be the Laver preparation forcing for $j(\kappa)$ as defined in $M$, but starting above $\theta$. Thus, $\mathbb{P}$ is $\leq\theta$-closed in $M$ and hence also in $V$, and by counting we can see that there are only $\theta^+$ many dense subsets of $\mathbb{P}$ in $V$. So in $V$ we may construct an $M$-generic filter $G\subset \mathbb{P}$. Thus, $M[G]$ is a transitive inner model of $V$ in which $j(\kappa)$ is a Laver indestructible supercompact cardinal. By also combining $\mathbb{P}$ with further forcing, we can ensure that the GCH holds or fails at $j(\kappa)$, or a variety of other situations. QED


The general theorem here is the following, where a partial order $\mathbb{Q}$ is $\lt\kappa$-friendly, if for every $\delta\lt\kappa$, there is a condition below which $\mathbb{Q}$ adds no new subsets to $\delta$. 


**Theorem.**(Seabold, Hamkins) If $\kappa$ is strongly compact, then for any $\lt\kappa$-friendly notion of forcing, there is a transitive inner model satisfying every sentence forced by $\mathbb{Q}$ over $V$. 


The proof uses Boolean ultrapowers, and the point is that strong compactness is enough to enable one to find a well-founded Boolean ultrapower. 


