Examples of statements which are true but not provable

Speaking informally and working, for example, in Peano Arithmetic (PA), we know that the essence of the Gödel's first incompleteness theorem is that there are true statements (in our model PA), which are not provable in that model. However, looking for "concrete" examples of such theorems, I found, for example, Paris–Harrington theorem - which is true but unprovable in PA.

Thus, I have a few questions: do we know that this theorem is true since it can be proven in the second-order arithmetic? and if so, are there other ways to prove "concrete" statements that they are unprovable but true, except showing that they have a proof in a bigger system?

In fact, is the separation between such "concrete" theorems and self-referring ones (as the ones appearing the Gödel's proof) a justified one, in the philosophical sense? That is - both are true but unprovable...

Thanks for everyone.

Before discussing any of the technical issues associated with your question: Yes, in order to ensure that a statement (about numbers) is true (in the standard model), we currently do not have any procedure other than exhibiting a proof. (In fact, most mathematicians would argue that this is the only way to meaningfully discuss truth.) If the statement is unprovable in $\mathsf{PA}$, such a proof by necessity is in a stronger system, typically a fragment of set theory, $\mathsf{ZFC}$, sometimes a fragment of second order arithmetic, $\mathsf{Z}_2$. But sometimes we go beyond $\mathsf{ZFC}$. The typical extensions we consider usually assume large cardinals. There is a well justified body of evidence indicating that it makes sense to say that proofs of arithmetic statements in these systems are indeed true (I link to a small discussion on these matters near the end).

(Since proof is at the heart of this discussion, you may be interested is a series of essays by computer scientists, mathematicians, and philosophers, on The nature of mathematical proof that was published in the journal Philos. Trans. R. Soc. Lond. Ser. A Math. Phys. Eng. Sci, vol 363, No. 1835, Oct 15, 2005. Sadly, the only link I have is behind a paywall.)

There is a technical difference between the sentences produced by Gödel's techniques (or Rosser's) and sentences such as the strong Ramsey theorem that the Paris-Harrington theorem discusses. (For additional examples, see here and the references listed there.)

Gödel's statement is $\Pi^0_1$, that is, it has the form $\forall n\,\psi(n)$ where $\psi$ is a recursive statement (in the language of arithmetic, all its quantifiers are bounded). The strong Ramsey theorem is $\Pi^0_2$, that is, it has the form $\forall n\,\exists m\,\psi(n,m)$, where $\psi$ is recursive.

