What arithmetical theorems can plain $\lambda \Pi$ reason about?
As Andrej notes, $\lambda\Pi$ is a conservative extension of first-order logic which means:


  Adding the axioms of PA to $\lambda\Pi$ gives exactly the same arithmetic theorems as PA.


However, because of the more expressive system, it is possible to finitely axiomatize induction using the following (encoding of) this axiom:

$$ \forall P: {\mathbb N}\rightarrow \mathrm{Type}, P\ 0 \rightarrow (\forall n, P\ n \rightarrow P\ (S\ n))\rightarrow \forall n, P\ n$$

Note that you need a single Martin-Löf universe to be able to state this. Adding equality and the other PA axioms (definitions for $+$, $\times$, injectivity of $S$) in a similar manner, one might ask if this axiomatization is conservative over PA, or rather HA, since we don't necessarily want the Excluded Middle.

The answer is yes, though this is quite a non-trivial thing! The proof involves some somewhat deep ideas from the field of realizability.

Finally, though this is a fine axiomatic system, it may be frustrating to note that $+$ and $\times$ (and equality, I guess) do not have the computational behavior one might expect in a dependently typed theory, as one would in a system like Coq or Agda.

This is where Martin-Löf's inductive families comes in: one can give a computational content to the induction axiom, which allows one to define addition and multiplication, as well as prove injectivity of $S$ if enough power is given to the type-level computation rules (this point is probably a story for another time). 

And finally one can even define existential quantifiers and equality itself using these families, which is a quite remarkable observation from the theory of inductive families.

Note that Twelf seems to frown upon these last 2 steps, preferring to keep $\beta$ equality alone in its computation, and having predicates for everything else. They have their reasons, I guess.