What does it mean for something to be true but not provable in peano arithmetic?

Specifically, the Paris-Harrington theorem.

In what sense is it true? True in Peano arithmetic but not provable in Peano arithmetic, or true in some other sense?

Solution 1:

Peano Arithmetic is a particular proof system for reasoning about the natural numbers. As such it does not make sense to speak about something being "true in PA" -- there is only "provable in PA", "disprovable in PA", and "independent of PA".

When we speak of "truth" it must be with respect to some particular model. In the case of arithmetic statements, the model we always speak about unless something else is explicitly specified is the actual (Platonic) natural numbers. Virtually all mathematicians expect these numbers to "exist" (in whichever philosophical sense you prefer mathematical objects to exist in) independently of any formal system for reasoning about them, and the great majority expect all statements about them to have objective (but not necessarily knowable) truth values.

We're very sure that everything that is "provable in PA" is also "true about the natural numbers", but the converse does not hold: There exist sentences that are "true about the actual natural numbers" but not "provable in PA". This was famously proved by Gödel -- actually he gave a (formalizable, with a few additional technical assumptions) proof that a particular sentence was neither "provable in PA" nor "disprovable in PA", and a convincing (but not strictly formalizable) argument that this sentence is true about the actual natural numbers.

Paris-Harrington shows that another particular sentence is of this kind: not provable in PA, yet true about the actual natural numbers.

Solution 2:

The Paris-Harrington theorem is actually the theorem that states that the strengthened [finite] Ramsey theorem is unprovable in first-order Peano Arithmetic.

However, since the Ramsey theorem is provable in second-order arithmetic, and therefore true in the standard model of Peano arithmetic, we can say that the theorem is true in a very deep and concrete sense.

Generally speaking, when we say a statement about the integer is true we mean that it is true in the standard model, which is the model of second-order Peano arithmetic, and it is all the numbers which can be generated by finitely many iteration of the successor function from zero. (Non-standard models of first-order PA exist, and there are non-standard integers which cannot be generated by finite iterations of the successor from zero.)

You may also want to read this thread about the difference between truth and provability.

Solution 3:

The other answers are excellent, but I would like to point out that Peano arithmetic is a particularly bad first example for understanding the distinction between truth and provability because

• you have an intuitive notion of what the word "true" means that is getting in the way, and
• there are, roughly speaking, two levels of mathematics going on and it is easy to confuse them.

So let's pick a better example where there's no possibility of confusion: the first-order theory of groups. I'm not going to spell out in detail what this is; consider it an exercise to write it down in full. After writing down the language of groups, write down the group theory axioms.

"Provable" has an unambiguous meaning here: it means "provable from the axioms of group theory." By the completeness theorem, this is equivalent to "true for all groups."

"True" is meaningless here unless you take it to mean "true for all groups," which is not the sense in which the Paris-Harrington theorem is true. What is meaningful is to say that a statement in the language of groups is true in a particular model: for example, the statement

$$\exists g : g \neq e, g^2 = e$$

is true in a group $G$ precisely when that group has a nontrivial element of order $2$.

The difference between group theory and first-order Peano arithmetic is that when it comes to Peano arithmetic, mathematicians have a special model that they really like, namely the "actual natural numbers," and "true" in this context means "true of this special model." As Asaf says, one way to define this model is as the unique model of second-order Peano arithmetic; however, first-order Peano arithmetic does not have a unique model (e.g. by upward Löwenheim-Skolem).

This is very different from the situation with group theory; nobody has a group $G$ that they like so much that they would define "true" to mean "true of $G$"!

As a final remark, note that by the completeness theorem, "true of the actual natural numbers but not provable" is equivalent to "true of the actual natural numbers but false for some other model of Peano arithmetic." This may seem like a strange state of affairs, but the analogous situation in group theory ("true of some group but false of some other group") is not so strange.