$\Pi^0_1$ are meaningful statements even by strict finitistic standards (see for example Richard Zach's dissertation and his discussion of Tait's analysis of Hilbert's program). They are true if they are unprovable (in fact, $\mathsf{PA}$ proves every sentence $\phi$ that is true of the natural numbers and such that $\lnot\phi$ is $\Pi^0_1$): If $\exists n\,\psi(n)$ is true, then for some number $m$, we can prove this statement simply by verifying $\psi(m)$ which, being a recursive statement, has a straightforward verification -- informally, we run a computer program that is guaranteed to halt, and check that the program outputs $\mathtt{Yes}$.

On the other hand, $\Pi^0_2$ statements cannot be called finitistic. If unprovable, this does not automatically ensure their validity (or falsehood). However, they admit a natural interpretation: They state that certain recursive function is total (if the sentence is $\forall n\,\exists m\,\psi(n,m)$, the function $f(n)=m$ assigns to each $n$ the least $m$ such that $\psi(n,m)$), that is, they state that certain computer program will halt, no matter its input. Typical independent $\Pi^0_2$ statements have the peculiarity that the corresponding recursive function is fast growing (see for example this discussion, or my article on Goodstein sequences). By a theorem of Wainer, there is a standard mathematical approach to verifying their unprovability, namely, one checks that the function $f$ under discussion eventually dominates the first $\varepsilon_0$ functions in a fast growing hierarchy.

One could consider Gödel statements and the like as first generation independence statements, and the more "combinatorial" $\Pi^0_2$ statements that followed as second generation. The mathematical arguments involved in either case are really very different. A third generation family of independence statements would be $\Pi^0_1$ combinatorial statements, so they are finitistic in the sense of Hilbert's program, but they have immediate, apparent mathematical (as opposed to meta-mathematical) meaning. Such a family of statements is considered of great interest. Remarkably, recent work of Harvey Friedman has produced such examples, see for example his book on Boolean relation theory, available at his page.

This is by no means the end of the story. For example, we now have a whole family of independent meta-mathematical statements of increased complexity of which $\mathrm{Con}(\mathsf{PA})$ (the sentence in the second incompleteness theorem) is but the weakest possible. See for example Aspects of Incompleteness by Per Lindström, or Metamathematics of first-order arithmetic by Petr Hájek and Pavel Pudlák. In the context of set theory, we can go further, as the completeness theorem tells us that set theory is consistent if and only if $\mathrm{Con}(\mathsf{ZFC})$ holds. We can go beyond this and require the existence of an $\omega$-model (one whose set of natural numbers is isomorphic to the standard model) or even stronger, the existence of a $\beta$-model (that is, a well-founded model). Woodin has explained how his $\Omega$-logic provides in a sense an ultimate extension to this process.

We also have families of $\Pi^0_2$ statements whose truth is harder and harder to verify. For example, the Paris-Harrington theorem gives a result that is not only independent of $\mathsf{PA}$ but also independent of the theory obtained by adding to $\mathsf{PA}$ all true $\Pi^0_1$ statements. But it is easy to verify once we go beyond this theory. On the other hand, Friedman identified a finite form of Kruskal's tree theorem that cannot be verified by so-called predicative means, which means that adding it to $\mathsf{PA}$ gives us a system with consistency strength significantly higher than that of $\mathsf{PA}$ with, say, Goodstein's theorem.

And we can go beyond, as Friedman has examples of $\Pi^0_2$ statements whose proof requires assumptions of a large cardinal character (typically, the existence of Mahlo cardinals of all finite orders, but recent examples go much further).

In set theory we study the consistency strength hierarchy, and have identified remarkable structure, starting with the identification of the large cardinal hierarchy. For a brief and somewhat technical discussion of these issues, see here. The point is that we can see these results as extending significantly beyond arithmetic the realm of what is true but unprovable (in specific formal systems).

First we need to define what do we mean when we say "true". In the context of $\sf PA$ this is somewhat of a Platonistic approach where we take $\Bbb N$ to be the standard model of $\sf PA$, so everything is measured against that model. Therefore when we say "true" about an arithmetical statement we mean that it is true in $\Bbb N$.

So in order to show that a statement is true we need to prove that it holds for $\Bbb N$. One way is indeed to prove it from a stronger system, like second-order arithmetic, which is categorical (i.e. it only has one model, up to isomorphism). Another would be using an even stronger system like set theory (e.g. $\sf ZFC$) to prove more about the natural numbers.

In order to prove that a statement is unprovable we need to show that there exists at least one model of $\sf PA$ in which it is false. We can do that either directly, or by showing that the statement implies something we already know is unprovable. For example, if we show that $\varphi$ implies $\operatorname{Con}(\sf PA)$ then we know that $\varphi$ is unprovable because $\operatorname{Con}(\sf PA)$ is unprovable.

Finally, the distinction between "concrete" and "contrived" statements which a true but unprovable is indeed a philosophical one, and I would accept that it is justified. We often want to know that a mathematical concept helps solving problems which are not created just for its own sake, and "contrived" statements often look like they were cooked specifically for the purpose of incompleteness (and they are, in most cases). However the line between these can be sometimes fuzzy and subjective -- much like any other philosophical line.

Löb's theorem provides many examples of a certain type. Following Gödel's construction, there is a predicate $$\operatorname{Prov}(·)$$ of Peano Arithmetic which means “this statement is provable in PA”.

(To do this, we set up a Gödel numbering scheme for statements of PA, so that the statement $S$ is represented by its Gödel number $⸢S⸣$, and then $$\operatorname{Prov}(⸢S⸣)$$ actually means “the statement $S$ whose Gödel number is $⸢S⸣$ is provable in PA”).)

Löb's theorem states that if PA can prove $\operatorname{Prov}(⸢P⸣)\to P$, then it can also prove $P$. The contrapositive is that if PA cannot prove $P$, then it cannot prove $\operatorname{Prov}(⸢P⸣)\to P$ either.

Now let $P$ be some false statement of arithmetic, say “$2+2=5$”. Certainly PA cannot prove $2+2=5$. Therefore, by Löb's theorem, it cannot prove $$\operatorname{Prov}(⸢2+2=5⸣) \to 2+2=5 \tag{$\star$}.$$

But $(\star)$ is unequivocally true, because the antecedent, $\operatorname{Prov}(⸢2+2=5⸣)$, is false. So this is a true statement of PA that, by Löb's theorem, is unprovable in PA.

Of course “$2+2=5$” can be replaced with any other trivially false claim.