I never heard anyone claim the existence of a forcing proof of the Erdős-Rado theorem. On the other hand, yes, there are several proofs of nonindependence statements that use forcing.
One is Shelah's proof for the existence of a finite *K*_{4}-free graph which, when the edges colored by 2 colors, always contains a monocolored triangle (a problem of Erdős and Hajnal). Here is the argument. He constructs a forcing extension which adds a graph *X* with the same property but with ℵ_{0} colors (this is not easy). Obviously, *X* has the edge-coloring property for 2 colors, as well. *X* must contain a finite subgraph *Y* with the same property. This is compactness, or, any proof for the Erdős-de Bruijn theorem gives it. As forcing cannot create new finite graphs, *Y* is already present in the underlying model. That is, there is a finite graph as required in any countable, transitive model of a sufficiently large part of ZFC. By Gödel, this is only possible, if ZFC proves that there is such a graph.

Another example is the original proof of the Baumgartner-Hajnal theorem: ω_{1}→(α)^{2}_{k} if α<ω_{1}, *k*<ω. They first deduced it from Martin's axiom, then a specific argument gives that if it holds in a cardinal preserving extension, then it holds in the original model. Therefore, it holds in every countable, transitive model of a sufficiently large fragment of ZFC, and we can finish as above.