What does the Kirby-Paris Theorem mean? I was recently reading about the Hydra game and how it always terminates. What amazed me was how this is not provable in Peano arithmetic. Now as far as I understand PA, it constructs the natural numbers by taking motivation from all the basic properties of numbers that we observe in the 'real' world. However, the Hydra game which essentially is a problem that you could encounter in 'real life' is not explainable using our basic knowledge about numbers. So that led me to think that there must be some property about numbers (that obviously exists axiomatically in mathematics) that exists in real life but we cannot observe it or are yet to observe.
I apologise if I am treating a lot of the things very non-rigourously but it was just a thought that entered my mind while reading about this. Would love to see what others think.
 A: Its about ordinals. Which can be defined in PA, and proved to be well founded, ie a generalization of induction. All ordinals up to but not including $\epsilon_0$ can be proved to be well ordered in PA. The hydra game requires induction on $\epsilon_0$, and it is this same level of induction that proves the consistency of PA.
A: 
as far as I understand PA, it constructs the natural numbers by taking motivation from all the basic properties of numbers that we observe in the 'real' world

I think this over-simplifies the issue.
There are two "levels" to $\mathsf{PA}$. The first is the idea that the natural numbers are uniquely captured (modulo some basic algebraic facts) by the principle of induction; this amounts to the categoricity of second-order Peano arithmetic. The second level is the choice of first-order logic as our specific mechanism for expressing this induction principle in $\mathsf{PA}$; different choices of logic would result in different amounts of power. First-order logic cannot directly express the "naive" induction principle, and so instead approximates it via a scheme of instances. (See here for some general comments about axiom schemes.)
The weakness of $\mathsf{PA}$ - by which I mean specifically first-order Peano arithmetic - should be thought of as reflecting the weakness of first-order logic as a framework. The same core idea, implemented in a different logic, can in fact entail the termination of all Hydra games. Interestingly, it takes some work to find a logic whose version of Peano arithmetic is "intermediate" in strength between $\mathsf{PA}$ and second-order Peano arithmetic; see e.g. here.
