lo.logic - A book explaining power and limitations of Peano Axioms?

Several people have given excellent answers to your second question, so let me address the first.

2) As far as I remember, PA do not have a "built-in" scheme for inductive definitions. So I assume that it is not immediately clear how to define things like $x_n$ or the $n$-th Fibonacci number. How do they do things like that? One can define some specific coding of finite sequences of numbers and use that, but this is so ugly and so specific to aritmetics, it there a better way?

Permitting definitions by primitive recursion moves you from Peano arithmetic to Godel's System T. This is a conservative extension of Peano arithmetic, which also allows defining functions by recursion over the natural numbers.

In the modern presentation (due to Tait, IIRC), the idea is that we move from a first-order logic with a domain of natural numbers, to a multi-sorted first-order logic, where quantification is permitted over functions of higher type in addition. So the sorts of the logic are types like $mathbb{N}$, $mathbb{N} to mathbb{N}$, $(mathbb{N} to mathbb{N}) to mathbb{N}$, and so on. The terms of higher type are given by a simple typed lambda calculus (i.e., a simple functional programming language).

One of the nice things about System T is that even though it is conservative over Peano arithmetic, it also makes the step from arithmetic to analysis much easier to see. Since a real number can be represented by a term of type $mathbb{N} to mathbb{N} times mathbb{N}$ (e.g, as a Cauchy sequence of rationals), in this setting it's easy to understand exactly how much extra axiomatic strength various theorems of analysis need beyond basic Peano arithmetic. As F.G. Dorais has already mentioned, Simpson's Subsystems of Second-Order Arithmetic is the standard reference here.