Are there books or survey articles explaining the subject to a non-expert? To clarify what I mean, here is a couple of issues that I would like to read about. (I am mainly interested in references but would appreciate answers to these specific questions.)
1) 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?
2) I vaguely remember that there are arithmetic facts provable in ZF but not in PA. Is this indeed the case? Are there simple explicit examples? Is there a way to understand, at least informally, why PA is not enough? (E.g. a proof may use analysis but why cannot it be reformulated in terms of some kind of "constructible" numbers and functions?)
Background: I am as far from logic as a mathematician can be.