A $\Pi_1^0$ statement is one of the form $\forall n\,\varphi(n)$, where $\varphi(n)$ is some recursively verifiable statement about $n$. This can be made more precise, but I want to keep the description this way, to give an idea of what some of the issues are. The negation of $\Pi^0_1$ statement, if true, is easily provable: After all, all it says is that some fixed number $n_0$ must have an easily verifiable property. You just have to exhibit a counterexample explicitly and it is straightforward to verify its validity.

In practice, of course, we know that there are computational issues that this ignores, but the point remains.

However, it is not so clear that, if true, a $\Pi^0_1$ statement must be provable. And, in fact, that is not the case. Goedel showed this, but his examples are not particularly natural. Now, if you prove that a $\Pi^0_1$ statement is not decidable from PA, the standard (first order) axioms of number theory, then of course the result must be true. Otherwise, its negation would have been provable.

There are a few natural combinatorial $\Pi^0_1$ statements that cannot be verified in PA. Harvey Friedman has worked hard to produce examples of this kind with intrinsic combinatorial interest (if not yet immediate appeal to number theorists), because most natural examples are more complicated: $\Pi^0_2$, essentially assertions that some function is total: For all $n$ there is some $m$ for which something straightforward to verify holds.

Ferretti mentioned Goodstein's theorem, and auniket mentioned Paris-Harrington. I like Goodstein's theorem, because a few years ago I managed to find a formula for the function that computes how long it takes the sequence starting with $n$ to stop. Since this is not provable in PA, the formula was just beyond what can be grasped in first order number theory, and *that*, I found very interesting.

A variant of Paris-Harrington is a result of Kanamori-McAloon, with which I've also done some work, showing combinatorially that the version for pairs gives rise to a function that grows precisle as Ackermann's function. The point is: Just because something is beyond the grasp of a formal system, does not mean it is beyond our comprehension. Very interesting combinatorics can still happen here.

Stillwell mentioned the graph minor theorem. This is more interesting, in that not only they are beyond PA, but also beyond significant strengthenings of PA.

All of these examples are provable in ZFC, the basic system of axioms of set theory. Harvey Friedman has produced natural examples that go beyond ZFC and involve large cardinals. His page is full of nice examples of this kind, mostly $\Pi^0_2$, but also (recently) several interesting $\Pi^0_1$ ones.

Still, as pointed out by agcl, in all of the $\Pi^0_1$ examples, there is a natural sense in which, once we show the statement is independent of the formal system, then we actually have that it is true.

Although Goldbach's conjecture is $\Pi^0_1$, another very famous problem in number theory, the twin primes conjecture, is not, at least not with our current knowledge. Neither it nor its negation are obviously true if verified independent. I am not saying there is any evidence whatsoever for assuming the twin primes conjecture is independent of PA, in fact, that would be more than unexpected. However, it is much more natural to expect that a natural $\Pi^0_2$ statement, such as this one, is independent, than it is to expect that for a $\Pi^0_1$. And it would be very interesting, because then we would need a different method for verifying its truth, since we would have consistency of both the statement and its negation, and no clear evidence of which holds in the usual (standard) model ${\mathbb N}$.

**Coda:** A recent thread mentioned a paper where it is claimed that all current approaches, if they show the independence of a $\Pi^0_2$ statement from PA, actually also show it from the (much) stronger system obtained by adding to PA all the true $\Pi^0_1$ statements. Although the claim is something of an exaggeration, it can be made more precise in terms of what kind of model theoretic arguments are used to show the independence. The natural combinatorial examples listed above all fall in this category: They are true, they are independent of PA, and they remain independent in the theory resulting from strengthening PA as explained. Harvey Friedman's examples in ZFC are more interesting in this regard.

*[Edited to fix some obvious unintentional lies.]*

14more comments