What arithmetical theorems can plain $\lambda \Pi$ reason about?

Question

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?

Answer 1

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.