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?
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.