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.
Best Answer
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).