show/hide this revision's text 1 [made Community Wiki]

Harvey Friedman has devoted a large portion of his career to finding "natural" statements that are unprovable in ZFC. One example is given at the end of Martin Davis's article "The incompleteness theorem," Notices AMS 53 (2006), 414-418:

http://www.ams.org/notices/200604/fea-davis.pdf

It takes a paragraph or so to state the definitions so I won't do so here, but the point is that, unlike many other examples, which clearly make reference to uncountable sets or are just Goedelian diagonalization statements in disguise, Friedman's proposition is a purely finitary statement in graph theory whose statement gives no hint of large cardinals. Indeed it is a small perturbation of a graph-theoretical theorem with an elementary proof.

For another example of Friedman's work, see his book Boolean Relation Theory and Incompleteness, a draft of which is downloadable from his website:

http://www.math.ohio-state.edu/~friedman/manuscripts.html

Here Friedman presents a family of innocuous-looking elementary statements about functions and sets and unions/intersections/complements. Almost all statements in the family have easy proofs in ZFC (or actually much weaker systems), but one of them requires a large cardinal axiom.

Friedman is aware that these examples don't quite reach the holy grail of a completely natural finitary mathematical statement that is independent of ZFC, but he continues to make progress in this direction. You can subscribe to the Foundations of Mathematics mailing list if you want to keep track of his latest results.