Producing finite objects by forcing! 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 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.
--

Question 3. Are there any results of the above type proved in other parts of mathematics other than logic?

Of course Shelah's result is of this type, but the example given by Hamkins is in mathematical logic.
 A: Here is another example. 
The theorem is: every finite partial order can be found as a suborder of the partial order of the Turing degrees. 
On the one hand, one can prove this by undertaking a priority construction, a detailed argument constructing the degrees directly. On the other hand, one can force to add countably many mutually generic Cohen reals $x_n$, and then noting that finite sums of them show that any finite power set algebra can be found in the degrees. But every finite partial order is a suborder of a finite power set order. Finally, the existence of any particular such pattern in the Turing degrees is a $\Sigma^1_1$ property and hence absolute to the ground model by Shoenfield absoluteness. So there was already such a pattern in the ground model. 
A similar argument finds every countable order as a suborder of the Turing degrees. In both cases, what the direct argument amounts to is the construction of sufficiently generic degrees. With forcing, we can just go all the way to a fully generic real, and this simplifies things.
