Provability in PA

[rzach]

There should be a discussion of what PA can prove (esp that Q can't). It'd be independently interesting & important to see how applying the induction schema works, but various facts are also stated without proof in model-theory/models-of-arithmetic/models-of-PA