It is a trivial fact that forcing can not produce finite sets of ground model objects. However there are situations, 
where we can use forcing to prove the existence of finite objects with some properties. For example consider the following 
result of Shelah (I learned this example from the answer given by Prof. Komjath in [http://mathoverflow.net/questions/29945/forcing-as-a-tool-to-prove-theorems](http://mathoverflow.net/questions/29945/forcing-as-a-tool-to-prove-theorems)):

>**Theorem (Shelah)** There exists  a finite $K_4$-free graph which, when the edges colored by $2$ colors, always contains a 
monocolored triangle.

Shelah's proof of the theorem is simply as follows: 
He constructs a forcing extension which adds a graph $X$ with the same property but 
with $\aleph_0$ colors. Then $X$ has the edge-coloring property for $2$ colors, 
as well. Then using compactness theorem, $X$ must contain a finite subgraph $Y$ with the same property.
 As forcing cannot create new finite graphs, $Y$ is already present 
in the ground model.  By Godel, $ZFC$ proves that there is such a graph. 


Now my question is that if there are more examples of the above kind. To be more precise:

>**Question 1.** Are there any other examples for producing some finite object $Y$ (with some properties)
in the following way:

>1) We provide a suitable generic extension in which there is an infinite object $X$ with the required properties,

>2) By compactness (or other devices), we can conclude that there must be a finite subset $Y$ of $X$ with the same properties,

>3) So we can conclude that the object must exist in the ground model.

**Remark 1.** I am mostly interested in examples where it is not known (or it is difficult) to produce such finite object directly

**Remark 2.** It seems that some partition type theorems are of this type: It is possible to derive some kind of 
finite partition theorems (like finite Ramsey theorem) using infinite versions of them. So if we can prove 
the infinite version of these partition theorems, then we have produced examples of the required type 
(there are cases where we can prove infinite partition theorems using forcing). 

>**Question 2.** Is Shelah's result the first non-trivial example of an answer to question 1? Are there othe non-trivial constructions of the above kind before him?

**Remark 3.** Here by non-trivial I mean the above strategy is, in some sense, the only method for producing the required finite object.