Unprovability results in ZFC

Here's one from Kunen's thesis to ponder upon: Is every subset of the plane in the sigma algebra generated by arbitrary rectangles (product of arbitrary sets of reals)?

Proof that this is true under CH: Suppose $W \subset \mathbb{R}^2$ is a well order on reals of order type $\omega_1$. Fix $A \subset \mathbb{R}^2$. Let $B = A \backslash W$, $C = A \cap W$. Then for any $x, y \in \mathbb{R}$, the vertical section $B_x = \{z : (x, z) \in B\}$ and the horizontal section $C^{y} = \{z: (z, y) \in C\}$ are countable. Let us show that $B$ is in the sigma algebra generated by rectangles. The argument for $C$ is similar. Notice that you can write $B$ as a countable union of subsets of plane all of whose vertical sections have at most one point. Now use the fact that any subset of plane all of whose vertical sections are closed is in the sigma algebra generated by rectangles.

Kunen generalizes this to show that under $MA(\kappa)$, every subsets of $\kappa^2$ is in the sigma algebra generated by rectangles in $\kappa^2$.

For the reverse, besides the rvm argument (which I didn't need in the comments below since I only needed a weak form of rvm that holds in Carlson's model), Kunen also showed that adding $\omega_2$ Cohen reals to a model of GCH gives a model where this statement is false.

There are numerous examples of statements of interest to ordinary mathematicians that are unprovable in $ZFC$. First to clarify that what "of interest to ordinary mathematicians" means. I understand it to mean that result that follow from proof theoretic theorems like the Godel Incompletement Theorem are not of interest to ordinary mathematicians. For instance, the following $\text{Con}(ZFC)$, $\text{Con}(ZFC + \text{Con}(ZFC))$, etc, where $Con$ means the statement asserting the consistency of the theory. Some people would consider statements studied by Set Theory to be not ordinary mathematics. This is a point of view I don't quite understand. Numerous problems unprovable in ZFC were questions from analysis, topology, or algebra. People such as Cantor and Lebesgue tried to obtain partial result by using method considered more ordinary today. After much research in set theory, it was found that these question were unprovable using ordinary method formalizable in ZFC. Some of these questions are arguably more interesting than they would otherwise have been because logical and set theoretic technique allowed something to be said.

Below are some statements that appear to be of ordinary mathematics and found to be independent of ZFC.

One of the most well known is the continuum hypothesis: Is every infinite subset of the $\mathbb{R}$ in bijection with $\mathbb{N}$ or $\mathbb{R}$. The Cantor Bendixson Theorem and the perfect set property were some early topological attempts to resolve this problem. Ultimately, Cohen's forcing and Godel's inner model L showed both answers to the the Continuum hypothesis are consistent. So neither answers can be proven or disproven in $ZFC$.

A topological space has the ccc (countable chain condition) if and only if all collections of disjoint open subsets are countable. For example $\mathbb{R}$ is ccc, which follows from being separable. $\mathbb{R}$ is also a linear ordering. The Suslin Hypothesis is the statement : There are no linearly ordered topological spaces that are ccc and not separable. This is also independent of ZFC (and even independent of ZFC + Generalized Continuum Hypothesis and ZFC + not the Continuum Hypothesis).

From algebra, the Whitehead problem: Is every abelian group $G$ such that $Ext^1(A;Z) = 0$ a free abelian group? Shelah proved this was independent of ZFC.

Large cardinals are little bit worse than the unprovability from above. ZFC + large cardinal axiom is strictly stronger consistency wise, in that their existence imply the consistency of ZFC.

Give $\mathbb{N}^\mathbb{N}$ the usual product topology. A set $A \subset \mathbb{N}^\mathbb{N}$ is analytic if it is the continuous image of a closed set. Two players play by choosing natural numbers in alternating turns. The game ends with a sequence $f$ of natural numbers by putting all the turns together. Player I wins if $f \in A$. Player II wins if $f \notin A$. The axiom of analytic determinacy states that for every analytic $A$ someone always has a winning strategy. This is unprovable in $ZFC$. It is equivalent to a large cardinal axiom: the exists of $x^\sharp$ for all reals $x$.

The axiom of determinacy is the the same statement above but for all $A \subset \mathbb{N}^\mathbb{N}$. This stronger form is inconsistent with the axiom of choice. It is unprovable in ZF. ZF + axiom of determinacy is equiconsistent to $ZFC + \omega$ Woodin Cardinals (an even stronger large cardinal hypothesis).

Interestingly, if one takes $A$ to be a closed or open set, this axiom of closed determinacy is the well known Gale-Stewart Theorem (which is proved in ZFC). If $A$ is a Borel Set, then by Martin Theorem, the determinacy of Borel Sets is provable in ZFC.

These are some statement which on first glance or historically appeared to have been questions properly of analysis, topology, algebra, or combinatorics. However the usual methods formalizable in ZFC were incapable of resolving these problems.

As for literature, Jech's $\textit{Set Theory}$ and Kunen's $\textit{Set Theory}$ are good place for these results and learning how the first two examples are proved. $\textit{The Higher Infinite}$ is a good place to learn about large cardinals and the history of large cardinals and determinacy. The proof of the determinacy results require more difficult inner model theory. They are probably in the Handbook of Set Theory.

By unprovable, do you mean undecidable/independent?

Have you seen the List of statements undecidable in ZFC on Wikipedia?

You may also find the following MathOverflow question useful: What are some reasonable-sounding statements that are independent of ZFC?

The continuum hypothesis is as 'real-world' as one could hope for, I think. Though calling that 'real-world' is a stretch.