I've read that System F cannot state or prove theorems of the First Order Theory of Arithmetic. I assume this is because we lack dependent types, so we cannot explicitly express $\forall n:\mathbb{N}.P(n)$ as an inhabitable type. Thus, $\lambda\Pi$/LF seems promising despite its lacking expressivity of functions.
My question concerns whether it is even possible to encode proofs of arithmetic in $\lambda\Pi$. I am assuming there would need to be some sense of equality, perhaps a type only inhabited when two terms are $\beta\eta$-equivalent. Some sense of induction seems necessary also. I'm not convinced that such things wouldn't require additional inference rules to the theory.
At a minimum, I'm interested in being able to encode statements like "$\forall x \forall y. x + y = y + x$", or "$\forall x\exists y.x<y\land\textrm{prime}(y)$", and I don't know if these can even be encoded as types.
- Can theorems of arithmetic be encoded and proved in plain $\lambda\Pi$? If not, what's required?