Examples of ZFC theorems proved via forcing  This is an old suggestion of Joel David Hamkins at the end of his answer to this question: Forcing as a tool to prove theorems
I just noticed it while trying to understand his answer. But indeed it would be nice to have a big list of $ZFC$ theorems that were proven first by forcing. 
A very well known example is Silver's Theorem about the fact that the $GCH$ can't fail first at a singular cardinal of uncountable cofinality (say for instance $\aleph_{\omega_1}$), I had read somewhere (Jech, maybe) that Silver proved it first using forcing. 
Also if anyone knows theorems of pcf theory that were first proven using forcing, please post them.
 A: In descriptive set theory, there is a significant number of results that have been established using forcing; typically, dichotomy theorems such as Silver's (a $\Pi^1_1$ equivalence relation has only countably many classes, or else there is a perfect set of pairwise inequivalent points).
Harrington used what is now called the Gandy-Harrington topology to eliminate the use of forcing from these arguments, replacing it instead with an appeal to ``effective'' techniques. So, for example, Silver's result can actually be stated as: If $E$ is a $\Pi^1_1$-in-the-parameter-$a$ equivalence relation, then either every $E$-class is itself $\Pi^1_1(a)$ (so, in particular, there are only countably many), or else there are perfectly many inequivalent classes.
For a long while, we actually thought these uses of forcing or effective descriptive set theory were essential to the theory. Benjamin Miller recently transformed the field by showing how ``derivative'' arguments can eliminate just about all these uses.
The latest twist is that Richard Ketchersid and I have been studying structural properties of models of determinacy, and have shown that the descriptive set theoretic dichotomies hold in this context. This is more general than what Miller's technique can establish. Once again, our arguments make essential use of forcing (and ultrapower constructions). 
For example, we have shown that the $G_0$-dichotomy of Kechris-Solecki-Todorcevic holds in models of ${\sf AD}^+$  of arbitrary graphs on reals: Any such graph either can be colored by ordinals (so that points connected by an edge receive different colors) or else, there is a continuous homomorphism of the graph $G_0$ into $G$. (See for example these slides from a recent talk for details and complete definitions).
Ben has shown how Baire category arguments allow one to deduce most other dichotomies from appropriate versions of the $G_0$-dichotomy. Using this, Richard and I have deduced some interesting global dichotomies in these models (meaning, they hold of all sets, not just sets of reals). For example, in the presence of large cardinals, $L({\mathbb R})$ is a model of determinacy, and for any $X\in L({\mathbb R})$, either $X$ can be well-ordered inside $L({\mathbb R})$, or else, there is in $L({\mathbb R})$ an injection of ${\mathbb R}$ into $X$. In short: containing a copy of the reals is the only obstacle to being well-orderable. (This is a strong version of the statement that one cannot well-order the reals "definably".) --- Actually, Richard and I first established this directly, via a forcing argument, but it can now be deduced from our version of the $G_0$-dichotomy.
(There is another, subtle use of forcing in the context of determinacy, via the theory of generic codings.)
A: The Gitik-Shelah theorem is also perhaps an example, first proved with forcing by its discoverers, and then without by Anastasis Kamburelis and David Fremlin independently: 
Moti Gitik, Saharon Shelah, Forcing with ideals and simple forcing notions, Israel J. Math., 68 (1989), 129-160.
And the same authors have more in:
More on simple forcing notions and forcing with ideals, APAL, 59 (1993), 219-238.
A: Another example is Solovays result to partition any stationary subset $S \subset \kappa$ into $\kappa$ many staionary subsets of $S$. It is mentioned in Jechs book that Solovay first used a generic ultrapower construction to prove this. Later a more elementary proof was found, using no 'metamathematical' concepts as forcing or ultrapowers of the universe, similar to the history of the proofs of Silvers theorem.
A: (A): In "A nonconstructible $Δ_3^1$ set of integers" the following is proved by Robert Solovay using forcing:
Theorem. Assuming the existence of a Ramsey cardinal, there is a $Δ_3^1$ set of sets of integers, $X$, which is not constructible from any set of integers $A$.
The following is stated about the proof of the above theorem:
It is amusing to note
that the proof uses Cohen's notion of a generic set of integers. This is probably the
first application of Cohen's method to set theory yielding an absolute result rather
than a relative consistency result.
(B): The paper "
Extensions of the measurable choice theorem by means of forcing.
Israel J. Math. 14 (1973), 104–114" by Wesley,  presents some $ZFC$ results using forcing. The following is taken from its introduction:
Using the method of forcing of set theory, we prove the following two theorems on the existence of measurable choice functions. Let $T$ be the closed unit interval $[0,1]$ and let $m$ be the usual Lebesgue measure defined on the Borel subsets of $T$. 
Theorem 1: Let $S⊂T×T$ be a Borel set such that, for all $t∈T$, $S_t=\{x|(t,x)∈S\}$ is countable and nonempty; then there exists a countable series of Lebesgue-measurable functions $f_n:T→T$ such that $S_t=\{f_n(t)|n∈ω\}$ for all $t∈T$. 
Theorem 2: Let $W⊂[0,1]×[0,1]$ be a Borel set such that, for each $x∈[0,1]$, $W_x=\{y|(x,y)∈W\}$ is uncountable; then there exists a function $h:[0,1]×[0,1]→W$ with the following properties: 
(a) for each $x∈[0,1]$, the function $h(x,⋅)$ is one-one and onto $W_x$ and is Borel measurable; 
(b) for each $y,h(⋅,y)$ is Lebesgue measurable; 
(c) the function $h$ is Lebesgue measurable.
A: Another example around a theorem of Gitik and Shelah: If there is a total extension $m:\mathcal{P}([0, 1]) \rightarrow [0, 1]$ of Lebesgue measure then there is an uncountable set of reals all of whose Lebesgue null subsets are countable.
Proof sketch: Force with the measure algebra of $m$. By (a weak form of) Gitik-Shelah theorem (whose original proof uses generic ultrapower arguments too), this forcing adds at least $\omega_1$-many random reals in the generic extension. But this set of randoms is also in the generic ultrapower so by elementarity we have such a set in $V$.
For some open questions along these lines see Fremlin's survey article on real valued measurable cardinals and also his problem list.
A: One example is Solovay's theorem that if the axiom of determinacy holds, then each subset of $\omega_1$ is constructible from a real. The proof breaks into cases. Case One is when $\omega^{L[t]}_1=\omega_1$ holds for some real $t$. Case Two is when this does not hold. Case One has a direct proof, and then Case Two is reduced to Case One via forcing. The punchline is that Case One never holds!  
A: The Baumgartner-Hajnal theorem, from "A proof (involving Martin’s Axiom) of a partition relation". Fund. Math., 78(3):193–203, 1973. 
Actually, there is a very interesting mathematical story here, and several problems. 
The question was first asked about uncountable sets of reals and $\omega_1$. Quickly, it was recognized to be a problem about what we now call non-special orders. $L$ is non-special iff $L\to(\omega)^1_\omega$, meaning that if $L$ is split into countably many pieces, at least one is not reverse-well-ordered, i.e., it contains a strictly increasing sequence. Baumgartner and Hajnal proved that $L\to(\alpha)^2_n$ for any countable ordinal $\alpha$ and $n<\omega$.
(In human: If L is non-special, and to each subset of $L$ of size 2 we assign a color, there being only finitely many colors to begin with, then for any countable ordinals $\alpha$ there is a subset of $L$ order isomorphic to $\alpha$, all of whose 2-sized subsets are assigned the same color.)
Their original proof uses Martin's axiom, as it depends on a kind of diagonalization over certain functions $f:\omega\to\omega$ and one needs that if there are not "too many" of them, then there is one dominating all. This is to my mind the key use of MA in their paper, although there is another one. Then one argues that being special is preserved by ccc forcing  and that the conclusion is absolute.
Galvin later found a very nice combinatorial argument that avoids forcing. Clinton Conley recently found a similar proof. It rests on a kind of abstract Fubini theorem, the point being that the special linear sub-orders of a non-special $L$ form a proper $\sigma$-complete ideal. Galvin noticed that the result should hold in a more general setting, and conjectured that that's the case.
The conjecture was later proved by Stevo Todorcevic: $P\to(\alpha)^2_n$ holds if $P$ is non-special, but it suffices that $P$ is a partial order, rather than a linear order. Stevo's beautiful argument  proceeds by three stages:


