On provability of Paris–Harrington theorem It is said that the Paris–Harrington theorem is true, but not provable in Peano arithmetic. I want to ask: So how do they know that it is true if it has no proof? I cannot imagine someone knows something is true but cannot explain why?
I think a proof has a definition for a theory like Peano arithmetic, probably it is a sequence of propositions satisfying some metalanguage rules‎! (is it correct?). So there is not any proof for Paris–Harrington theorem with this definition. But there is some proof (defined somehow else). There doesn't seem to be a way to know something without a convincing proof‎! Is there?
 A: First, a bit of terminology. There is a particular combinatorial result, a strengthened form of Ramsey's theorem. That result is provable in many systems, including ZF set theory. Let's call this combinatorial result $R$. The Paris-Harrington theorem shows that result $R$ is not provable in Peano Arithmetic. In what I believe is the most common terminology in the field, the result $R$ itself is not the "Paris-Harrington theorem". 
Now, $R$ cannot be disprovable in Peano Arithmetic, because then it would be disprovable in ZF as well. But $R$ is provable in ZF, and ZF is consistent. 
Keep in mind that most ordinary mathematical proofs are not written in any formal system: they are just written in natural language using accepted methods of reasoning. 

As a side note, the Paris-Harrington theorem itself is unprovable in Peano arithmetic, but for a trivial reason: the Paris-Harrington theorem states that $R$ is unprovable in Peano Arithmetic, and because of the incompleteness theorem Peano Arithmetic cannot prove that any theorem is unprovable in itself. Peano Arithmetic cannot even prove that "1 + 1 = 3 is unprovable in Peano Arithmetic", much less that $R$ is unprovable.
What Paris and Harrington actually showed is that $R$ implies, within PA, the consistency of PA. Therefore, by the incompleteness theorem, $R$ cannot be provable in PA. 