*

*To each $P$ we can associate a certain tree; if $P$ is non-special, so is the tree (in the usual sense of non-special, hence the name), and the result holds for $P$ iff it does for the tree. This is a direct combinatorial argument, but it is very general (not just for colorings of pairs). For example, it simplifies the proof that $P\to(\omega)^1_\omega$ implies $P\to(\alpha)^1_\omega$ for any $\alpha<\omega_1$. We get a nice combinatorial theory of non-special trees: For example, an appropriate version of Fodor's lemma holds.

*The result holds for non-special trees of size less than the pseudo-intersection number ${\mathfrak p}$. (This is one of the cardinal invariants of the continuum.) Again, the proof does not use forcing.

*Finally, a forcing argument shows that ${\mathfrak p}$ can be made as large as one wants while preserving being non-special, and by absoluteness we get the full theorem. The argument here shows in particular, that one does not need preservation of being non-special under ccc forcing, simpler particular classes of forcing notions suffice. 


Stevo's paper is "Partition relations for partially ordered sets". Acta Math., 155(1-2):1–25, 1985. 
As far as I know, there is no forcing-free proof of 3., that the result holds for all non-special trees $T$, even if $|T|\ge{\mathfrak p}$. It cannot be a direct argument, as Stevo found examples of non-special trees all of whose subtrees of small size are special. Albin Jones indicated a while ago that he had an argument, but I never saw it and his webpage and contact information vanished since. In my mind, this remains open.
A few years ago, Rene Schipperus proved a "topological" version of Baumgartner-Hajnal, namely that if $L$ is an uncountable subset of ${\mathbb R}$, or $\omega_1$, then for any $\alpha<\omega_1$ and any coloring of the 2-sized subsets of $L$ with finitely many colors, we can find monochromatic sets of type $\alpha+1$ that, moreover, are closed in the natural topology of ${\mathbb R}$ or $\omega_1$. Rene uses an argument that builds on the original approach, and in particular uses MA. I don't know how to prove his theorem without using forcing.
Finally: The corresponding result in dimension 3 should be that if $P$ is a non-special partial order, then $P\to(\alpha,n)^3$, i.e., that if the 3-sized subsets of $P$ are colored with 2 colors, then either for the first color for each $\alpha<\omega_1$ there are homogeneous sets of type $\alpha$, or else for the second color there are linearly ordered homogeneous sets of any finite size. This is open, and several people have worked hard on it for years.  
A: I gave a talk on the very same subject this week, and some of the given examples were not mentioned here. Have a look at the slides.
A: My favorite example of this is Stevo Todorcevic's paper "Compact subsets of the first Baire class" (JAMS, 1999).  Fix a Polish space $X$ (for us it will be no loss of generality to take $X = \mathbb{N}^\mathbb{N}$).  The Baire class 1 functions on $X$ are those functions which are the limit of a pointwise convergent sequence of continuous functions.  A compact space which embeddable into the Baire class 1 functions with the pointwise topology is said to be Rosenthal compact.  A typical example of a Rosenthal compacta is the set $\mathbb{H}$ of monotone increasing functions from $[0,1]$ to $[0,1]$.
Two others are the ``split interval'' (which consists of those elements of $\mathbb{H}$ whose range is contained in $\{0,1\}$) and the one point compactification of a discrete set of cardinality at most continuum.  The class of Rosenthal compacta is closed under countable products and closed subspaces.
Todorcevic proved several ZFC results about Rosenthal compacta using forcing.  Probably the best example in the paper (in terms of the use of forcing machinery) is the proof that any Rosenthal compacta contains a dense metrizable subspace.  Before this it was an open problem whether there was a c.c.c. non-separable Rosenthal compacta.  Todorcevic also proves in this paper that a Rosenthal compacta which does not contain an uncountable discrete subspace must map at most two-to-one into a metric space.  Furthermore if such a space is non-metrizable, it must contain a homeomorphic copy of the split interval.  Finally, he showed that any non $G_\delta$-point in a separable Rosenthal compacta is the unique accumulation point of a discrete subspace of cardinality continuum.  One of the key lemmas of the paper is that the property of being a Rosenthal compacta is preserved when one appropriately reinterprets the compacta in any generic extension.
